Merge pull request #2037 from JasonGross/shld

Add support for shld

Author: JasonGross

src/Assembly/Symbolic.v

@@ -4335,6 +4335,12 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
     v <- Symeval (or s@(shr s@(lo, cnt), shl s@(hi, cnt')));
     _ <- SetOperand dst v;
     HavocFlags
+  | shld, [hi as dst; lo; cnt] =>
+    let cnt := andZ@(cnt, (PreApp (const (Z.of_N s-1)%Z) nil)) in
+    let cnt' := addZ@(Z.of_N s, PreApp negZ [cnt]) in
+    v <- Symeval (or s@(shr s@(lo, cnt'), shl s@(hi, cnt)));
+    _ <- SetOperand dst v;
+    HavocFlags
   | inc, [dst] =>
     v <- Symeval (add s@(dst, PreARG 1%Z));
     o <- Symeval (addoverflow s@(dst, PreARG 1%Z));

src/Assembly/WithBedrock/Semantics.v

@@ -327,6 +327,23 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
       let st := if cnt =? 1 then SetFlag st OF signchange else st in
       let st := SetFlag st CF (Z.testbit l (cnt-1)) in
       Some (HavocFlag st AF)
+  | shld, [dst as hi; lo; cnt] =>
+    lv <- DenoteOperand sa s st lo;
+    hv <- DenoteOperand sa s st hi;
+    cnt <- DenoteOperand sa s st cnt;
+    let l := Z.lor lv (Z.shiftl hv (Z.of_N s)) in
+    let l_shifted := Z.shiftl l (Z.land cnt (Z.of_N s-1)) in
+    let l_shifted_hi := Z.shiftr l_shifted (Z.of_N s) in
+    let v := Z.land l_shifted_hi (Z.ones (Z.of_N s)) in
+    st <- SetOperand sa s st dst v;
+    if cnt =? 0 then Some st else
+    if Z.of_N s <? cnt then Some (HavocFlags st) else
+      let st := HavocFlagsFromResult s st l in
+      let signchange := xorb (signed s hv <? 0)%Z (signed s v <? 0)%Z in
+      (* Note: IA-32 SDM does not make it clear what sign change is in question *)
+      let st := if cnt =? 1 then SetFlag st OF signchange else st in
+      let st := SetFlag st CF (Z.testbit hv (Z.of_N s - cnt)) in
+      Some (HavocFlag st AF)
   | (and | xor | or) as opc, [dst; src] =>
     let f := match opc with and => Z.land | xor => Z.lxor | _ => Z.lor end in
     v1 <- DenoteOperand sa s st dst;

src/Assembly/WithBedrock/SymbolicProofs.v

@@ -3,6 +3,7 @@ From Coq Require Import Lia.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.
 From Coq Require Import NArith.
 From Coq Require Import ZArith.
+Require Import Crypto.Util.ZUtil.Testbit.
 Require Import Crypto.AbstractInterpretation.ZRange.
 Require Import Crypto.Util.ErrorT.
 Import Coq.Lists.List. (* [map] is [List.map] not [ErrorT.map] *)
@@ -1343,6 +1344,18 @@ Proof using Type.
     3: enough (0 <= Z.land v3 (Z.of_N n - 1)) by lia; eapply Z.land_nonneg; right.
     1,2,3:pose_operation_size_cases; intuition (subst; cbn; clear; lia). }
 
+  Unshelve. all : match goal with H : context[Syntax.shld] |- _ => idtac | _ => shelve end; shelve_unifiable.
+  { repeat match goal with H : ?x = Some _, H' : ?x = Some _ |- _ => rewrite H' in *; Option.inversion_option end.
+    progress subst.
+    replace (Z.land (Z.of_N n) (Z.ones (Z.of_N n))) with (Z.of_N n)
+      by (rewrite Z.land_ones, Z.mod_small; try split; try lia; apply Zpow_facts.Zpower2_lt_lin; lia).
+    assert (0 <= Z.of_N n - 1) by (pose_operation_size_cases; intuition (subst; cbn; clear; lia)).
+    rewrite <- !Z.shiftl_opp_r.
+    rewrite !Z.shiftl_lor.
+    rewrite <- !Z.land_lor_distr_l, <- Z.land_assoc, Z.land_diag.
+    rewrite !Z.shiftl_shiftl by (try apply Z.land_nonneg; lia).
+    f_equal; f_equal; f_equal; try lia. }
+
   Unshelve. all : match goal with H : context[Syntax.shlx] |- _ => idtac | _ => shelve end; shelve_unifiable.
   { rewrite <- Z.land_assoc.
     f_equal; f_equal; [].