diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
index 5849e9547a..fd58e85dcf 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -4351,6 +4351,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, [lo as dst; hi; 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@(shl s@(lo, cnt), shr 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));
diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
index d8f6ef024e..73fc8a1935 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -329,6 +329,22 @@ 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 lo; hi; 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 v := Z.land l_shifted (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 lv <? 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 lv (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;