Modified assembly equivalence checker to allow parsing asm files cont…

…aining "or" instructions. (#1492)

Co-authored-by: OwenConoly <[email protected]>

src/Assembly/Parse.v

@@ -152,6 +152,7 @@ Global Instance show_OpCode : Show OpCode
         | movzx => "movzx"
         | mul => "mul"
         | mulx => "mulx"
+        | or => "or"
         | pop => "pop"
         | push => "push"
         | rcr => "rcr"

src/Assembly/Symbolic.v

@@ -3361,6 +3361,11 @@ Definition SymexNormalInstruction {descr:description} (instr : NormalInstruction
     _ <- SetOperand dst v;
     _ <- HavocFlags;
     zero <- Symeval (PreApp (const 0) nil); _ <- SetFlag CF zero; SetFlag OF zero
+  | Syntax.or, [dst; src] => (* side effects of "or" are identical to side effects of "and" and "xor", according to https://en.wikibooks.org/wiki/X86_Assembly/Logic *)
+    v <- Symeval (orZ@(dst,src));
+    _ <- SetOperand dst v;
+    _ <- HavocFlags;
+    zero <- Symeval (PreApp (const 0) nil); _ <- SetFlag CF zero; SetFlag OF zero
   | Syntax.bzhi, [dst; src; cnt] =>
     cnt <- GetOperand cnt;
     cnt <- RevealConst cnt;

src/Assembly/Syntax.v

@@ -75,6 +75,7 @@ Inductive OpCode :=
 | movzx
 | mul
 | mulx
+| or
 | pop
 | push
 | rcr

src/Assembly/WithBedrock/Semantics.v

@@ -329,8 +329,8 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
       let st := if cnt =? 1 then SetFlag st OF signchange else st in
       let st := SetFlag st CF (Z.testbit l (cnt-1)) in
       Some (HavocFlag st AF)
-  | (and | xor) as opc, [dst; src] =>
-    let f := match opc with and => Z.land | _ => Z.lxor end in
+  | (and | xor | or) as opc, [dst; src] =>
+    let f := match opc with and => Z.land | xor => Z.lxor | _ => Z.lor end in
     v1 <- DenoteOperand sa s st dst;
     v2 <- DenoteOperand sa s st src;
     let v := f v1 v2 in
@@ -398,6 +398,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
   | lea, _
   | mov, _
   | movzx, _
+  | or, _
   | imul, _
   | inc, _
   | push, _

src/Assembly/WithBedrock/SymbolicProofs.v

@@ -1142,7 +1142,7 @@ Proof using Type.
                     | progress Option.inversion_option
                     | progress subst ].
 
-  all : cbn [fold_right map]; rewrite ?N2Z.id, ?Z.add_0_r, ?Z.add_assoc, ?Z.mul_1_r, ?Z.land_m1_r, ?Z.lxor_0_r;
+  all : cbn [fold_right map]; rewrite ?N2Z.id, ?Z.add_0_r, ?Z.add_assoc, ?Z.mul_1_r, ?Z.land_m1_r, ?Z.lxor_0_r, ?Z.lor_0_r;
     (congruence||eauto).
   all: rewrite ?Z.land_ones_low_alt by now try split; try apply Zpow_facts.Zpower2_lt_lin; lia.
   all: rewrite ?(fun x => Z.land_ones_low_alt (x / 8) x) by now split; try (eapply Z.le_lt_trans; [ | apply Zpow_facts.Zpower2_lt_lin ]); try lia; Z.to_euclidean_division_equations; nia.