Add support for movabs

JasonGross · Mar 6, 2025 · 91f67d4 · 91f67d4
1 parent efc121c
commit 91f67d4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
@@ -4199,7 +4199,7 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
   let s : OperationSize := s in
   let resize_reg r := some_or (fun _ => reg_of_index_and_shift_and_bitcount_opt (reg_index r, 0%N (* offset *), s)) (fun _ => error.unimplemented_instruction instr) in
   match instr.(Syntax.op), instr.(args) with
-  | (mov | movzx), [dst; src] => (* Note: unbundle when switching from N to Z *)
+  | (mov | movzx | movabs), [dst; src] => (* Note: unbundle when switching from N to Z *)
     v <- GetOperand src;
     SetOperand dst v
   | xchg, [a; b] => (* Note: unbundle when switching from N to Z *)

diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
@@ -165,7 +165,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
   let resize_reg r := reg_of_index_and_shift_and_bitcount_opt (reg_index r, 0%N (* offset *), s) in
   match instr.(prefix) with None =>
   match instr.(op), instr.(args) with
-  | (mov | movzx), [dst; src] => (* Note: unbundle when switching from N to Z *)
+  | (mov | movzx | movabs), [dst; src] => (* Note: unbundle when switching from N to Z *)
     v <- DenoteOperand sa s st src;
     SetOperand sa s st dst v
   | xchg, [a; b] => (* Flags Affected: None *)