From 5047e39e77c2124eadb5b46c7d870e88baa16b39 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Tue, 8 Nov 2022 22:12:51 -0500
Subject: [PATCH] add cmovo (#1483)

---
 src/Assembly/Parse.v                      |  1 +
 src/Assembly/Syntax.v                     |  1 +
 src/Assembly/WithBedrock/Semantics.v      | 12 +++++++-----
 src/Assembly/WithBedrock/SymbolicProofs.v |  4 ++--
 4 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
index f2ed5ceed5..f654292e06 100644
--- a/src/Assembly/Parse.v
+++ b/src/Assembly/Parse.v
@@ -136,6 +136,7 @@ Global Instance show_OpCode : Show OpCode
         | cmovb => "cmovb"
         | cmovc => "cmovc"
         | cmovnz => "cmovnz"
+        | cmovo => "cmovo"
         | cmp => "cmp"
         | db => "db"
         | dd => "dd"
diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
index 6cb40f6fd5..fddc4d4357 100644
--- a/src/Assembly/Syntax.v
+++ b/src/Assembly/Syntax.v
@@ -59,6 +59,7 @@ Inductive OpCode :=
 | cmovb
 | cmovc
 | cmovnz
+| cmovo
 | cmp
 | db
 | dd
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index fed36bd63b..e347aa498a 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -179,12 +179,14 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
     SetOperand sa s st dst (Z.b2z b)
   | clc, [] => Some (update_flag_with st (fun fs =>
     set_flag fs CF false))
-  | cmovc, [dst; src] (* Flags Affected: None *)
-  | cmovb, [dst; src] (* Flags Affected: None *)
+  | cmovc, [dst; src] (* CMOVcc: Flags Affected: None *)
+  | cmovb, [dst; src]
+  | cmovo, [dst; src]
     =>
+    let flag := match instr.(op) with cmovc|cmovb => CF | cmovo => OF | _ => PF end in
     v <- DenoteOperand sa s st src;
-    cf <- get_flag st CF;
-    if cf
+    cc <- get_flag st flag;
+    if cc
     then SetOperand sa s st dst v
     else Some st
   | cmovnz, [dst; src] => (* Flags Affected: None *)
@@ -193,7 +195,6 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
     if negb zf
     then SetOperand sa s st dst v
     else Some st
-
   | lea, [reg dst; mem src] => (* Flags Affected: None *)
     Some (update_reg_with st (fun rs => set_reg rs dst (DenoteAddress sa st src)))
   | (add | adc) as opc, [dst; src] =>
@@ -388,6 +389,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
   | jmp, _
   | cmovc, _
   | cmovb, _
+  | cmovo, _
   | cmovnz, _
   | setc, _
   | seto, _
diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v
index 78980799e6..7aaa4ec143 100644
--- a/src/Assembly/WithBedrock/SymbolicProofs.v
+++ b/src/Assembly/WithBedrock/SymbolicProofs.v
@@ -1264,8 +1264,8 @@ Proof using Type.
   Unshelve. all : match goal with H : context[Syntax.adox] |- _ => idtac | _ => shelve end.
   { cbn [fold_right] in *; rewrite ?Z.bit0_odd, ?Z.add_0_r, ?Z.add_assoc in *; assumption. }
 
-  Unshelve. all : match goal with H : context[Syntax.cmovc] |- _ => idtac |  H : context[Syntax.cmovb] |- _ => idtac | _ => shelve end.
-  (* cmovc / cmovb *)
+  Unshelve. all : match goal with H : context[Syntax.cmovc] |- _ => idtac |  H : context[Syntax.cmovb] |- _ => idtac |  H : context[Syntax.cmovo] |- _=> idtac | _ => shelve end.
+  (* cmovc / cmovb / cmovo *)
   all: destruct vCF; cbn [negb Z.b2z Z.eqb] in *; eauto 9; [].
   all: enough (m = m0) by (subst; eauto 9).
   all: clear -Hm0 Hv frame G ; eauto using SetOperand_same.