implicitly increment PC for uninterpreted instrs

GaloisInc · Nov 1, 2023 · 694a427 · 694a427
1 parent f3004d6
commit 694a427
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs b/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
@@ -693,6 +693,10 @@ a32InstructionMatcher (ARMDis.Instruction opc operands) =
             G.finishWithTerminator MCB.FetchAndExecute
       _ | isUninterpretedA32Opcode opc -> Just $ do
             G.addStmt (MC.ExecArchStmt (UninterpretedA32Opcode opc operands))
+            let pc = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_PC")
+            pc_orig <- G.getRegVal pc
+            pc_next <- G.addExpr (G.AppExpr (MC.BVAdd NR.knownNat pc_orig (MC.BVValue NR.knownNat 4)))
+            G.setRegVal pc pc_next
         | otherwise -> Nothing
 
 -- | This is a coarse heuristic to treat any instruction beginning with 'V' as a
@@ -761,6 +765,10 @@ t32InstructionMatcher (ThumbDis.Instruction opc operands) =
 
       _ | isUninterpretedT32Opcode opc -> Just $ do
             G.addStmt (MC.ExecArchStmt (UninterpretedT32Opcode opc operands))
+            let pc = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_PC")
+            pc_orig <- G.getRegVal pc
+            pc_next <- G.addExpr (G.AppExpr (MC.BVAdd NR.knownNat pc_orig (MC.BVValue NR.knownNat 4)))
+            G.setRegVal pc pc_next
         | otherwise -> Nothing
 
 instance MSS.SimplifierExtension ARM.AArch32 where