From 72f2c6291869d847abb018ab3e71e7a8f8edacf4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Oct 2016 18:05:43 -0400 Subject: Add instructions with carry flags --- src/BoundedArithmetic/Interface.v | 117 ++++++++++++++++++++++++++++++++++---- 1 file changed, 107 insertions(+), 10 deletions(-) (limited to 'src/BoundedArithmetic') 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. -- cgit v1.2.3