Rust catch-up (#273)

* Add wands to the ast Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * Add a wands set to the pstate Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * defunctorize things that are only ever instantiated to be symbolic Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * some fixes Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * Can produce and consume wands Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * basic support for wands in WISL Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * Add package to the syntax, start implementing Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * magic wand is implemented! Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * add parsing for magic wands Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * adds non-empty check for packaging wands Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * use consumer and producers insteda of get/set/rem Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * Add splitting mechanism, can't implement its usage in unifier yet Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * license date update Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * implement master unification plans Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * splitting mechanism for wand footprint consumption is working! Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * package lcmd improve printing Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * some extensions Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * removing batteries, updating printbox yada yada yada Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * remove printbox_text dependency of core Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * extract_head passes in Gillian-Rust Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * fix pretty printing of apply_lem Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * attempt at something Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * Revert "attempt at something" This reverts commit a9b728c. * add shl infix for Expr Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * forgot to expose Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * add utility Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * slight optim of div Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * helpers Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * temp hack Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * adds implication to the language of formulae Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * udpate z3 Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * Revert "udpate z3" This reverts commit 6730699. * specialized simpl * add support for repeat operation Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * expose Expr.list_repeat Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * debug Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * can learn last element of a list also Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * second step of merge, kanillian but only the trivial part * done * esy-gmp fix * fix normalisation of pure expressions Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com> * PC.Dummy exposes annot type * forgot to expose in mli --------- Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
GillianPlatform · Dec 12, 2023 · c7bbb9e · c7bbb9e
1 parent 5ac2402
commit c7bbb9e
Show file tree

Hide file tree

Showing 106 changed files with 4,213 additions and 3,923 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -28,17 +28,17 @@ jobs:
         with:
           python-version: "3.10"
       - name: Installing esy
-        run: sudo npm install -g esy@0.6.12 --unsafe-perm
+        run: sudo npm install -g esy@0.7.2 --unsafe-perm
       - name: Installing Python prerequisites
         run: sudo pip install sphinx furo
       - name: Restore Cache
         id: restore-cache
         uses: actions/cache@v3
         with:
           path: _export
-          key: ${{ runner.os }}-esy-0.6.12-${{ hashFiles('esy.lock/index.json') }}
+          key: ${{ runner.os }}-esy-0.7.2-${{ hashFiles('esy.lock/index.json') }}
           restore-keys: |
-            ${{ runner.os }}-esy-0.6.12-
+            ${{ runner.os }}-esy-0.7.2-
       - name: Esy install
         run: "esy install"
       - name: Import Cache
@@ -280,9 +280,9 @@ jobs:
         uses: actions/cache@v3
         with:
           path: _export
-          key: docker-esy-0.6.12-${{ hashFiles('esy.lock/index.json') }}
+          key: docker-esy-0.7.2-${{ hashFiles('esy.lock/index.json') }}
           restore-keys: |
-            docker-esy-0.6.12-
+            docker-esy-0.7.2-
       - name: build and export docker image
         uses: docker/build-push-action@v4
         with:

diff --git a/Gillian-C/lib/CMemory.ml b/Gillian-C/lib/CMemory.ml
@@ -151,27 +151,4 @@ let execute_action name heap params =
   | AMem Free -> execute_free heap params
   | AMem Move -> execute_move heap params
   | AGEnv GetDef -> execute_genvgetdef heap params
-  | AMem
-      ( GetSingle
-      | SetSingle
-      | RemSingle
-      | GetArray
-      | SetArray
-      | RemArray
-      | GetBounds
-      | SetBounds
-      | RemBounds
-      | GetHole
-      | SetHole
-      | RemHole
-      | GetZeros
-      | SetZeros
-      | RemZeros
-      | GetFreed
-      | SetFreed
-      | RemFreed ) ->
-      failwith
-        (Printf.sprintf
-           "%s is an action related to a General Assertion, it should never be \
-            called during a concrete execution"
-           name)
+  | AMem SetZeros -> failwith "cannot execute set_zeros in concrete memory"
diff --git a/Gillian-C/lib/LActions.ml b/Gillian-C/lib/LActions.ml
@@ -9,24 +9,7 @@ type mem_ac =
   | Load
   | Free
   | Move
-  | GetSingle
-  | SetSingle
-  | RemSingle
-  | GetArray
-  | SetArray
-  | RemArray
-  | GetHole
-  | SetHole
-  | RemHole
-  | GetZeros
   | SetZeros
-  | RemZeros
-  | GetBounds
-  | SetBounds
-  | RemBounds
-  | GetFreed
-  | SetFreed
-  | RemFreed
 
 type genv_ac = GetDef
 type ac = AGEnv of genv_ac | AMem of mem_ac
@@ -38,36 +21,6 @@ type ga = Single | Array | Hole | Zeros | Bounds | Freed
 
 let is_overlapping_asrt _ = false
 
-let ga_to_setter ga =
-  AMem
-    (match ga with
-    | Single -> SetSingle
-    | Array -> SetArray
-    | Hole -> SetHole
-    | Zeros -> SetZeros
-    | Bounds -> SetBounds
-    | Freed -> SetFreed)
-
-let ga_to_getter ga =
-  AMem
-    (match ga with
-    | Single -> GetSingle
-    | Array -> GetArray
-    | Hole -> GetHole
-    | Zeros -> GetZeros
-    | Bounds -> GetBounds
-    | Freed -> GetFreed)
-
-let ga_to_deleter ga =
-  AMem
-    (match ga with
-    | Single -> RemSingle
-    | Array -> RemArray
-    | Hole -> RemHole
-    | Zeros -> RemZeros
-    | Bounds -> RemBounds
-    | Freed -> RemFreed)
-
 (* Then serialization and deserialization functions *)
 
 let mem_prefix = "mem"
@@ -82,24 +35,7 @@ let str_mem_ac = function
   | Load -> "load"
   | Move -> "move"
   | Free -> "free"
-  | GetSingle -> "getSingle"
-  | SetSingle -> "setSingle"
-  | RemSingle -> "remSingle"
-  | GetArray -> "getArray"
-  | SetArray -> "setArray"
-  | RemArray -> "remArray"
-  | GetBounds -> "getBounds"
-  | SetBounds -> "setBounds"
-  | RemBounds -> "remBounds"
-  | GetHole -> "getHole"
-  | SetHole -> "setHole"
-  | RemHole -> "remHole"
-  | GetZeros -> "getZeros"
   | SetZeros -> "setZeros"
-  | RemZeros -> "remZeros"
-  | GetFreed -> "getFreed"
-  | SetFreed -> "setFreed"
-  | RemFreed -> "remFreed"
 
 let mem_ac_from_str = function
   | "alloc" -> Alloc
@@ -110,24 +46,7 @@ let mem_ac_from_str = function
   | "load" -> Load
   | "free" -> Free
   | "move" -> Move
-  | "getSingle" -> GetSingle
-  | "setSingle" -> SetSingle
-  | "remSingle" -> RemSingle
-  | "getArray" -> GetArray
-  | "setArray" -> SetArray
-  | "remArray" -> RemArray
-  | "getBounds" -> GetBounds
-  | "setBounds" -> SetBounds
-  | "remBounds" -> RemBounds
-  | "getHole" -> GetHole
-  | "setHole" -> SetHole
-  | "remHole" -> RemHole
-  | "getZeros" -> GetZeros
   | "setZeros" -> SetZeros
-  | "remZeros" -> RemZeros
-  | "getFreed" -> GetFreed
-  | "setFreed" -> SetFreed
-  | "remFreed" -> RemFreed
   | s -> failwith ("Unkown Memory Action : " ^ s)
 
 let str_genv_ac = function
@@ -168,11 +87,6 @@ let ga_from_str = function
   | "mem_freed" -> Freed
   | str -> failwith ("Unkown memory assertion : " ^ str)
 
-let ga_to_action_str action str = ga_from_str str |> action |> str_ac
-let ga_to_setter_str = ga_to_action_str ga_to_setter
-let ga_to_getter_str = ga_to_action_str ga_to_getter
-let ga_to_deleter_str = ga_to_action_str ga_to_deleter
-
 (** Additional stuff *)
 
 let is_overlapping_asrt_str str = ga_from_str str |> is_overlapping_asrt
diff --git a/Gillian-C/lib/LActions.mli b/Gillian-C/lib/LActions.mli
@@ -9,24 +9,7 @@ type mem_ac =
   | Load
   | Free
   | Move
-  | GetSingle
-  | SetSingle
-  | RemSingle
-  | GetArray
-  | SetArray
-  | RemArray
-  | GetHole
-  | SetHole
-  | RemHole
-  | GetZeros
   | SetZeros
-  | RemZeros
-  | GetBounds
-  | SetBounds
-  | RemBounds
-  | GetFreed
-  | SetFreed
-  | RemFreed
 
 type genv_ac = GetDef
 
@@ -45,19 +28,10 @@ val str_ac : ac -> string
 (** Deserializes a string into an action *)
 val ac_from_str : string -> ac
 
-(** {3 Global assertion and their actions} *)
-
-val ga_to_setter : ga -> ac
-val ga_to_getter : ga -> ac
-val ga_to_deleter : ga -> ac
-
 (** {3 Global assertion serialization } *)
 
 val str_ga : ga -> string
 val ga_from_str : string -> ga
-val ga_to_setter_str : string -> string
-val ga_to_getter_str : string -> string
-val ga_to_deleter_str : string -> string
 
 (** {3 Gillian-related things} *)