Add instructions with carry flags

1 files changed, 107 insertions, 10 deletions

diff --git a/src/BoundedArithmetic/Interface.v b/src/BoundedArithmetic/Interface.v
index d66cb5c02..35770b2cd 100644
--- a/src/BoundedArithmetic/Interface.v
+++ b/src/BoundedArithmetic/Interface.v
@@ -89,6 +89,29 @@ Section InstructionGallery.
         0 <= count < n
         -> decode (shrd high low count) <~=~> (((decode high << n) + decode low) >> count) mod 2^n.
 
+  (** Quoting http://www.felixcloutier.com/x86/SHRD.html:
+
+      If the count is 1 or greater, the CF flag is filled with the
+      last bit shifted out of the destination operand and the SF, ZF,
+      and PF flags are set according to the value of the result. For a
+      1-bit shift, the OF flag is set if a sign change occurred;
+      otherwise, it is cleared. For shifts greater than 1 bit, the OF
+      flag is undefined. If a shift occurs, the AF flag is
+      unde-fined. If the count operand is 0, the flags are not
+      affected. If the count is greater than the operand size, the
+      flags are undefined.
+
+      We ignore the CF in the specification; we only have it so that
+      we can ensure that the CF flag gets appropriately clobbered. *)
+  Class shift_right_doubleword_immediate_with_CF := { shrdf : W -> W -> imm -> bool * W }.
+  Global Coercion shrdf : shift_right_doubleword_immediate_with_CF >-> Funclass.
+
+  Class is_shift_right_doubleword_immediate_with_CF (shrdf : shift_right_doubleword_immediate_with_CF) :=
+    decode_snd_shift_right_doubleword_with_CF :>
+      forall high low count,
+        0 <= count < n
+        -> decode (snd (shrdf high low count)) <~=~> (((decode high << n) + decode low) >> count) mod 2^n.
+
   Class shift_left_immediate := { shl : W -> imm -> W }.
   Global Coercion shl : shift_left_immediate >-> Funclass.
 
@@ -96,6 +119,26 @@ Section InstructionGallery.
     decode_shift_left_immediate :>
       forall r count, 0 <= count < n -> decode (shl r count) <~=~> (decode r << count) mod 2^n.
 
+  (** Quoting http://www.felixcloutier.com/x86/SAL:SAR:SHL:SHR.html:
+
+      The CF flag contains the value of the last bit shifted out of
+      the destination operand; it is undefined for SHL and SHR
+      instructions where the count is greater than or equal to the
+      size (in bits) of the destination operand. The OF flag is
+      affected only for 1-bit shifts (see “Description” above);
+      otherwise, it is undefined. The SF, ZF, and PF flags are set
+      according to the result. If the count is 0, the flags are not
+      affected. For a non-zero count, the AF flag is undefined.
+
+      We ignore the CF in the specification; we only have it so that
+      we can ensure that the CF flag gets appropriately clobbered. *)
+  Class shift_left_immediate_with_CF := { shlf : W -> imm -> bool * W }.
+  Global Coercion shlf : shift_left_immediate_with_CF >-> Funclass.
+
+  Class is_shift_left_immediate_with_CF (shlf : shift_left_immediate_with_CF) :=
+    decode_shift_left_immediate_with_CF :>
+      forall r count, 0 <= count < n -> decode (snd (shlf r count)) <~=~> (decode r << count) mod 2^n.
+
   Class shift_right_immediate := { shr : W -> imm -> W }.
   Global Coercion shr : shift_right_immediate >-> Funclass.
 
@@ -103,6 +146,13 @@ Section InstructionGallery.
     decode_shift_right_immediate :>
       forall r count, 0 <= count < n -> decode (shr r count) <~=~> (decode r >> count).
 
+  Class shift_right_immediate_with_CF := { shrf : W -> imm -> bool * W }.
+  Global Coercion shrf : shift_right_immediate_with_CF >-> Funclass.
+
+  Class is_shift_right_immediate_with_CF (shrf : shift_right_immediate_with_CF) :=
+    decode_shift_right_immediate_with_CF :>
+      forall r count, 0 <= count < n -> decode (snd (shrf r count)) <~=~> (decode r >> count).
+
   Class spread_left_immediate := { sprl : W -> imm -> tuple W 2 (* [(low, high)] *) }.
   Global Coercion sprl : spread_left_immediate >-> Funclass.
 
@@ -132,6 +182,20 @@ Section InstructionGallery.
       decode_bitwise_and :> forall x y, decode (and x y) <~=~> Z.land (decode x) (decode y)
     }.
 
+  (** Quoting http://www.felixcloutier.com/x86/AND.html:
+
+      The OF and CF flags are cleared; the SF, ZF, and PF flags are set
+      according to the result. The state of the AF flag is
+      undefined. *)
+  Class bitwise_and_with_CF := { andf : W -> W -> bool * W }.
+  Global Coercion andf : bitwise_and_with_CF >-> Funclass.
+
+  Class is_bitwise_and_with_CF (andf : bitwise_and_with_CF) :=
+    {
+      decode_snd_bitwise_and_with_CF :> forall x y, decode (snd (andf x y)) <~=~> Z.land (decode x) (decode y);
+      fst_bitwise_and_with_CF :> forall x y, fst (andf x y) =~> false
+    }.
+
   Local Notation bit b := (if b then 1 else 0).
 
   Class add_with_carry := { adc : W -> W -> bool -> bool * W }.
@@ -166,6 +230,16 @@ Section InstructionGallery.
   Global Coercion mulhwhh : multiply_high_high >-> Funclass.
   Class multiply_double := { muldw : W -> W -> tuple W 2 }.
   Global Coercion muldw : multiply_double >-> Funclass.
+  (** Quoting http://www.felixcloutier.com/x86/MUL.html:
+
+      The OF and CF flags are set to 0 if the upper half of the result
+      is 0; otherwise, they are set to 1. The SF, ZF, AF, and PF flags
+      are undefined.
+
+      We ignore the CF in the specification; we only have it so that
+      we can ensure that the CF flag gets appropriately clobbered. *)
+  Class multiply_double_with_CF := { muldwf : W -> W -> bool * tuple W 2 }.
+  Global Coercion muldwf : multiply_double_with_CF >-> Funclass.
 
   Class is_mul_low_low (w:Z) (mulhwll : multiply_low_low) :=
     decode_mul_low_low :>
@@ -184,6 +258,14 @@ Section InstructionGallery.
         forall x y, decode (snd (muldw x y)) =~> (decode x * decode y) >> n
     }.
 
+  Class is_mul_double_with_CF (muldwf : multiply_double_with_CF) :=
+    {
+      decode_fst_mul_double_with_CF :>
+        forall x y, decode (fst (snd (muldwf x y))) =~> (decode x * decode y) mod 2^n;
+      decode_snd_mul_double_with_CF :>
+        forall x y, decode (snd (snd (muldwf x y))) =~> (decode x * decode y) >> n
+    }.
+
   Class select_conditional := { selc : bool -> W -> W -> W }.
   Global Coercion selc : select_conditional >-> Funclass.
 
@@ -203,11 +285,15 @@ End InstructionGallery.
 
 Global Arguments load_immediate : clear implicits.
 Global Arguments shift_right_doubleword_immediate : clear implicits.
+Global Arguments shift_right_doubleword_immediate_with_CF : clear implicits.
 Global Arguments shift_left_immediate : clear implicits.
+Global Arguments shift_left_immediate_with_CF : clear implicits.
 Global Arguments shift_right_immediate : clear implicits.
+Global Arguments shift_right_immediate_with_CF : clear implicits.
 Global Arguments spread_left_immediate : clear implicits.
 Global Arguments mask_keep_low : clear implicits.
 Global Arguments bitwise_and : clear implicits.
+Global Arguments bitwise_and_with_CF : clear implicits.
 Global Arguments add_with_carry : clear implicits.
 Global Arguments sub_with_carry : clear implicits.
 Global Arguments multiply : clear implicits.
@@ -215,15 +301,20 @@ Global Arguments multiply_low_low : clear implicits.
 Global Arguments multiply_high_low : clear implicits.
 Global Arguments multiply_high_high : clear implicits.
 Global Arguments multiply_double : clear implicits.
+Global Arguments multiply_double_with_CF : clear implicits.
 Global Arguments select_conditional : clear implicits.
 Global Arguments add_modulo : clear implicits.
 Global Arguments ldi {_ _} _.
+Global Arguments shrdf {_ _} _ _ _.
 Global Arguments shrd {_ _} _ _ _.
 Global Arguments shl {_ _} _ _.
+Global Arguments shlf {_ _} _ _.
 Global Arguments shr {_ _} _ _.
+Global Arguments shrf {_ _} _ _.
 Global Arguments sprl {_ _} _ _.
 Global Arguments mkl {_ _} _ _.
 Global Arguments and {_ _} _ _.
+Global Arguments andf {_ _} _ _.
 Global Arguments adc {_ _} _ _ _.
 Global Arguments subc {_ _} _ _ _.
 Global Arguments mul {_ _} _ _.
@@ -231,17 +322,22 @@ Global Arguments mulhwll {_ _} _ _.
 Global Arguments mulhwhl {_ _} _ _.
 Global Arguments mulhwhh {_ _} _ _.
 Global Arguments muldw {_ _} _ _.
+Global Arguments muldwf {_ _} _ _.
 Global Arguments selc {_ _} _ _ _.
 Global Arguments addm {_ _} _ _ _.
 
 Global Arguments is_decode {_ _} _.
 Global Arguments is_load_immediate {_ _ _} _.
 Global Arguments is_shift_right_doubleword_immediate {_ _ _} _.
+Global Arguments is_shift_right_doubleword_immediate_with_CF {_ _ _} _.
 Global Arguments is_shift_left_immediate {_ _ _} _.
+Global Arguments is_shift_left_immediate_with_CF {_ _ _} _.
 Global Arguments is_shift_right_immediate {_ _ _} _.
+Global Arguments is_shift_right_immediate_with_CF {_ _ _} _.
 Global Arguments is_spread_left_immediate {_ _ _} _.
 Global Arguments is_mask_keep_low {_ _ _} _.
 Global Arguments is_bitwise_and {_ _ _} _.
+Global Arguments is_bitwise_and_with_CF {_ _ _} _.
 Global Arguments is_add_with_carry {_ _ _} _.
 Global Arguments is_sub_with_carry {_ _ _} _.
 Global Arguments is_mul {_ _ _} _.
@@ -249,6 +345,7 @@ Global Arguments is_mul_low_low {_ _ _} _ _.
 Global Arguments is_mul_high_low {_ _ _} _ _.
 Global Arguments is_mul_high_high {_ _ _} _ _.
 Global Arguments is_mul_double {_ _ _} _.
+Global Arguments is_mul_double_with_CF {_ _ _} _.
 Global Arguments is_select_conditional {_ _ _} _.
 Global Arguments is_add_modulo {_ _ _} _.
 
@@ -297,25 +394,25 @@ Module x86.
       W : Type (* [n]-bit word *);
       decode :> decoder n W;
       ldi :> load_immediate W;
-      shrd :> shift_right_doubleword_immediate W;
-      shl :> shift_left_immediate W;
-      shr :> shift_right_immediate W;
+      shrdf :> shift_right_doubleword_immediate_with_CF W;
+      shlf :> shift_left_immediate_with_CF W;
+      shrf :> shift_right_immediate_with_CF W;
       adc :> add_with_carry W;
       subc :> sub_with_carry W;
-      muldw :> multiply_double W;
-      and :> bitwise_and W
+      muldwf :> multiply_double_with_CF W;
+      andf :> bitwise_and_with_CF W
     }.
 
   Class arithmetic {n} (ops:instructions n) :=
     {
       decode_range :> is_decode decode;
       load_immediate :> is_load_immediate ldi;
-      shift_right_doubleword_immediate :> is_shift_right_doubleword_immediate shrd;
-      shift_left_immediate :> is_shift_left_immediate shl;
-      shift_right_immediate :> is_shift_right_immediate shr;
+      shift_right_doubleword_immediate_with_CF :> is_shift_right_doubleword_immediate_with_CF shrdf;
+      shift_left_immediate_with_CF :> is_shift_left_immediate_with_CF shlf;
+      shift_right_immediate_with_CF :> is_shift_right_immediate_with_CF shrf;
       add_with_carry :> is_add_with_carry adc;
       sub_with_carry :> is_sub_with_carry subc;
-      multiply_double :> is_mul_double muldw;
-      bitwise_and :> is_bitwise_and and
+      multiply_double_with_CF :> is_mul_double_with_CF muldwf;
+      bitwise_and_with_CF :> is_bitwise_and_with_CF andf
     }.
 End x86.