Changed syntax to load_effect/store_effect (#24)

Update syntax --------- Co-authored-by: Amber Wu <[email protected]> Co-authored-by: Alexa VanHattum <[email protected]>
wellesley-prog-sys · Jul 26, 2024 · c32d6e0 · c32d6e0
1 parent 93af1fb
commit c32d6e0
Show file tree

Hide file tree

Showing 16 changed files with 45 additions and 45 deletions.
diff --git a/cranelift/codegen/src/inst_specs.isle b/cranelift/codegen/src/inst_specs.isle
@@ -236,7 +236,7 @@
 )
 (spec (load flags val offset)
     (provide 
-       (= result (load flags (widthof result) (bvadd val (sign_ext 64 offset))))))
+       (= result (load_effect flags (widthof result) (bvadd val (sign_ext 64 offset))))))
 (instantiate load load)
 
 (form store
@@ -247,5 +247,5 @@
 )
 (spec (store flags val_to_store addr offset)
     (provide 
-       (= result (store flags (widthof val_to_store) val_to_store (bvadd (zero_ext 64 addr) (sign_ext 64 offset))))))
+       (= result (store_effect flags (widthof val_to_store) val_to_store (bvadd (zero_ext 64 addr) (sign_ext 64 offset))))))
 (instantiate store store)
diff --git a/cranelift/codegen/src/isa/aarch64/inst.isle b/cranelift/codegen/src/isa/aarch64/inst.isle
@@ -3323,7 +3323,7 @@
 ;; widths and sign/zero-extending properties.
 (decl aarch64_uload8 (AMode MemFlags) Reg)
 (spec (aarch64_uload8 amode flags)
-      (provide (= result (zero_ext 32 (load flags 8 amode))))
+      (provide (= result (zero_ext 32 (load_effect flags 8 amode))))
       (require (= 32 (widthof result))))
 (rule (aarch64_uload8 amode flags)
       (let ((dst WritableReg (temp_writable_reg $I64))
@@ -3336,7 +3336,7 @@
         dst))
 (decl aarch64_uload16 (AMode MemFlags) Reg)
 (spec (aarch64_uload16 amode flags)
-      (provide (= result (zero_ext 32 (load flags 16 amode))))
+      (provide (= result (zero_ext 32 (load_effect flags 16 amode))))
       (require (= 32 (widthof result))))
 (rule (aarch64_uload16 amode flags)
       (let ((dst WritableReg (temp_writable_reg $I64))
@@ -3349,7 +3349,7 @@
         dst))
 (decl aarch64_uload32 (AMode MemFlags) Reg)
 (spec (aarch64_uload32 amode flags)
-      (provide (= result (load flags 32 amode)))
+      (provide (= result (load_effect flags 32 amode)))
       (require (= 32 (widthof result))))
 (rule (aarch64_uload32 amode flags)
       (let ((dst WritableReg (temp_writable_reg $I64))
@@ -3362,7 +3362,7 @@
         dst))
 (decl aarch64_uload64 (AMode MemFlags) Reg)
 (spec (aarch64_uload64 amode flags)
-      (provide (= result (load flags 64 amode)))
+      (provide (= result (load_effect flags 64 amode)))
       (require (= 64 (widthof result))))
 (rule (aarch64_uload64 amode flags)
       (let ((dst WritableReg (temp_writable_reg $I64))
@@ -3394,22 +3394,22 @@
 ;; widths.
 (decl aarch64_store8 (AMode MemFlags Reg) SideEffectNoResult)
 (spec (aarch64_store8 amode flags val)
-      (provide (= result (store flags 8 (extract 7 0 val) amode))))
+      (provide (= result (store_effect flags 8 (extract 7 0 val) amode))))
 (rule (aarch64_store8 amode flags val)
       (SideEffectNoResult.Inst (MInst.Store8 val amode flags)))
 (decl aarch64_store16 (AMode MemFlags Reg) SideEffectNoResult)
 (spec (aarch64_store16 amode flags val)
-      (provide (= result (store flags 16 (extract 15 0 val) amode))))
+      (provide (= result (store_effect flags 16 (extract 15 0 val) amode))))
 (rule (aarch64_store16 amode flags val)
       (SideEffectNoResult.Inst (MInst.Store16 val amode flags)))
 (decl aarch64_store32 (AMode MemFlags Reg) SideEffectNoResult)
 (spec (aarch64_store32 amode flags val)
-      (provide (= result (store flags 32 (extract 31 0 val) amode))))
+      (provide (= result (store_effect flags 32 (extract 31 0 val) amode))))
 (rule (aarch64_store32 amode flags val)
       (SideEffectNoResult.Inst (MInst.Store32 val amode flags)))
 (decl aarch64_store64 (AMode MemFlags Reg) SideEffectNoResult)
 (spec (aarch64_store64 amode flags val)
-      (provide (= result (store flags 64 val amode))))
+      (provide (= result (store_effect flags 64 val amode))))
 (rule (aarch64_store64 amode flags val)
       (SideEffectNoResult.Inst (MInst.Store64 val amode flags)))
 (decl aarch64_fpustore32 (AMode MemFlags Reg) SideEffectNoResult)

diff --git a/cranelift/codegen/src/isa/x64/inst.isle b/cranelift/codegen/src/isa/x64/inst.isle
@@ -2373,7 +2373,7 @@
 
 (decl x64_mov (Amode) Reg)
 (spec (x64_mov addr)
-      (provide (= result (conv_to 64 (load (extract 79 64 addr) 64 (extract 63 0 addr))))))
+      (provide (= result (conv_to 64 (load_effect (extract 79 64 addr) 64 (extract 63 0 addr))))))
 (rule (x64_mov addr)
       (mov64_mr addr))
 
@@ -2385,7 +2385,7 @@
                         64  
                         (zero_ext
                               32
-                              (load 
+                              (load_effect 
                                     (extract 79 64 src)
                                     (switch mode 
                                           ((ExtMode.BL) 8)
@@ -2556,7 +2556,7 @@
 
 (decl x64_movrm (Type SyntheticAmode Gpr) SideEffectNoResult)
 (spec (x64_movrm ty addr data)
-       (provide (= result (store (extract 79 64 addr) ty (conv_to ty data) (extract 63 0 addr)))))
+       (provide (= result (store_effect (extract 79 64 addr) ty (conv_to ty data) (extract 63 0 addr)))))
 (rule (x64_movrm ty addr data)
       (let ((size OperandSize (raw_operand_size_of_type ty)))
         (SideEffectNoResult.Inst (MInst.MovRM size data addr))))
@@ -4628,10 +4628,10 @@
 
 (decl x64_add_mem (Type Amode Gpr) SideEffectNoResult)
 (spec (x64_add_mem ty addr val)
-      (provide (= result (store 
+      (provide (= result (store_effect 
                         (extract 79 64 addr) 
                         ty 
-                        (conv_to ty (bvadd (load (extract 79 64 addr) ty (extract 63 0 addr)) (conv_to ty val))) 
+                        (conv_to ty (bvadd (load_effect (extract 79 64 addr) ty (extract 63 0 addr)) (conv_to ty val))) 
                         (extract 63 0 addr))
             )
       )

diff --git a/cranelift/isle/isle/src/ast.rs b/cranelift/isle/isle/src/ast.rs
@@ -206,8 +206,8 @@ pub enum SpecOp {
     If,
     Switch,
 
-    Load,
-    Store,
+    LoadEffect,
+    StoreEffect,
 }
 
 /// A specification of the semantics of a term.

diff --git a/cranelift/isle/isle/src/parser.rs b/cranelift/isle/isle/src/parser.rs
@@ -536,8 +536,8 @@ impl<'a> Parser<'a> {
             "rev" => Ok(SpecOp::Rev),
             "cls" => Ok(SpecOp::Cls),
             "clz" => Ok(SpecOp::Clz),
-            "load" => Ok(SpecOp::Load),
-            "store" => Ok(SpecOp::Store),
+            "load_effect" => Ok(SpecOp::LoadEffect),
+            "store_effect" => Ok(SpecOp::StoreEffect),
             x => Err(self.error(pos, format!("Not a valid spec operator: {x}"))),
         }
     }

diff --git a/cranelift/isle/isle/src/printer.rs b/cranelift/isle/isle/src/printer.rs
@@ -277,8 +277,8 @@ impl Printable for SpecOp {
             SpecOp::Rev => "rev",
             SpecOp::Cls => "cls",
             SpecOp::Clz => "clz",
-            SpecOp::Load => "load", 
-            SpecOp::Store => "store",
+            SpecOp::LoadEffect => "load_effect", 
+            SpecOp::StoreEffect => "store_effect",
         })
     }
 }

diff --git a/cranelift/isle/veri/veri_engine/examples/load/load_add_panic.isle b/cranelift/isle/veri/veri_engine/examples/load/load_add_panic.isle
@@ -10,13 +10,13 @@
   ((args (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
 )
 (spec (lhs x y) 
-  (provide (= result (bvadd (load #x0000 (widthof x) x) (load #x0000 (widthof y) y)))))
+  (provide (= result (bvadd (load_effect #x0000 (widthof x) x) (load #x0000 (widthof y) y)))))
 (decl lhs (Value Value) Inst)
 (extern extractor lhs lhs)
 (instantiate lhs lhs_form)
 
 (spec (rhs x y) 
-  (provide (= result (bvadd (load #x0000 (widthof x) x) (load #x0000 (widthof y) y)))))
+  (provide (= result (bvadd (load_effect #x0000 (widthof x) x) (load #x0000 (widthof y) y)))))
 (decl rhs (Value Value) Inst)
 (extern constructor rhs rhs)
 

diff --git a/cranelift/isle/veri/veri_engine/examples/load/load_conditional.isle b/cranelift/isle/veri/veri_engine/examples/load/load_conditional.isle
@@ -10,13 +10,13 @@
 )
 
 (spec (lhs cond x y) 
-  (provide (= result (load #x0000 (widthof (if cond x y)) (if cond x y)))))
+  (provide (= result (load_effect #x0000 (widthof (if cond x y)) (if cond x y)))))
 (decl lhs (bool Value Value) Inst)
 (extern extractor lhs lhs)
 (instantiate lhs lhs_form)
 
 (spec (rhs x y) 
-  (provide (= result (load #x0000 (widthof x) x))))
+  (provide (= result (load_effect #x0000 (widthof x) x))))
 (decl rhs (Value Value) Inst)
 (extern constructor rhs rhs)
 

diff --git a/cranelift/isle/veri/veri_engine/examples/store/broken_bvsub_store_with_load.isle b/cranelift/isle/veri/veri_engine/examples/store/broken_bvsub_store_with_load.isle
@@ -43,10 +43,10 @@
 
 (decl x64_add_mem (Type Amode Gpr) SideEffectNoResult)
 (spec (x64_add_mem ty addr val)
-      (provide (= result (store 
+      (provide (= result (store_effect 
                         (extract 79 64 addr) 
                         ty 
-                        (conv_to ty (bvsub (load (extract 79 64 addr) ty (extract 63 0 addr)) (conv_to ty val))) 
+                        (conv_to ty (bvsub (load_effect (extract 79 64 addr) ty (extract 63 0 addr)) (conv_to ty val))) 
                         (extract 63 0 addr))
             )
       )

diff --git a/cranelift/isle/veri/veri_engine/examples/store/broken_isub_store_with_load.isle b/cranelift/isle/veri/veri_engine/examples/store/broken_isub_store_with_load.isle
@@ -43,10 +43,10 @@
 
 (decl x64_add_mem (Type Amode Gpr) SideEffectNoResult)
 (spec (x64_add_mem ty addr val)
-      (provide (= result (store
+      (provide (= result (store_effect
                         (extract 79 64 addr) 
                         ty 
-                        (conv_to ty (bvadd (load (extract 79 64 addr) ty (extract 63 0 addr)) (conv_to ty val))) 
+                        (conv_to ty (bvadd (load_effect (extract 79 64 addr) ty (extract 63 0 addr)) (conv_to ty val))) 
                         (extract 63 0 addr))
             )
       )

diff --git a/cranelift/isle/veri/veri_engine/examples/store/store_switch.isle b/cranelift/isle/veri/veri_engine/examples/store/store_switch.isle
@@ -10,14 +10,14 @@
 )
 
 (spec (lhs cond val2 val3)
-  (provide (= result (store #x0000 (widthof (switch cond ($true val2) ($false val3))) (switch cond ($true val2) ($false val3)) #x0000000000000000)))
+  (provide (= result (store_effect #x0000 (widthof (switch cond ($true val2) ($false val3))) (switch cond ($true val2) ($false val3)) #x0000000000000000)))
   )
 (decl lhs (bool Value Value) Inst)
 (extern extractor lhs lhs)
 (instantiate lhs lhs_form)
 
 (spec (rhs val2 val3) 
-  (provide (= result (store #x0000 (widthof val2) val2 #x0000000000000000))))
+  (provide (= result (store_effect #x0000 (widthof val2) val2 #x0000000000000000))))
 (decl rhs (Value Value) Inst)
 (extern constructor rhs rhs)
 

diff --git a/cranelift/isle/veri/veri_engine/src/annotations.rs b/cranelift/isle/veri/veri_engine/src/annotations.rs
@@ -259,27 +259,27 @@ fn spec_op_to_expr(s: &SpecOp, args: &Vec<SpecExpr>, pos: &Pos, env: &ParsingEnv
                 .collect();
             Expr::Switch(Box::new(swith_on), arms)
         }
-        SpecOp::Load => {
+        SpecOp::LoadEffect => {
             assert_eq!(
                 args.len(),
                 3,
                 "Unexpected number of args for load operator {:?}",
                 pos
             );
-            Expr::Load(
+            Expr::LoadEffect(
                 Box::new(spec_to_expr(&args[0], env)),
                 Box::new(spec_to_expr(&args[1], env)),
                 Box::new(spec_to_expr(&args[2], env)),
             )
         }
-        SpecOp::Store => {
+        SpecOp::StoreEffect => {
             assert_eq!(
                 args.len(),
                 4,
                 "Unexpected number of args for store operator {:?}",
                 pos
             );
-            Expr::Store(
+            Expr::StoreEffect(
                 Box::new(spec_to_expr(&args[0], env)),
                 Box::new(spec_to_expr(&args[1], env)),
                 Box::new(spec_to_expr(&args[2], env)),

diff --git a/cranelift/isle/veri/veri_engine/src/solver.rs b/cranelift/isle/veri/veri_engine/src/solver.rs
@@ -1249,7 +1249,7 @@ impl SolverCtx {
                     .rev()
                     .fold(last, |acc, x| self.smt.concat(*x, acc))
             }
-            Expr::Load(x, y, z) => {
+            Expr::LoadEffect(x, y, z) => {
                 let ex = self.vir_expr_to_sexp(*x);
                 let ey = self.vir_expr_to_sexp(*y);
                 let ez = self.vir_expr_to_sexp(*z);
@@ -1278,7 +1278,7 @@ impl SolverCtx {
                     self.load_return.unwrap()
                 }
             }
-            Expr::Store(w, x, y, z) => {
+            Expr::StoreEffect(w, x, y, z) => {
                 let ew = self.vir_expr_to_sexp(*w);
                 let ex = self.vir_expr_to_sexp(*x);
                 let ez = self.vir_expr_to_sexp(*z);

diff --git a/cranelift/isle/veri/veri_engine/src/type_inference.rs b/cranelift/isle/veri/veri_engine/src/type_inference.rs
@@ -1380,7 +1380,7 @@ fn add_annotation_constraints(
             tree.next_type_var += 1;
             (veri_ir::Expr::BVPopcnt(Box::new(e1)), t)
         }
-        annotation_ir::Expr::Load(x, y, z) => {
+        annotation_ir::Expr::LoadEffect(x, y, z) => {
             let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
             let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
             let (e3, t3) = add_annotation_constraints(*z, tree, annotation_info);
@@ -1397,11 +1397,11 @@ fn add_annotation_constraints(
 
             tree.next_type_var += 1;
             (
-                veri_ir::Expr::Load(Box::new(e1), Box::new(e2), Box::new(e3)),
+                veri_ir::Expr::LoadEffect(Box::new(e1), Box::new(e2), Box::new(e3)),
                 t,
             )
         }
-        annotation_ir::Expr::Store(w, x, y, z) => {
+        annotation_ir::Expr::StoreEffect(w, x, y, z) => {
             let (e0, t0) = add_annotation_constraints(*w, tree, annotation_info);
             let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
             let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
@@ -1421,7 +1421,7 @@ fn add_annotation_constraints(
 
             tree.next_type_var += 1;
             (
-                veri_ir::Expr::Store(Box::new(e0), Box::new(e1), Box::new(e2), Box::new(e3)),
+                veri_ir::Expr::StoreEffect(Box::new(e0), Box::new(e1), Box::new(e2), Box::new(e3)),
                 t,
             )
         }

diff --git a/cranelift/isle/veri/veri_ir/src/annotation_ir.rs b/cranelift/isle/veri/veri_ir/src/annotation_ir.rs
@@ -225,9 +225,9 @@ pub enum Expr {
     // Switch
     Switch(Box<Expr>, Vec<(Expr, Expr)>),
 
-    Load(Box<Expr>, Box<Expr>, Box<Expr>),
+    LoadEffect(Box<Expr>, Box<Expr>, Box<Expr>),
 
-    Store(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>), 
+    StoreEffect(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>), 
 }
 
 impl Expr {

diff --git a/cranelift/isle/veri/veri_ir/src/lib.rs b/cranelift/isle/veri/veri_ir/src/lib.rs
@@ -190,8 +190,8 @@ pub enum Expr {
 
     WidthOf(Box<Expr>),
 
-    Load(Box<Expr>, Box<Expr>, Box<Expr>),
-    Store(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>),
+    LoadEffect(Box<Expr>, Box<Expr>, Box<Expr>),
+    StoreEffect(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>),
 }
 
 /// To-be-flushed-out verification counterexample for failures
-Original file line number
+Diff line change
@@ Expand Up / @@ -206,8 +206,8 @@ pub enum SpecOp { @@
         If,
         Switch,
-        Load,
-        Store,
+        LoadEffect,
+        StoreEffect,
     }
     /// A specification of the semantics of a term.
@@ Expand Down @@