Skip to content

Commit 465a84e

Browse files
robdockinsrobdockins
committed
Update with changes flowing from GaloicInc/crucible#945.
This mostly deals with the splitting of the old `sym` type into two: one for dealing with expression creation, and a new simulator backend type for dealing with control-flow and assertions.
1 parent 2845d6f commit 465a84e

File tree

22 files changed

+535
-462
lines changed

22 files changed

+535
-462
lines changed

‎macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs

+26-26
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
{-# LANGUAGE GADTs #-}
2+
{-# LANGUAGE RankNTypes #-}
23
{-# LANGUAGE StandaloneDeriving #-}
34
module Data.Macaw.AArch32.Symbolic.Functions (
45
SymFuns
@@ -82,33 +83,33 @@ funcSemantics :: (CB.IsSymInterface sym, MS.ToCrucibleType mt ~ t)
8283
-> IO (CS.RegValue sym t, S sym rtp bs r ctx)
8384
funcSemantics sfns fn st0 =
8485
case fn of
85-
MAA.SDiv _rep lhs rhs -> withSym st0 $ \sym -> do
86-
lhs' <- toValBV sym lhs
87-
rhs' <- toValBV sym rhs
86+
MAA.SDiv _rep lhs rhs -> withBackend st0 $ \sym bak -> do
87+
lhs' <- toValBV bak lhs
88+
rhs' <- toValBV bak rhs
8889
-- NOTE: We are applying division directly here without checking the divisor for zero.
8990
--
9091
-- The ARM semantics explicitly check this and have different behaviors
9192
-- depending on what CPU flags are set; this operation is never called
9293
-- with a divisor of zero. We could add an assertion to that effect here,
9394
-- but it might be difficult to prove.
9495
LL.llvmPointer_bv sym =<< WI.bvSdiv sym lhs' rhs'
95-
MAA.UDiv _rep lhs rhs -> withSym st0 $ \sym -> do
96-
lhs' <- toValBV sym lhs
97-
rhs' <- toValBV sym rhs
96+
MAA.UDiv _rep lhs rhs -> withBackend st0 $ \sym bak -> do
97+
lhs' <- toValBV bak lhs
98+
rhs' <- toValBV bak rhs
9899
-- NOTE: See the note in SDiv
99100
LL.llvmPointer_bv sym =<< WI.bvUdiv sym lhs' rhs'
100-
MAA.URem _rep lhs rhs -> withSym st0 $ \sym -> do
101-
lhs' <- toValBV sym lhs
102-
rhs' <- toValBV sym rhs
101+
MAA.URem _rep lhs rhs -> withBackend st0 $ \sym bak -> do
102+
lhs' <- toValBV bak lhs
103+
rhs' <- toValBV bak rhs
103104
-- NOTE: See the note in SDiv
104105
LL.llvmPointer_bv sym =<< WI.bvUrem sym lhs' rhs'
105-
MAA.SRem _rep lhs rhs -> withSym st0 $ \sym -> do
106-
lhs' <- toValBV sym lhs
107-
rhs' <- toValBV sym rhs
106+
MAA.SRem _rep lhs rhs -> withBackend st0 $ \sym bak -> do
107+
lhs' <- toValBV bak lhs
108+
rhs' <- toValBV bak rhs
108109
-- NOTE: See the note in SDiv
109110
LL.llvmPointer_bv sym =<< WI.bvSrem sym lhs' rhs'
110-
MAA.UnsignedRSqrtEstimate _rep v -> withSym st0 $ \sym -> do
111-
v' <- toValBV sym v
111+
MAA.UnsignedRSqrtEstimate _rep v -> withBackend st0 $ \sym bak -> do
112+
v' <- toValBV bak v
112113
let args = Ctx.empty Ctx.:> v'
113114
res <- lookupApplySymFun sym sfns "unsignedRSqrtEstimate" CT.knownRepr args CT.knownRepr
114115
LL.llvmPointer_bv sym res
@@ -139,22 +140,21 @@ funcSemantics sfns fn st0 =
139140
MAA.ARMSyscall {} ->
140141
AP.panic AP.AArch32 "funcSemantics" ["The ARM syscall primitive should be eliminated and replaced by a handle lookup"]
141142

142-
withSym :: (CB.IsSymInterface sym)
143-
=> S sym rtp bs r ctx
144-
-> (sym -> IO a)
145-
-> IO (a, S sym rtp bs r ctx)
146-
withSym s action = do
147-
let sym = s ^. CSET.stateSymInterface
148-
val <- action sym
149-
return (val, s)
150-
143+
withBackend ::
144+
S sym rtp bs r ctx ->
145+
(forall bak. CB.IsSymBackend sym bak => sym -> bak -> IO a) ->
146+
IO (a, S sym rtp bs r ctx)
147+
withBackend s action = do
148+
CSET.withBackend (s^.CSET.stateContext) $ \bak ->
149+
do val <- action (CB.backendGetSym bak) bak
150+
return (val, s)
151151

152152
-- | Assert that the wrapped value is a bitvector
153-
toValBV :: (CB.IsSymInterface sym)
154-
=> sym
153+
toValBV :: (CB.IsSymBackend sym bak)
154+
=> bak
155155
-> AA.AtomWrapper (CS.RegEntry sym) (MT.BVType w)
156156
-> IO (CS.RegValue sym (CT.BVType w))
157-
toValBV sym (AA.AtomWrapper x) = LL.projectLLVM_bv sym (CS.regValue x)
157+
toValBV bak (AA.AtomWrapper x) = LL.projectLLVM_bv bak (CS.regValue x)
158158

159159
-- | Apply an uninterpreted function to the provided arguments
160160
--

‎macaw-aarch32-symbolic/tests/Main.hs

+7-3
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,7 @@ import qualified Data.Macaw.Discovery as M
3737
import qualified Data.Macaw.Symbolic as MS
3838
import qualified Data.Macaw.Symbolic.Testing as MST
3939
import qualified What4.Config as WC
40+
import qualified What4.Expr.Builder as WEB
4041
import qualified What4.Interface as WI
4142
import qualified What4.ProblemFeatures as WPF
4243
import qualified What4.Solver as WS
@@ -113,6 +114,8 @@ mkSymExTest expected exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOpti
113114
symExTestSized expected exePath saveSMT saveMacaw step ehi MA.arm_linux_info
114115
Elf.ELFCLASS64 -> TTH.assertFailure "64 bit ARM is not supported"
115116

117+
data MacawAarch32TestData t = MacawAarch32TestData
118+
116119
symExTestSized :: MST.SimulationResult
117120
-> FilePath
118121
-> SaveSMT
@@ -128,19 +131,20 @@ symExTestSized expected exePath saveSMT saveMacaw step ehi archInfo = do
128131
step ("Testing " ++ BS8.unpack name ++ " at " ++ show (M.discoveredFunAddr dfi))
129132
writeMacawIR saveMacaw (BS8.unpack name) dfi
130133
Some (gen :: PN.NonceGenerator IO t) <- PN.newIONonceGenerator
131-
CBO.withYicesOnlineBackend CBO.FloatRealRepr gen CBO.NoUnsatFeatures WPF.noFeatures $ \sym -> do
134+
sym <- WEB.newExprBuilder WEB.FloatRealRepr MacawAarch32TestData gen
135+
CBO.withYicesOnlineBackend sym CBO.NoUnsatFeatures WPF.noFeatures $ \bak -> do
132136
-- We are using the z3 backend to discharge proof obligations, so
133137
-- we need to add its options to the backend configuration
134138
let solver = WS.z3Adapter
135139
let backendConf = WI.getConfiguration sym
136140
WC.extendConfig (WS.solver_adapter_config_options solver) backendConf
137141

138-
execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend sym)
142+
execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend bak)
139143
let Just archVals = MS.archVals (Proxy @MA.ARM) Nothing
140144
let extract = armResultExtractor archVals
141145
logger <- makeGoalLogger saveSMT solver name exePath
142146
let ?memOpts = LLVM.defaultMemOptions
143-
simRes <- MST.simulateAndVerify solver logger sym execFeatures archInfo archVals mem extract dfi
147+
simRes <- MST.simulateAndVerify solver logger bak execFeatures archInfo archVals mem extract dfi
144148
TTH.assertEqual "AssertionResult" expected simRes
145149

146150
writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()

‎macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs

+3-3
Original file line numberDiff line numberDiff line change
@@ -19,15 +19,15 @@ import Data.Macaw.ARM.Arch ( a32InstructionMatcher )
1919
import Data.Macaw.ARM.Semantics.TH ( armAppEvaluator, armNonceAppEval, loadSemantics, armTranslateType )
2020
import qualified Data.Macaw.CFG as MC
2121
import Data.Macaw.SemMC.Generator ( Generator )
22-
import Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction )
22+
import Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction, MacawSemMC(..) )
2323
import qualified Data.Macaw.Types as MT
2424
import Data.Parameterized.Classes ( showF )
2525
import qualified Data.Parameterized.Map as MapF
2626
import qualified Data.Parameterized.Nonce as PN
2727
import Data.Parameterized.Some ( Some(..), mapSome )
2828
import Data.Proxy ( Proxy(..) )
2929
import Dismantle.ARM.A32 -- must be present to supply definitions for genExecInstruction output
30-
import qualified Lang.Crucible.Backend.Simple as CBS
30+
import qualified What4.Expr.Builder as WEB
3131
import qualified Language.Haskell.TH as TH
3232
import qualified SemMC.Architecture.AArch32 as ARMSem
3333
import SemMC.Architecture.ARM.Opcodes ( ASLSemantics(..), allA32OpcodeInfo )
@@ -40,7 +40,7 @@ execInstruction :: MC.Value ARMSem.AArch32 ids (MT.BVType 32)
4040
-> Maybe (Generator ARMSem.AArch32 ids s ())
4141
execInstruction =
4242
$(do Some ng <- TH.runIO PN.newIONonceGenerator
43-
sym <- TH.runIO (CBS.newSimpleBackend CBS.FloatIEEERepr ng)
43+
sym <- TH.runIO (WEB.newExprBuilder WEB.FloatIEEERepr MacawSemMC ng)
4444
sem <- TH.runIO (loadSemantics sym)
4545
let
4646
aconv :: (MapF.Pair (Opcode Operand) x)

‎macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs

+2-2
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ import qualified Data.Parameterized.Context as Ctx
4646
import qualified Data.Parameterized.TraversableFC as FC
4747
import Data.Parameterized.NatRepr
4848
import GHC.TypeLits as TL
49-
import qualified Lang.Crucible.Backend.Simple as CBS
49+
import qualified What4.Expr.Builder as WEB
5050
import Language.Haskell.TH
5151
import qualified SemMC.Architecture.AArch32 as ARM
5252
import qualified SemMC.Architecture.ARM.Opcodes as ARM
@@ -55,7 +55,7 @@ import qualified What4.Expr.Builder as WB
5555

5656
import qualified Language.ASL.Globals as ASL
5757

58-
loadSemantics :: CBS.SimpleBackend t fs -> IO (ARM.ASLSemantics (CBS.SimpleBackend t fs))
58+
loadSemantics :: WEB.ExprBuilder t st fs -> IO (ARM.ASLSemantics (WEB.ExprBuilder t st fs))
5959
loadSemantics sym = ARM.loadSemantics sym (ARM.ASLSemanticsOpts { ARM.aslOptTrimRegs = True})
6060

6161
-- n.b. although MacawQ is a monad and therefore has a fail

‎macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs

+3-3
Original file line numberDiff line numberDiff line change
@@ -19,15 +19,15 @@ import Data.Macaw.ARM.Arch ( t32InstructionMatcher )
1919
import Data.Macaw.ARM.Semantics.TH ( armAppEvaluator, armNonceAppEval, loadSemantics, armTranslateType )
2020
import qualified Data.Macaw.CFG as MC
2121
import Data.Macaw.SemMC.Generator ( Generator )
22-
import Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction )
22+
import Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction, MacawSemMC(..) )
2323
import qualified Data.Macaw.Types as MT
2424
import Data.Parameterized.Classes ( showF )
2525
import qualified Data.Parameterized.Map as MapF
2626
import qualified Data.Parameterized.Nonce as PN
2727
import Data.Parameterized.Some ( Some(..) )
2828
import Data.Proxy ( Proxy(..) )
2929
import Dismantle.ARM.T32 -- as ThumbDis -- must be present to supply definitions for genExecInstruction output
30-
import qualified Lang.Crucible.Backend.Simple as CBS
30+
import qualified What4.Expr.Builder as WEB
3131
import qualified Language.Haskell.TH as TH
3232
import qualified SemMC.Architecture.AArch32 as ARMSem
3333
import SemMC.Architecture.ARM.Opcodes ( ASLSemantics(..), allT32OpcodeInfo )
@@ -39,7 +39,7 @@ execInstruction :: MC.Value ARMSem.AArch32 ids (MT.BVType 32)
3939
-> Maybe (Generator ARMSem.AArch32 ids s ())
4040
execInstruction =
4141
$(do Some ng <- TH.runIO PN.newIONonceGenerator
42-
sym <- TH.runIO (CBS.newSimpleBackend CBS.FloatIEEERepr ng)
42+
sym <- TH.runIO (WEB.newExprBuilder WEB.FloatIEEERepr MacawSemMC ng)
4343
sem <- TH.runIO (loadSemantics sym)
4444
let
4545
aconv :: (MapF.Pair (Opcode Operand) x)

0 commit comments

Comments
 (0)