add cmovo (#1483)

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"

src/Assembly/Syntax.v

@@ -59,6 +59,7 @@ Inductive OpCode :=
 | cmovb
 | cmovc
 | cmovnz
+| cmovo
 | cmp
 | db
 | dd

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, _

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.