Add support for nop (#2034)

mit-plv · Mar 7, 2025 · cd21d34 · cd21d34
1 parent efc121c
commit cd21d34
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
@@ -4386,6 +4386,9 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
        rsp' <- Symeval (s:=stack_addr_size) (add stack_addr_size@(rsp', PreARG ((Z.of_N s/8)%Z)));
        _    <- SetOperand rsp rsp';
                SetOperand dst v
+
+  | nop, [] => ret tt
+
   | _, _ => err (error.unimplemented_instruction instr)
  end
   | Some prefix => err (error.unimplemented_prefix instr) end

diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v
@@ -369,6 +369,8 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
        st   <- SetOperand stack_addr_size s st rsp rsp';
                SetOperand sa s st dst v
 
+  | nop, [] => Some st
+
   | ret, _ => None (* not sure what to do with this ret, maybe exlude it? *)
 
   | adc, _