From a63e54ca057d61c4ffa9d1d1f240bb95e432fbc7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Oct 2016 20:10:51 -0400 Subject: Add some more instructions --- src/BoundedArithmetic/Interface.v | 32 +++++++++++++++-- src/BoundedArithmetic/StripCF.v | 74 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 104 insertions(+), 2 deletions(-) create mode 100644 src/BoundedArithmetic/StripCF.v (limited to 'src/BoundedArithmetic') diff --git a/src/BoundedArithmetic/Interface.v b/src/BoundedArithmetic/Interface.v index 35770b2cd..5988108a6 100644 --- a/src/BoundedArithmetic/Interface.v +++ b/src/BoundedArithmetic/Interface.v @@ -196,6 +196,28 @@ Section InstructionGallery. fst_bitwise_and_with_CF :> forall x y, fst (andf x y) =~> false }. + Class bitwise_or := { or : W -> W -> W }. + Global Coercion or : bitwise_or >-> Funclass. + + Class is_bitwise_or (or : bitwise_or) := + { + decode_bitwise_or :> forall x y, decode (or x y) <~=~> Z.lor (decode x) (decode y) + }. + + (** Quoting http://www.felixcloutier.com/x86/OR.html: + + The OF or CF flags are cleared; the SF, ZF, or PF flags are set + according to the result. The state of the AF flag is + undefined. *) + Class bitwise_or_with_CF := { orf : W -> W -> bool * W }. + Global Coercion orf : bitwise_or_with_CF >-> Funclass. + + Class is_bitwise_or_with_CF (orf : bitwise_or_with_CF) := + { + decode_snd_bitwise_or_with_CF :> forall x y, decode (snd (orf x y)) <~=~> Z.lor (decode x) (decode y); + fst_bitwise_or_with_CF :> forall x y, fst (orf x y) =~> false + }. + Local Notation bit b := (if b then 1 else 0). Class add_with_carry := { adc : W -> W -> bool -> bool * W }. @@ -294,6 +316,8 @@ 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 bitwise_or : clear implicits. +Global Arguments bitwise_or_with_CF : clear implicits. Global Arguments add_with_carry : clear implicits. Global Arguments sub_with_carry : clear implicits. Global Arguments multiply : clear implicits. @@ -315,6 +339,8 @@ Global Arguments sprl {_ _} _ _. Global Arguments mkl {_ _} _ _. Global Arguments and {_ _} _ _. Global Arguments andf {_ _} _ _. +Global Arguments or {_ _} _ _. +Global Arguments orf {_ _} _ _. Global Arguments adc {_ _} _ _ _. Global Arguments subc {_ _} _ _ _. Global Arguments mul {_ _} _ _. @@ -338,6 +364,8 @@ 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_bitwise_or {_ _ _} _. +Global Arguments is_bitwise_or_with_CF {_ _ _} _. Global Arguments is_add_with_carry {_ _ _} _. Global Arguments is_sub_with_carry {_ _ _} _. Global Arguments is_mul {_ _ _} _. @@ -400,7 +428,7 @@ Module x86. adc :> add_with_carry W; subc :> sub_with_carry W; muldwf :> multiply_double_with_CF W; - andf :> bitwise_and_with_CF W + selc :> select_conditional W }. Class arithmetic {n} (ops:instructions n) := @@ -413,6 +441,6 @@ Module x86. add_with_carry :> is_add_with_carry adc; sub_with_carry :> is_sub_with_carry subc; multiply_double_with_CF :> is_mul_double_with_CF muldwf; - bitwise_and_with_CF :> is_bitwise_and_with_CF andf + select_conditional :> is_select_conditional selc }. End x86. diff --git a/src/BoundedArithmetic/StripCF.v b/src/BoundedArithmetic/StripCF.v new file mode 100644 index 000000000..f44b1b7f7 --- /dev/null +++ b/src/BoundedArithmetic/StripCF.v @@ -0,0 +1,74 @@ +(** * Strip CF for Interface for bounded arithmetic *) +Require Import Coq.ZArith.ZArith. +Require Import Crypto.BoundedArithmetic.Interface. + +Local Open Scope type_scope. +Local Open Scope Z_scope. + +Section strip_CF. + Context (n : Z) (* bit-width of width of [W] *) + {W : Type} (* bounded type, [W] for word *) + (Wdecoder : decoder n W). + Local Notation imm := Z (only parsing). (* immediate (compile-time) argument *) + + Global Instance shift_right_doubleword_immediate_strip_CF + {shrdf : shift_right_doubleword_immediate_with_CF W} + : shift_right_doubleword_immediate W + := { shrd x y z := snd (shrdf x y z) }. + Global Instance is_shift_right_doubleword_immediate_strip_CF + {shrdf : shift_right_doubleword_immediate_with_CF W} + {shift_right_doubleword_immediate_with_CF : is_shift_right_doubleword_immediate_with_CF shrdf} + : is_shift_right_doubleword_immediate shift_right_doubleword_immediate_strip_CF + := shift_right_doubleword_immediate_with_CF. + + Global Instance shift_left_immediate_strip_CF + {shlf : shift_left_immediate_with_CF W} + : shift_left_immediate W + := { shl x y := snd (shlf x y) }. + Global Instance is_shift_left_immediate_strip_CF + {shlf : shift_left_immediate_with_CF W} + {shift_left_immediate_with_CF : is_shift_left_immediate_with_CF shlf} + : is_shift_left_immediate shift_left_immediate_strip_CF + := shift_left_immediate_with_CF. + + Global Instance shift_right_immediate_strip_CF + {shrf : shift_right_immediate_with_CF W} + : shift_right_immediate W + := { shr x y := snd (shrf x y) }. + Global Instance is_shift_right_immediate_strip_CF + {shrf : shift_right_immediate_with_CF W} + {shift_right_immediate_with_CF : is_shift_right_immediate_with_CF shrf} + : is_shift_right_immediate shift_right_immediate_strip_CF + := shift_right_immediate_with_CF. + + Global Instance bitwise_and_strip_CF + {andf : bitwise_and_with_CF W} + : bitwise_and W + := { and x y := snd (andf x y) }. + Global Instance is_bitwise_and_strip_CF + {andf : bitwise_and_with_CF W} + {bitwise_and_with_CF : is_bitwise_and_with_CF andf} + : is_bitwise_and bitwise_and_strip_CF + := { decode_bitwise_and := @decode_snd_bitwise_and_with_CF _ _ _ _ bitwise_and_with_CF }. + + Global Instance bitwise_or_strip_CF + {orf : bitwise_or_with_CF W} + : bitwise_or W + := { or x y := snd (orf x y) }. + Global Instance is_bitwise_or_strip_CF + {orf : bitwise_or_with_CF W} + {bitwise_or_with_CF : is_bitwise_or_with_CF orf} + : is_bitwise_or bitwise_or_strip_CF + := { decode_bitwise_or := @decode_snd_bitwise_or_with_CF _ _ _ _ bitwise_or_with_CF }. + + Global Instance multiply_double_strip_CF + {muldwf : multiply_double_with_CF W} + : multiply_double W + := { muldw x y := snd (muldwf x y) }. + Global Instance is_mul_double_strip_CF + {muldwf : multiply_double_with_CF W} + {multiply_double_with_CF : is_mul_double_with_CF muldwf} + : is_mul_double multiply_double_strip_CF + := { decode_fst_mul_double := @decode_fst_mul_double_with_CF _ _ _ _ multiply_double_with_CF; + decode_snd_mul_double := @decode_snd_mul_double_with_CF _ _ _ _ multiply_double_with_CF}. +End strip_CF. -- cgit v1.2.3