From 4625ea21c2cf3c4c38bd8399d56627e35bc15456 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 4 Jan 2021 13:57:45 -0500 Subject: [PATCH 01/22] Initial support for aarch32 --- .gitmodules | 15 + cabal.project | 11 + deps/arm-asl-parser | 1 + deps/asl-translator | 1 + deps/dismantle | 1 + deps/macaw | 2 +- deps/semmc | 1 + deps/what4-serialize | 1 + saw-script.cabal | 4 + src/SAWScript/Crucible/LLVM/AArch32.hs | 1032 ++++++++++++++++++++++++ src/SAWScript/Interpreter.hs | 16 + 11 files changed, 1084 insertions(+), 1 deletion(-) create mode 160000 deps/arm-asl-parser create mode 160000 deps/asl-translator create mode 160000 deps/dismantle create mode 160000 deps/semmc create mode 160000 deps/what4-serialize create mode 100644 src/SAWScript/Crucible/LLVM/AArch32.hs diff --git a/.gitmodules b/.gitmodules index f417eb4edb..f74ac3ad51 100644 --- a/.gitmodules +++ b/.gitmodules @@ -52,3 +52,18 @@ [submodule "deps/argo"] path = deps/argo url = https://github.com/galoisinc/argo +[submodule "deps/what4-serialize"] + path = deps/what4-serialize + url = https://github.com/GaloisInc/what4-serialize +[submodule "deps/asl-translator"] + path = deps/asl-translator + url = https://github.com/GaloisInc/asl-translator +[submodule "deps/arm-asl-parser"] + path = deps/arm-asl-parser + url = https://github.com/GaloisInc/arm-asl-parser +[submodule "deps/dismantle"] + path = deps/dismantle + url = https://github.com/travitch/dismantle +[submodule "deps/semmc"] + path = deps/semmc + url = https://github.com/GaloisInc/semmc diff --git a/cabal.project b/cabal.project index 9611b571f0..cea83d12ad 100644 --- a/cabal.project +++ b/cabal.project @@ -24,10 +24,21 @@ packages: deps/parameterized-utils deps/flexdis86 deps/flexdis86/binary-symbols + deps/what4-serialize + deps/asl-translator + deps/arm-asl-parser + deps/dismantle/dismantle-tablegen + deps/dismantle/dismantle-arm-xml + deps/semmc/semmc + deps/semmc/semmc-synthesis + deps/semmc/semmc-aarch32 deps/macaw/base deps/macaw/symbolic deps/macaw/x86 deps/macaw/x86_symbolic + deps/macaw/macaw-semmc + deps/macaw/macaw-aarch32 + deps/macaw/macaw-aarch32-symbolic deps/elf-edit deps/dwarf deps/argo/argo diff --git a/deps/arm-asl-parser b/deps/arm-asl-parser new file mode 160000 index 0000000000..afbeff2db4 --- /dev/null +++ b/deps/arm-asl-parser @@ -0,0 +1 @@ +Subproject commit afbeff2db4781e138bb8c920d803b7e7a88383b7 diff --git a/deps/asl-translator b/deps/asl-translator new file mode 160000 index 0000000000..943cf7d724 --- /dev/null +++ b/deps/asl-translator @@ -0,0 +1 @@ +Subproject commit 943cf7d724b15c6ae4b650061f96c8bf0b63344a diff --git a/deps/dismantle b/deps/dismantle new file mode 160000 index 0000000000..1c2e7892c6 --- /dev/null +++ b/deps/dismantle @@ -0,0 +1 @@ +Subproject commit 1c2e7892c6edc514cef94efa68717c7a7505140a diff --git a/deps/macaw b/deps/macaw index 7761a6f6e1..12ce4d05d8 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 7761a6f6e1348e6479b2ad272ad47e59fb5a8fd7 +Subproject commit 12ce4d05d81d21854fd68aba33e05c9ca5e6eb96 diff --git a/deps/semmc b/deps/semmc new file mode 160000 index 0000000000..a60ace5ab6 --- /dev/null +++ b/deps/semmc @@ -0,0 +1 @@ +Subproject commit a60ace5ab6036dcb0c63aec0dddd2324b288ef9c diff --git a/deps/what4-serialize b/deps/what4-serialize new file mode 160000 index 0000000000..1266de365f --- /dev/null +++ b/deps/what4-serialize @@ -0,0 +1 @@ +Subproject commit 1266de365f6fd094fd7456311a2072cb1ef651ed diff --git a/saw-script.cabal b/saw-script.cabal index b892c19b47..ea2692ce93 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -91,9 +91,12 @@ library , GraphSCC , macaw-base , macaw-x86 + , macaw-aarch32 , macaw-symbolic , macaw-x86-symbolic + , macaw-aarch32-symbolic , flexdis86 + , asl-translator , elf-edit , reflection , aeson @@ -155,6 +158,7 @@ library SAWScript.Crucible.LLVM.Skeleton SAWScript.Crucible.LLVM.Skeleton.Builtins SAWScript.Crucible.LLVM.X86 + SAWScript.Crucible.LLVM.AArch32 SAWScript.Crucible.JVM.Builtins SAWScript.Crucible.JVM.BuiltinsJVM diff --git a/src/SAWScript/Crucible/LLVM/AArch32.hs b/src/SAWScript/Crucible/LLVM/AArch32.hs new file mode 100644 index 0000000000..8eb00e7ff1 --- /dev/null +++ b/src/SAWScript/Crucible/LLVM/AArch32.hs @@ -0,0 +1,1032 @@ +{- | +Module : SAWScript.Crucible.LLVM.AArch32 +Description : Implements a SAWScript primitive for verifying aarch32 functions + against LLVM specifications. +Maintainer : sbreese +Stability : provisional +-} + +{-# Language OverloadedStrings #-} +{-# Language FlexibleContexts #-} +{-# Language ScopedTypeVariables #-} +{-# Language TypeOperators #-} +{-# Language PatternSynonyms #-} +{-# Language LambdaCase #-} +{-# Language MultiWayIf #-} +{-# Language TupleSections #-} +{-# Language ImplicitParams #-} +{-# Language TypeApplications #-} +{-# Language GADTs #-} +{-# Language RankNTypes #-} +{-# Language DataKinds #-} +{-# Language ConstraintKinds #-} +{-# Language GeneralizedNewtypeDeriving #-} +{-# Language TemplateHaskell #-} + +module SAWScript.Crucible.LLVM.AArch32 + ( llvm_verify_aarch32 + ) where + +import Control.Lens.TH (makeLenses) + +import GHC.Natural (Natural) + +import System.IO (stdout) +import Control.Exception (Exception(..), throw) +import Control.Lens (view, use, toListOf, folded, (&), (^.), (.~), (%~), (.=)) +import Control.Applicative ((<|>)) +import Control.Monad.State +import Control.Monad.Catch (MonadThrow) + +import qualified Data.BitVector.Sized as BV +import Data.Foldable (foldlM) +import qualified Data.List.NonEmpty as NE +import qualified Data.Vector as Vector +import qualified Data.Text as Text +import Data.Text.Encoding (decodeUtf8, encodeUtf8) +import Data.ByteString (ByteString) +import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BSC +import qualified Data.Set as Set +import qualified Data.Map as Map +import Data.Map (Map) +import Data.Maybe + +import qualified Text.LLVM.AST as LLVM + +import Data.Parameterized.Some +import Data.Parameterized.NatRepr +import Data.Parameterized.Context hiding (view) +import Data.Parameterized.Nonce + +import Verifier.SAW.FiniteValue +import Verifier.SAW.SharedTerm +import Verifier.SAW.TypedTerm +import Verifier.SAW.Recognizer (asBool) + +import SAWScript.Proof +import SAWScript.Prover.SolverStats +import SAWScript.TopLevel +import SAWScript.Value +import SAWScript.Options + +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import qualified SAWScript.Crucible.Common.Override as O +import qualified SAWScript.Crucible.Common.Setup.Type as Setup + +import SAWScript.Crucible.LLVM.Builtins +import SAWScript.Crucible.LLVM.MethodSpecIR +import SAWScript.Crucible.LLVM.ResolveSetupValue +import qualified SAWScript.Crucible.LLVM.Override as LO + +import qualified What4.Expr as W4 +import qualified What4.FunctionName as W4 +import qualified What4.Interface as W4 +import qualified What4.LabeledPred as W4 +import qualified What4.ProgramLoc as W4 +import qualified What4.Solver.Yices as Yices + +import qualified Lang.Crucible.Analysis.Postdom as C +import qualified Lang.Crucible.Backend as C +import qualified Lang.Crucible.Backend.SAWCore as C +import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.FunctionHandle as C +import qualified Lang.Crucible.Simulator.EvalStmt as C +import qualified Lang.Crucible.Simulator.ExecutionTree as C +import qualified Lang.Crucible.Simulator.GlobalState as C +import qualified Lang.Crucible.Simulator.Operations as C +import qualified Lang.Crucible.Simulator.OverrideSim as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Simulator.SimError as C +import qualified Lang.Crucible.Simulator.PathSatisfiability as C + +import qualified Lang.Crucible.LLVM.DataLayout as C.LLVM +import qualified Lang.Crucible.LLVM.Extension as C.LLVM +import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM +import qualified Lang.Crucible.LLVM.MemModel as C.LLVM +import qualified Lang.Crucible.LLVM.MemType as C.LLVM +import qualified Lang.Crucible.LLVM.Translation as C.LLVM +import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM + +import qualified Data.Macaw.Types as Macaw +import qualified Data.Macaw.Discovery as Macaw +import qualified Data.Macaw.Memory as Macaw +import qualified Data.Macaw.Memory.LoadCommon as Macaw +import qualified Data.Macaw.Memory.ElfLoader as Macaw +import qualified Data.Macaw.CFG as Macaw +import qualified Data.Macaw.Symbolic as Macaw +import qualified Data.Macaw.Symbolic.Backend as Macaw +import qualified Data.Macaw.AArch32.Symbolic as Macaw +import qualified Data.Macaw.AArch32.Symbolic as Macaw.AArch32 +import qualified Data.Macaw.ARM as Macaw +import qualified Data.Macaw.ARM.ARMReg as Macaw + +import qualified Data.ElfEdit as Elf + +import qualified Language.ASL.Globals as ASL + +------------------------------------------------------------------------------- +-- ** Utility type synonyms and functions + +type Sym = C.SAWCoreBackend GlobalNonceGenerator Yices.Connection (W4.Flags W4.FloatReal) +type LLVMArch = C.LLVM.X86 32 +type LLVM = C.LLVM.LLVM LLVMArch +type LLVMOverrideMatcher = O.OverrideMatcher LLVM +type Regs = Assignment (C.RegValue' Sym) (Macaw.MacawCrucibleRegTypes Macaw.ARM) +type Register = Macaw.ARMReg (Macaw.BVType 32) +type Mem = C.LLVM.MemImpl Sym +type Ptr = C.LLVM.LLVMPtr Sym 32 +type AArch32Constraints = + ( C.LLVM.HasPtrWidth (C.LLVM.ArchWidth LLVMArch) + , C.LLVM.HasLLVMAnn Sym + , ?lc :: C.LLVM.TypeContext + ) + +newtype AArch32Error = AArch32Error String deriving Show +instance Exception AArch32Error + +throwAArch32 :: MonadThrow m => String -> m a +throwAArch32 = throw . AArch32Error + +data RelevantElf = RelevantElf + { memory :: Macaw.Memory 32 + , funSymMap :: Macaw.AddrSymMap 32 + , symMap :: Macaw.AddrSymMap 32 + } + +data Unit = Bytes | Words | DWords | QWords | V128s | V256s deriving Show + +unitByteSize :: Unit -> (forall w. (1 <= w) => NatRepr w -> a) -> a +unitByteSize u k = + case u of + Bytes -> k (knownNat @1) + Words -> k (knownNat @2) + DWords -> k (knownNat @4) + QWords -> k (knownNat @8) + V128s -> k (knownNat @16) + V256s -> k (knownNat @32) + +getElf :: FilePath -> IO (Elf.ElfHeaderInfo 32) +getElf path = + do bs <- BS.readFile path + case Elf.decodeElfHeaderInfo bs of + Right (Elf.SomeElf hdr) + | Elf.ELFCLASS32 <- Elf.headerClass (Elf.header hdr) -> pure hdr + | otherwise -> throwAArch32 "64-bit ELF format" + Left _ -> throwAArch32 "Invalid ELF header" + + +getRelevant :: Elf.ElfHeaderInfo 32 -> IO RelevantElf +getRelevant elf = + case (Macaw.memoryForElf opts elf, Macaw.memoryForElfAllSymbols opts elf) of + (Left err, _) -> throwAArch32 err + (_, Left err) -> throwAArch32 err + (Right (mem, faddrs, _warnings, _errs), Right (_, addrs, _, _)) -> + do let toEntry msym = (Macaw.memSymbolStart msym, Macaw.memSymbolName msym) + return RelevantElf { memory = mem + , funSymMap = Map.fromList (map toEntry faddrs) + , symMap = Map.fromList (map toEntry addrs) + } + + where + opts = Macaw.LoadOptions + { Macaw.loadOffset = Just 0 + } + +posFn :: Macaw.MemSegmentOff 32 -> W4.Position +posFn = W4.OtherPos . Text.pack . show + +findSymbols :: Macaw.AddrSymMap 32 -> ByteString -> [Macaw.MemSegmentOff 32] +findSymbols addrs nm = Map.findWithDefault [] nm invertedMap + where + invertedMap = Map.fromListWith (++) [ (y,[x]) | (x,y) <- Map.toList addrs ] + +loadGlobal :: + RelevantElf -> + (ByteString, Integer, Unit) -> + IO [(String, Integer, Unit, [Integer])] +loadGlobal elf (nm,n,u) = + case findSymbols (symMap elf) nm of + [] -> do print $ symMap elf + err "Global not found" + _ -> mapM loadLoc (findSymbols (symMap elf) nm) + where + mem = memory elf + sname = BSC.unpack nm + + readOne a = case u of + Bytes -> check (Macaw.readWord8 mem a) + Words -> check (Macaw.readWord16le mem a) + DWords -> check (Macaw.readWord32le mem a) + QWords -> check (Macaw.readWord64le mem a) + _ -> err ("unsuported global size: " ++ show u) + + nextAddr = Macaw.incAddr $ fromIntegral (unitByteSize u natValue :: Natural) + + addrsFor o = Prelude.take (fromIntegral n) (iterate nextAddr o) + + check :: (Show b, Integral a) => Either b a -> IO Integer + check res = case res of + Left e -> err (show e) + Right a -> return (fromIntegral a) + + + loadLoc off = do let start = Macaw.segoffAddr off + a = Macaw.memWordToUnsigned (Macaw.addrOffset start) + is <- mapM readOne (addrsFor start) + return (sname, a, u, is) + + err :: [Char] -> IO a + err xs = fail $ unlines + [ "Failed to load global." + , "*** Global: " ++ show nm + , "*** Error: " ++ xs + ] + +freshVal :: + Sym -> C.TypeRepr t -> Bool {- ptrOK ?-}-> String -> IO (C.RegValue Sym t) +freshVal sym t ptrOk nm = + case t of + C.BoolRepr -> do + sn <- symName nm + W4.freshConstant sym sn C.BaseBoolRepr + C.StructRepr tps -> + traverseWithIndex (\idx repr -> C.RV <$> freshVal sym repr True (nm ++ "_field_" ++ show idx)) tps + C.LLVM.LLVMPointerRepr w + | ptrOk, Just Refl <- testEquality w (knownNat @64) -> do + sn_base <- symName (nm ++ "_base") + sn_off <- symName (nm ++ "_off") + base <- W4.freshConstant sym sn_base C.BaseNatRepr + off <- W4.freshConstant sym sn_off (C.BaseBVRepr w) + return (C.LLVM.LLVMPointer base off) + | otherwise -> do + sn <- symName nm + base <- W4.natLit sym 0 + off <- W4.freshConstant sym sn (C.BaseBVRepr w) + return (C.LLVM.LLVMPointer base off) + it -> fail ("[freshVal] Unexpected type repr: " ++ show it) + + where + symName s = + case W4.userSymbol ("macaw_" ++ s) of + Left err -> error ("Invalid symbol name " ++ show s ++ ": " ++ show err) + Right a -> return a + +freshRegister :: Sym -> Index ctx tp -> C.TypeRepr tp -> IO (C.RegValue' Sym tp) +freshRegister sym idx repr = C.RV <$> freshVal sym repr True ("reg" ++ show idx) + +mkGlobalMap :: + C.LLVM.HasLLVMAnn Sym => + Map.Map Macaw.RegionIndex Ptr -> + Macaw.GlobalMap Sym C.LLVM.Mem 32 +mkGlobalMap rmap sym mem region off = + mapConcreteRegion <|> passThroughConcreteRegion <|> mapSymbolicRegion + where + mapConcreteRegion = maybe mzero id (addOffset <$> thisRegion) + thisRegion = join (findRegion <$> W4.asNat region) + findRegion r = Map.lookup (fromIntegral r) rmap + addOffset p = C.LLVM.doPtrAddOffset sym mem p off + where ?ptrWidth = knownNat + passThroughConcreteRegion = + case W4.asNat region of + Nothing -> mzero + Just _ -> return (C.LLVM.LLVMPointer region off) + -- If the symbolic nat is (symbolically) equal to any of the entries in the + -- rmap, we need to do the translation; otherwise, we pass it through + mapSymbolicRegion = foldlM muxSymbolicRegion (C.LLVM.LLVMPointer region off) (Map.toList rmap) + muxSymbolicRegion others (regionNum, basePtr) = do + thisRegionNat <- W4.natLit sym (fromIntegral regionNum) + isEqRegion <- W4.natEq sym thisRegionNat region + adjustedPtr <- addOffset basePtr + C.LLVM.muxLLVMPtr sym isEqRegion adjustedPtr others + +data Goal = Goal + { gAssumes :: [Term] + , gShows :: Term + , gLoc :: W4.ProgramLoc + , gMessage :: C.SimErrorReason + } + +gGoal :: SharedContext -> Goal -> IO Prop +gGoal sc g0 = predicateToProp sc Universal [] =<< go (gAssumes g) + where + g = g0 { gAssumes = mapMaybe skip (gAssumes g0) } + + _shG = do putStrLn "Assuming:" + mapM_ _shT (gAssumes g) + putStrLn "Shows:" + _shT (gShows g) + + + _shT t = putStrLn (" " ++ showTerm t) + + skip a = case asBool a of + Just True -> Nothing + _ -> Just a + + go xs = case xs of + [] -> return (gShows g) + a : as -> scImplies sc a =<< go as + +getGoals :: Sym -> IO [Goal] +getGoals sym = + do obls <- C.proofGoalsToList <$> C.getProofObligations sym + mapM toGoal obls + where + toGoal (C.ProofGoal asmps g) = + do as <- mapM (C.toSC sym) (toListOf (folded . C.labeledPred) asmps) + p <- C.toSC sym (g ^. C.labeledPred) + let C.SimError loc msg = g^.C.labeledPredMsg + return Goal { gAssumes = as + , gShows = p + , gLoc = loc + , gMessage = msg + } + +newtype AArch32Sim a = AArch32Sim { unAArch32Sim :: StateT AArch32State IO a } + deriving (Functor, Applicative, Monad, MonadIO, MonadState AArch32State, MonadThrow) + +data AArch32State = AArch32State + { _aarch32Sym :: Sym + , _aarch32Options :: Options + , _aarch32SharedContext :: SharedContext + , _aarch32CrucibleContext :: LLVMCrucibleContext LLVMArch + , _aarch32ElfSymtab :: Elf.Symtab 32 + , _aarch32RelevantElf :: RelevantElf + , _aarch32MethodSpec :: MS.CrucibleMethodSpecIR LLVM + , _aarch32Mem :: Mem + , _aarch32Regs :: Regs + , _aarch32GlobalBase :: Ptr + } +makeLenses ''AArch32State + +runAArch32Sim :: AArch32State -> AArch32Sim a -> IO (a, AArch32State) +runAArch32Sim st m = runStateT (unAArch32Sim m) st + +setReg :: + (MonadIO m, MonadThrow m) => + Register -> + C.RegValue Sym (C.LLVM.LLVMPointerType 32) -> + Regs -> + m Regs +setReg reg val regs = pure $ Macaw.AArch32.updateReg reg (C.RV . const val) regs + +getReg :: + (MonadIO m, MonadThrow m) => + Register -> + Regs -> + m (C.RegValue Sym (C.LLVM.LLVMPointerType 32)) +getReg reg regs = case Macaw.AArch32.lookupReg reg regs of C.RV val -> pure val + +------------------------------------------------------------------------------- +-- ** Entrypoint + +llvm_verify_aarch32 :: + Some LLVMModule {- ^ Module to associate with method spec -} -> + FilePath {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Bool {- ^ Whether to enable path satisfiability checking -} -> + LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> + ProofScript SatResult {- ^ Tactic used to use when discharging goals -} -> + TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) +llvm_verify_aarch32 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic + | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @32) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do + let ?ptrWidth = knownNat @32 + let ?recordLLVMAnnotation = \_ _ -> return () + sc <- getSharedContext + opts <- getOptions + basic_ss <- getBasicSS + sym <- liftIO $ C.newSAWCoreBackend W4.FloatRealRepr sc globalNonceGenerator + halloc <- getHandleAlloc + let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule + sfs <- liftIO $ Macaw.newSymFuns sym + + (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc path nm + liftIO . print $ cfg + addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0 + then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr + else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"] + let maxAddr = addrInt + toInteger (Macaw.segmentSize $ Macaw.segoffSegment addr) + + let + cc :: LLVMCrucibleContext x + cc = LLVMCrucibleContext + { _ccLLVMModule = llvmModule + , _ccBackend = sym + , _ccBasicSS = basic_ss + + -- It's unpleasant that we need to do this to use resolveSetupVal. + , _ccLLVMSimContext = error "Attempted to access ccLLVMSimContext" + , _ccLLVMGlobals = error "Attempted to access ccLLVMGlobals" + } + + liftIO . printOutLn opts Info $ mconcat + [ "Simulating function \"" + , nm + , "\" (at address " + , show addr + , ")" + ] + + liftIO $ printOutLn opts Info "Examining specification to determine preconditions" + methodSpec <- buildMethodSpec llvmModule nm (show addr) checkSat setup + let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx + + liftIO $ printOutLn opts Info "foo" + + emptyState <- liftIO $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr + liftIO $ printOutLn opts Info "bar" + (env, preState) <- liftIO . runAArch32Sim emptyState $ setupMemory globsyms + liftIO $ printOutLn opts Info "baz" + + let + funcLookup = Macaw.LookupFunctionHandle $ \st _mem regs -> do + C.LLVM.LLVMPointer _base off <- getReg Macaw.ip_reg regs + case BV.asUnsigned <$> W4.asBV off of + Nothing -> fail $ mconcat + [ "Attempted to call a function with non-concrete address " + , show $ W4.ppExpr off + ] + Just funcAddr -> do + case Macaw.resolveRegionOff (memory relf) 0 $ fromIntegral funcAddr of + Nothing -> fail $ mconcat + [ "Failed to resolve function address " + , show $ W4.ppExpr off + ] + Just funcAddrOff -> do + case Map.lookup funcAddrOff cfgs of + Just (C.SomeCFG funcCFG) -> + pure + ( C.cfgHandle funcCFG + , st & C.stateContext . C.functionBindings + %~ C.insertHandleMap (C.cfgHandle funcCFG) (C.UseCFG funcCFG $ C.postdomInfo funcCFG) + ) + Nothing -> fail $ mconcat + [ "Unable to find CFG for function at address " + , show $ W4.ppExpr off + ] + noExtraValidityPred _ _ _ _ = return Nothing + ctx :: C.SimContext (Macaw.MacawSimulatorState Sym) Sym (Macaw.MacawExt Macaw.ARM) + ctx = C.SimContext + { C._ctxSymInterface = sym + , C.ctxSolverProof = id + , C.ctxIntrinsicTypes = C.LLVM.llvmIntrinsicTypes + , C.simHandleAllocator = halloc + , C.printHandle = stdout + , C.extensionImpl = + Macaw.macawExtensions (Macaw.aarch32MacawEvalFn sfs) mvar + (mkGlobalMap . Map.singleton 0 $ preState ^. aarch32GlobalBase) + funcLookup noExtraValidityPred + , C._functionBindings = C.insertHandleMap (C.cfgHandle cfg) (C.UseCFG cfg $ C.postdomInfo cfg) C.emptyHandleMap + , C._cruciblePersonality = Macaw.MacawSimulatorState + , C._profilingMetrics = Map.empty + } + globals = C.insertGlobal mvar (preState ^. aarch32Mem) C.emptyGlobals + macawStructRepr = C.StructRepr $ Macaw.crucArchRegTypes Macaw.aarch32MacawSymbolicFns + initial = C.InitialState ctx globals C.defaultAbortHandler macawStructRepr + $ C.runOverrideSim macawStructRepr + $ Macaw.crucGenArchConstraints Macaw.aarch32MacawSymbolicFns + $ do + r <- C.callCFG cfg . C.RegMap . singleton . C.RegEntry macawStructRepr $ preState ^. aarch32Regs + globals' <- C.readGlobals + mem' <- C.readGlobal mvar + let finalState = preState + { _aarch32Mem = mem' + , _aarch32Regs = C.regValue r + , _aarch32CrucibleContext = cc & ccLLVMGlobals .~ globals' + } + liftIO $ printOutLn opts Info + "Examining specification to determine postconditions" + liftIO . void . runAArch32Sim finalState $ assertPost globals' env (preState ^. aarch32Mem) (preState ^. aarch32Regs) + pure $ C.regValue r + + liftIO $ printOutLn opts Info "Simulating function" + + psatf <- + if checkSat then + do f <- liftIO (C.pathSatisfiabilityFeature sym (C.considerSatisfiability sym)) + pure [C.genericToExecutionFeature f] + else + pure [] + + let execFeatures = psatf + + liftIO $ C.executeCrucible execFeatures initial >>= \case + C.FinishedResult{} -> pure () + C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns" + C.TimeoutResult{} -> fail "Execution timed out" + + stats <- checkGoals sym opts sc tactic + + returnProof $ SomeLLVM (methodSpec & MS.csSolverStats .~ stats) + | otherwise = fail "LLVM module must be AArch32" + +-------------------------------------------------------------------------------- +-- ** Computing the CFG + +-- | Load the given ELF file and use Macaw to construct a Crucible CFG. +buildCFG :: + Options -> + C.HandleAllocator -> + String {- ^ Path to ELF file -} -> + String {- ^ Function's symbol in ELF file -} -> + IO ( C.SomeCFG + (Macaw.MacawExt Macaw.ARM) + (EmptyCtx ::> Macaw.ArchRegStruct Macaw.ARM) + (Macaw.ArchRegStruct Macaw.ARM) + , Elf.ElfHeaderInfo 32 + , RelevantElf + , Macaw.MemSegmentOff 32 + , Map + (Macaw.MemSegmentOff 32) + (C.SomeCFG + (Macaw.MacawExt Macaw.ARM) + (EmptyCtx ::> Macaw.ArchRegStruct Macaw.ARM) + (Macaw.ArchRegStruct Macaw.ARM)) + ) +buildCFG opts halloc path nm = do + printOutLn opts Info $ mconcat ["Finding symbol for \"", nm, "\""] + elf <- getElf path + relf <- getRelevant elf + (addr :: Macaw.MemSegmentOff 32) <- + case findSymbols (symMap relf) . encodeUtf8 $ Text.pack nm of + (addr:_) -> pure addr + _ -> fail $ mconcat ["Could not find symbol \"", nm, "\""] + printOutLn opts Info $ mconcat ["Found symbol at address ", show addr, ", building CFG"] + let + initialDiscoveryState = + Macaw.emptyDiscoveryState (memory relf) (funSymMap relf) Macaw.arm_linux_info + -- "inline" any function addresses that we happen to jump to + & Macaw.trustedFunctionEntryPoints .~ Map.empty + finalState = Macaw.cfgFromAddrsAndState initialDiscoveryState [addr] [] + finfos = finalState ^. Macaw.funInfo + cfgs <- forM finfos $ \(Some finfo) -> + Macaw.mkFunCFG Macaw.aarch32MacawSymbolicFns halloc + (W4.functionNameFromText . decodeUtf8 $ Macaw.discoveredFunName finfo) + posFn finfo + + case Map.lookup addr cfgs of + Nothing -> throwAArch32 $ "Unable to discover CFG from address " <> show addr + Just scfg -> pure (scfg, elf, relf, addr, cfgs) + +-------------------------------------------------------------------------------- +-- ** Computing the specification + +-- | Construct the method spec like we normally would in llvm_verify. +-- Unlike in llvm_verify, we can't reuse the simulator state (due to the +-- different memory layout / RegMap). +buildMethodSpec :: + LLVMModule LLVMArch -> + String {- ^ Name of method -} -> + String {- ^ Source location for method spec (here, we use the address) -} -> + Bool {- ^ check sat -} -> + LLVMCrucibleSetupM () -> + TopLevel (MS.CrucibleMethodSpecIR LLVM) +buildMethodSpec lm nm loc checkSat setup = + setupLLVMCrucibleContext checkSat lm $ \cc -> do + let methodId = LLVMMethodId nm Nothing + let programLoc = + W4.mkProgramLoc (W4.functionNameFromText $ Text.pack nm) + . W4.OtherPos $ Text.pack loc + let lc = modTrans lm ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx + opts <- getOptions + (args, ret) <- case llvmSignature opts lm nm of + Left err -> fail $ mconcat ["Could not find declaration for \"", nm, "\": ", err] + Right x -> pure x + (mtargs, mtret) <- case (,) <$> mapM (llvmTypeToMemType lc) args <*> mapM (llvmTypeToMemType lc) ret of + Left err -> fail err + Right x -> pure x + let initialMethodSpec = MS.makeCrucibleMethodSpecIR @LLVM + methodId mtargs mtret programLoc lm + view Setup.csMethodSpec <$> execStateT (runLLVMCrucibleSetupM setup) + (Setup.makeCrucibleSetupState cc initialMethodSpec) + +llvmTypeToMemType :: + C.LLVM.TypeContext -> + LLVM.Type -> + Either String C.LLVM.MemType +llvmTypeToMemType lc t = let ?lc = lc in C.LLVM.liftMemType t + +-- | Find a function declaration in the LLVM AST and return its signature. +llvmSignature :: + Options -> + LLVMModule LLVMArch -> + String -> + Either String ([LLVM.Type], Maybe LLVM.Type) +llvmSignature opts llvmModule nm = + case findDecl (modAST llvmModule) nm of + Left err -> case findDefMaybeStatic (modAST llvmModule) nm of + Left _ -> Left $ displayVerifExceptionOpts opts err + Right defs -> pure + ( LLVM.typedType <$> LLVM.defArgs (NE.head defs) + , case LLVM.defRetType $ NE.head defs of + LLVM.PrimType LLVM.Void -> Nothing + x -> Just x + ) + Right decl -> pure + ( LLVM.decArgs decl + , case LLVM.decRetType decl of + LLVM.PrimType LLVM.Void -> Nothing + x -> Just x + ) + +-------------------------------------------------------------------------------- +-- ** Building the initial state + +initialState :: + AArch32Constraints => + Sym -> + Options -> + SharedContext -> + LLVMCrucibleContext LLVMArch -> + Elf.ElfHeaderInfo 32 -> + RelevantElf -> + MS.CrucibleMethodSpecIR LLVM -> + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + Integer {- ^ Minimum size of the global allocation (here, the end of the .text segment -} -> + IO AArch32State +initialState sym opts sc cc elf relf ms globs maxAddr = do + emptyMem <- C.LLVM.emptyMem C.LLVM.LittleEndian + emptyRegs <- traverseWithIndex (freshRegister sym) C.knownRepr + symTab <- case Elf.decodeHeaderSymtab elf of + Nothing -> throwAArch32 "Elf file has no symbol table" + Just (Left _err) -> throwAArch32 "Failed to decode symbol table" + Just (Right st) -> pure st + let + align = C.LLVM.exponentToAlignment 4 + allocGlobalEnd :: MS.AllocGlobal LLVM -> Integer + allocGlobalEnd (LLVMAllocGlobal _ (LLVM.Symbol nm)) = globalEnd nm + globalEnd :: String -> Integer + globalEnd nm = maybe 0 (\entry -> fromIntegral $ Elf.steValue entry + Elf.steSize entry) $ + (Vector.!? 0) + . Vector.filter (\e -> Elf.steName e == encodeUtf8 (Text.pack nm)) + $ Elf.symtabEntries symTab + sz <- W4.bvLit sym knownNat . BV.mkBV knownNat . maximum $ mconcat + [ [maxAddr, globalEnd "_end"] + , globalEnd . fst <$> globs + , allocGlobalEnd <$> ms ^. MS.csGlobalAllocs + ] + (base, mem) <- C.LLVM.doMalloc sym C.LLVM.GlobalAlloc C.LLVM.Immutable + "globals" emptyMem sz align + pure $ AArch32State + { _aarch32Sym = sym + , _aarch32Options = opts + , _aarch32SharedContext = sc + , _aarch32CrucibleContext = cc + , _aarch32ElfSymtab = symTab + , _aarch32RelevantElf = relf + , _aarch32MethodSpec = ms + , _aarch32Mem = mem + , _aarch32Regs = emptyRegs + , _aarch32GlobalBase = base + } + +-------------------------------------------------------------------------------- +-- ** Precondition + +-- | Given the method spec, build the initial memory, register map, and global map. +setupMemory :: + AArch32Constraints => + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + AArch32Sim (Map MS.AllocIndex Ptr) +setupMemory globsyms = do + setupGlobals globsyms + + liftIO $ putStrLn "1" + + -- Allocate a reasonable amount of stack (4 KiB + 1 qword for IP) + allocateStack 4096 + + liftIO $ putStrLn "2" + + ms <- use aarch32MethodSpec + + let + tyenv = ms ^. MS.csPreState . MS.csAllocs + nameEnv = MS.csTypeNames ms + + env <- foldlM assumeAllocation Map.empty . Map.assocs $ tyenv + + liftIO $ putStrLn "3" + + mapM_ (assumePointsTo env tyenv nameEnv) $ ms ^. MS.csPreState . MS.csPointsTos + + liftIO $ putStrLn "4" + + setArgs env tyenv nameEnv . fmap snd . Map.elems $ ms ^. MS.csArgBindings + + liftIO $ putStrLn "5" + + pure env + +-- | Given an alist of symbol names and sizes (in bytes), allocate space and copy +-- the corresponding globals from the Macaw memory to the Crucible LLVM memory model. +setupGlobals :: + AArch32Constraints => + [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} -> + AArch32Sim () +setupGlobals globsyms = do + sym <- use aarch32Sym + mem <- use aarch32Mem + relf <- use aarch32RelevantElf + base <- use aarch32GlobalBase + let + readInitialGlobal :: (String, Integer) -> IO [(String, Integer, [Integer])] + readInitialGlobal (nm, sz) = do + res <- loadGlobal relf (encodeUtf8 $ Text.pack nm, sz, Bytes) + pure $ (\(name, addr, _unit, bytes) -> (name, addr, bytes)) <$> res + convertByte :: Integer -> IO (C.LLVM.LLVMVal Sym) + convertByte byte = + C.LLVM.LLVMValInt <$> W4.natLit sym 0 <*> W4.bvLit sym (knownNat @8) (BV.mkBV knownNat byte) + writeGlobal :: Mem -> (String, Integer, [Integer]) -> IO Mem + writeGlobal m (_nm, addr, bytes) = do + ptr <- C.LLVM.doPtrAddOffset sym m base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr) + v <- Vector.fromList <$> mapM convertByte bytes + let st = C.LLVM.arrayType (fromIntegral $ length bytes) $ C.LLVM.bitvectorType 1 + C.LLVM.storeConstRaw sym m ptr st C.LLVM.noAlignment + $ C.LLVM.LLVMValArray (C.LLVM.bitvectorType 1) v + globs <- liftIO $ mconcat <$> mapM readInitialGlobal globsyms + mem' <- liftIO $ foldlM writeGlobal mem globs + aarch32Mem .= mem' + +-- | Allocate memory for the stack, and pushes a fresh pointer as the return +-- address. +allocateStack :: + AArch32Constraints => + Integer {- ^ Stack size in bytes -} -> + AArch32Sim () +allocateStack szInt = do + sym <- use aarch32Sym + mem <- use aarch32Mem + regs <- use aarch32Regs + let align = C.LLVM.exponentToAlignment 4 + sz <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ szInt + 8 + (base, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc C.LLVM.Mutable + "stack_alloc" mem sz align + sn <- case W4.userSymbol "stack" of + Left err -> throwAArch32 $ "Invalid symbol for stack: " <> show err + Right sn -> pure sn + aarch32Mem .= mem' + finalRegs <- setReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R13")) base regs + aarch32Regs .= finalRegs + +-- | Process an llvm_alloc statement, allocating the requested memory and +-- associating a pointer to that memory with the appropriate index. +assumeAllocation :: + AArch32Constraints => + Map MS.AllocIndex Ptr -> + (MS.AllocIndex, LLVMAllocSpec) {- ^ llvm_alloc statement -} -> + AArch32Sim (Map MS.AllocIndex Ptr) +assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc False) = do + cc <- use aarch32CrucibleContext + sym <- use aarch32Sym + mem <- use aarch32Mem + sz' <- liftIO $ resolveSAWSymBV cc knownNat sz + (ptr, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc mut + (show $ W4.plSourceLoc loc) mem sz' align + aarch32Mem .= mem' + pure $ Map.insert i ptr env +assumeAllocation env _ = pure env + -- no allocation is done for llvm_fresh_pointer + -- TODO: support llvm_fresh_pointer in x86 verification + +-- | Process an llvm_points_to statement, writing some SetupValue to a pointer. +assumePointsTo :: + AArch32Constraints => + Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> + Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> + AArch32Sim () +assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do + when (isJust cond) $ throwAArch32 "unsupported x86_64 command: llvm_conditional_points_to" + tval <- checkConcreteSizePointsToValue tptval + sym <- use aarch32Sym + cc <- use aarch32CrucibleContext + mem <- use aarch32Mem + ptr <- resolvePtrSetupValue env tyenv tptr + val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval + storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval + mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val + aarch32Mem .= mem' + +resolvePtrSetupValue :: + AArch32Constraints => + Map MS.AllocIndex Ptr -> + Map MS.AllocIndex LLVMAllocSpec -> + MS.SetupValue LLVM -> + AArch32Sim Ptr +resolvePtrSetupValue env tyenv tptr = do + sym <- use aarch32Sym + cc <- use aarch32CrucibleContext + mem <- use aarch32Mem + symTab <- use aarch32ElfSymtab + base <- use aarch32GlobalBase + case tptr of + MS.SetupGlobal () nm -> case + (Vector.!? 0) + . Vector.filter (\e -> Elf.steName e == encodeUtf8 (Text.pack nm)) + $ Elf.symtabEntries symTab of + Nothing -> throwAArch32 $ mconcat ["Global symbol \"", nm, "\" not found"] + Just entry -> do + let addr = fromIntegral $ Elf.steValue entry + liftIO $ C.LLVM.doPtrAddOffset sym mem base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr) + _ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + =<< resolveSetupVal cc mem env tyenv Map.empty tptr + +checkConcreteSizePointsToValue :: LLVMPointsToValue LLVMArch -> AArch32Sim (MS.SetupValue LLVM) +checkConcreteSizePointsToValue = \case + ConcreteSizeValue val -> return val + SymbolicSizeValue{} -> throwAArch32 "unsupported x86_64 command: llvm_points_to_array_prefix" + +-- | Write each SetupValue passed to llvm_execute_func to the appropriate +-- x86_64 register from the calling convention. +setArgs :: + AArch32Constraints => + Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> + Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + [MS.SetupValue LLVM] {- ^ Arguments passed to llvm_execute_func -} -> + AArch32Sim () +setArgs env tyenv nameEnv args + | length args > length argRegs = throwAArch32 "More arguments than would fit into general-purpose registers" + | otherwise = do + sym <- use aarch32Sym + cc <- use aarch32CrucibleContext + mem <- use aarch32Mem + let + setRegSetupValue rs (reg, sval) = typeOfSetupValue cc tyenv nameEnv sval >>= \ty -> + case ty of + C.LLVM.PtrType _ -> do + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + =<< resolveSetupVal cc mem env tyenv nameEnv sval + setReg reg val rs + C.LLVM.IntType 32 -> do + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + =<< resolveSetupVal cc mem env tyenv nameEnv sval + setReg reg val rs + C.LLVM.IntType _ -> do + C.LLVM.LLVMValInt base off <- resolveSetupVal cc mem env tyenv nameEnv sval + case testLeq (incNat $ W4.bvWidth off) (knownNat @32) of + Nothing -> fail "Argument bitvector does not fit in a single general-purpose register" + Just LeqProof -> do + off' <- W4.bvZext sym (knownNat @32) off + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @32) + $ C.LLVM.LLVMValInt base off' + setReg reg val rs + _ -> fail "Argument does not fit into a single general-purpose register" + regs <- use aarch32Regs + newRegs <- liftIO . foldlM setRegSetupValue regs $ zip argRegs args + aarch32Regs .= newRegs + where + argRegs = + [ Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R0") + , Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R1") + , Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R2") + , Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R3") + ] + +-------------------------------------------------------------------------------- +-- ** Postcondition + +-- | Assert the postcondition for the spec, given the final memory and register map. +assertPost :: + AArch32Constraints => + C.SymGlobalState Sym -> + Map MS.AllocIndex Ptr -> + Mem {- ^ The state of memory before simulation -} -> + Regs {- ^ The state of the registers before simulation -} -> + AArch32Sim () +assertPost globals env premem preregs = do + sym <- use aarch32Sym + opts <- use aarch32Options + sc <- use aarch32SharedContext + cc <- use aarch32CrucibleContext + ms <- use aarch32MethodSpec + postregs <- use aarch32Regs + let + tyenv = ms ^. MS.csPreState . MS.csAllocs + nameEnv = MS.csTypeNames ms + + expectedIP <- getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R14")) preregs + actualIP <- getReg Macaw.ip_reg postregs + correctRetAddr <- liftIO $ C.LLVM.ptrEq sym C.LLVM.PtrWidth actualIP expectedIP + liftIO . C.addAssertion sym . C.LabeledPred correctRetAddr . C.SimError W4.initializationLoc + $ C.AssertFailureSimError "Instruction pointer not set to return address" "" + + prersp <- getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R13")) preregs + postrsp <- getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R13")) postregs + correctStack <- liftIO $ C.LLVM.ptrEq sym C.LLVM.PtrWidth prersp postrsp + liftIO $ C.addAssertion sym . C.LabeledPred correctStack . C.SimError W4.initializationLoc + $ C.AssertFailureSimError "Stack not preserved" "" + + returnMatches <- case (ms ^. MS.csRetValue, ms ^. MS.csRet) of + (Just expectedRet, Just retTy) -> do + postRAX <- C.LLVM.ptrToPtrVal <$> getReg (Macaw.ARMGlobalBV (ASL.knownGlobalRef @"_R0")) postregs + case (postRAX, C.LLVM.memTypeBitwidth retTy) of + (C.LLVM.LLVMValInt base off, Just retTyBits) -> do + let + truncateRAX :: forall r. NatRepr r -> AArch32Sim (C.LLVM.LLVMVal Sym) + truncateRAX rsz = + case (testLeq (knownNat @1) rsz, testLeq rsz (W4.bvWidth off)) of + (Just LeqProof, Just LeqProof) -> + case testStrictLeq rsz (W4.bvWidth off) of + Left LeqProof -> do + offTrunc <- liftIO $ W4.bvTrunc sym rsz off + pure $ C.LLVM.LLVMValInt base offTrunc + _ -> pure $ C.LLVM.LLVMValInt base off + _ -> throwAArch32 "Width of return type is zero bits" + postRAXTrunc <- viewSome truncateRAX (mkNatRepr retTyBits) + pure [LO.matchArg opts sc cc ms MS.PostState postRAXTrunc retTy expectedRet] + _ -> throwAArch32 $ "Invalid return type: " <> show (C.LLVM.ppMemType retTy) + _ -> pure [] + + pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) + $ assertPointsTo env tyenv nameEnv + + let setupConditionMatches = fmap + (LO.learnSetupCondition opts sc cc ms MS.PostState) + $ ms ^. MS.csPostState . MS.csConditions + + let + initialECs = Map.fromList + [ (ecVarIndex ec, ec) + | tt <- ms ^. MS.csPreState . MS.csFreshVars + , let ec = tecExt tt + ] + initialFree = Set.fromList . fmap (ecVarIndex . tecExt) $ ms ^. MS.csPostState . MS.csFreshVars + + initialTerms <- liftIO $ traverse (scExtCns sc) initialECs + + result <- liftIO + . O.runOverrideMatcher sym globals env initialTerms initialFree (ms ^. MS.csLoc) + . sequence_ $ mconcat + [ returnMatches + , pointsToMatches + , setupConditionMatches + ] + st <- case result of + Left err -> throwAArch32 $ show err + Right (_, st) -> pure st + liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) -> + C.addAssertion sym $ C.LabeledPred p r + +-- | Assert that a points-to postcondition holds. +assertPointsTo :: + AArch32Constraints => + Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> + Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> + AArch32Sim (LLVMOverrideMatcher md ()) +assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptexpected) = do + when (isJust cond) $ throwAArch32 "unsupported x86_64 command: llvm_conditional_points_to" + texpected <- checkConcreteSizePointsToValue tptexpected + sym <- use aarch32Sym + opts <- use aarch32Options + sc <- use aarch32SharedContext + cc <- use aarch32CrucibleContext + ms <- use aarch32MethodSpec + mem <- use aarch32Mem + ptr <- resolvePtrSetupValue env tyenv tptr + memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv texpected + storTy <- liftIO $ C.LLVM.toStorableType memTy + + actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment + pure $ LO.matchArg opts sc cc ms MS.PostState actual memTy texpected + +-- | Gather and run the solver on goals from the simulator. +checkGoals :: + Sym -> + Options -> + SharedContext -> + ProofScript SatResult -> + TopLevel SolverStats +checkGoals sym opts sc tactic = do + gs <- liftIO $ getGoals sym + liftIO . printOutLn opts Info $ mconcat + [ "Simulation finished, running solver on " + , show $ length gs + , " goals" + ] + stats <- forM (zip [0..] gs) $ \(n, g) -> do + term <- liftIO $ gGoal sc g + let proofgoal = ProofGoal n "vc" (show $ gMessage g) term + r <- evalStateT tactic $ startProof proofgoal + case r of + Unsat stats -> return stats + SatMulti stats vals -> do + printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g] + printOutLnTop Info (show stats) + printOutLnTop OnlyCounterExamples "----------Counterexample----------" + ppOpts <- sawPPOpts . rwPPOpts <$> getTopLevelRW + case vals of + [] -> printOutLnTop OnlyCounterExamples "<>" + _ -> let showAssignment (name, val) = + mconcat [ " ", name, ": ", show $ ppFirstOrderValue ppOpts val ] + in mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals + printOutLnTop OnlyCounterExamples "----------------------------------" + throwTopLevel "Proof failed." + liftIO $ printOutLn opts Info "All goals succeeded" + return (mconcat stats) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index be1a04c75c..5cb4b699b3 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -83,6 +83,7 @@ import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ import SAWScript.Crucible.LLVM.Builtins import SAWScript.Crucible.JVM.Builtins import SAWScript.Crucible.LLVM.X86 +import SAWScript.Crucible.LLVM.AArch32 import SAWScript.Crucible.LLVM.Boilerplate import SAWScript.Crucible.LLVM.Skeleton.Builtins import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR @@ -2498,6 +2499,21 @@ primitives = Map.fromList Current [ "Use the default set of callee-saved registers during x86 verification.." ] + , prim "llvm_verify_aarch32" + "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> LLVMSetup () -> ProofScript SatResult -> TopLevel LLVMSpec" + (pureVal llvm_verify_aarch32) + Experimental + [ "Verify an AArch32 function from an ELF file for use as an override in an" + , "LLVM verification. The first argument specifies the LLVM module" + , "containing the _caller_. The second and third specify the ELF file" + , "name and symbol name of the function to be verifier. The fourth" + , "specifies the names and sizes (in bytes) of global variables to" + , "initialize, and the fifth whether to perform path satisfiability" + , "checking. The last argument is the LLVM specification of the calling" + , "context against which to verify the function. Returns a method spec" + , "that can be used as an override when verifying other LLVM functions." + ] + , prim "llvm_array_value" "[SetupValue] -> SetupValue" (pureVal CIR.anySetupArray) From f44106f47a5e7ce12829fc03632fc8b116efd4b0 Mon Sep 17 00:00:00 2001 From: David Holland Date: Tue, 8 Apr 2025 19:21:52 -0400 Subject: [PATCH 02/22] aarch32: bump macaw commit (I merged macaw master with the small aarch32 commit in macaw and this is the result) (There was an earlier version of this commit that references a broken version of the macaw commit; that commit got reconned and so did the one referencing it, and if you're seeing this both should have disappeared. This note is to prevent confusion in case one of them comes back from the dead again at some point.) --- deps/macaw | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/macaw b/deps/macaw index 12ce4d05d8..898c3d1dab 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 12ce4d05d81d21854fd68aba33e05c9ca5e6eb96 +Subproject commit 898c3d1dabe21580c6fb860b464f22ebef4b71b3 From 527398c08fe3f7be8e1cbc54280a3e726c70ff1d Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 9 Apr 2025 20:09:59 -0400 Subject: [PATCH 03/22] Bump the new git submodules to their current versions. (the new git submodules on this branch, aarch32, are exactly the ones updated in this commit, since all were quite out of date) --- deps/arm-asl-parser | 2 +- deps/asl-translator | 2 +- deps/dismantle | 2 +- deps/semmc | 2 +- deps/what4-serialize | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/deps/arm-asl-parser b/deps/arm-asl-parser index afbeff2db4..4473ebc229 160000 --- a/deps/arm-asl-parser +++ b/deps/arm-asl-parser @@ -1 +1 @@ -Subproject commit afbeff2db4781e138bb8c920d803b7e7a88383b7 +Subproject commit 4473ebc229c2ee44ed6cf51e3eedebebce5a4bb7 diff --git a/deps/asl-translator b/deps/asl-translator index 943cf7d724..9940a0483f 160000 --- a/deps/asl-translator +++ b/deps/asl-translator @@ -1 +1 @@ -Subproject commit 943cf7d724b15c6ae4b650061f96c8bf0b63344a +Subproject commit 9940a0483f7042c021984281ad5ca5e3b781215e diff --git a/deps/dismantle b/deps/dismantle index 1c2e7892c6..e4ebe05fbc 160000 --- a/deps/dismantle +++ b/deps/dismantle @@ -1 +1 @@ -Subproject commit 1c2e7892c6edc514cef94efa68717c7a7505140a +Subproject commit e4ebe05fbce079973e9619198c9eb14dec74fe5f diff --git a/deps/semmc b/deps/semmc index a60ace5ab6..519d70e2a5 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit a60ace5ab6036dcb0c63aec0dddd2324b288ef9c +Subproject commit 519d70e2a588a9c69f2d5caa3af31c61a0c5f100 diff --git a/deps/what4-serialize b/deps/what4-serialize index 1266de365f..e8dc91e232 160000 --- a/deps/what4-serialize +++ b/deps/what4-serialize @@ -1 +1 @@ -Subproject commit 1266de365f6fd094fd7456311a2072cb1ef651ed +Subproject commit e8dc91e232033b708bf61b5389226a9504b5d4e5 From ef603117d714a177fe05b276386b6172bcc4b7d5 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 9 Apr 2025 21:10:07 -0400 Subject: [PATCH 04/22] cabal.project: add macaw-loader-aarch32, drop what4-serialize macaw-loader-aarch32 is now needed by the other aarch32 bits; what4-serialize was merged into what4 upstream. --- cabal.project | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index 27bc6c6fcf..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -35,7 +35,6 @@ packages: deps/flexdis86/binary-symbols deps/lmdb/lmdb deps/lmdb/lmdb-simple - deps/what4-serialize deps/asl-translator deps/arm-asl-parser deps/dismantle/dismantle-tablegen @@ -46,6 +45,7 @@ packages: deps/macaw/base deps/macaw/macaw-dump deps/macaw/macaw-loader + deps/macaw/macaw-loader-aarch32 deps/macaw/macaw-loader-x86 deps/macaw/symbolic deps/macaw/x86 From c8509bc5e5021cf8b580f43c83f0a65e3948bcb5 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 9 Apr 2025 21:13:00 -0400 Subject: [PATCH 05/22] Remove the what4-serialize submodule as it's no longer relevant. (it was added on this branch) --- .gitmodules | 3 --- deps/what4-serialize | 1 - 2 files changed, 4 deletions(-) delete mode 160000 deps/what4-serialize diff --git a/.gitmodules b/.gitmodules index 257af32498..743a61f250 100644 --- a/.gitmodules +++ b/.gitmodules @@ -52,9 +52,6 @@ [submodule "deps/mir-json"] path = deps/mir-json url = https://github.com/GaloisInc/mir-json.git -[submodule "deps/what4-serialize"] - path = deps/what4-serialize - url = https://github.com/GaloisInc/what4-serialize [submodule "deps/asl-translator"] path = deps/asl-translator url = https://github.com/GaloisInc/asl-translator diff --git a/deps/what4-serialize b/deps/what4-serialize deleted file mode 160000 index e8dc91e232..0000000000 --- a/deps/what4-serialize +++ /dev/null @@ -1 +0,0 @@ -Subproject commit e8dc91e232033b708bf61b5389226a9504b5d4e5 From 4c8b8a5043bfbdef2ba8c5a251535d20a3711bbe Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 9 Apr 2025 21:32:31 -0400 Subject: [PATCH 06/22] Add a copy of SAWCore.hs from crucible-saw. This will be SAWScript.Crucible.CrucibleSAW.SAWCore in the module namespace, at least for now. (The old module path was Lang.Crucible.Backend.SAWCore.) This is a verbatim copy of the file from crucible-saw as it existed when it was deleted from the crucible tree two months ago. It won't build without updating its module header, but I'm going to commit that separately for ease of possible later rearrangements. --- src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 1296 +++++++++++++++++ 1 file changed, 1296 insertions(+) create mode 100644 src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs new file mode 100644 index 0000000000..f04f1605a0 --- /dev/null +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -0,0 +1,1296 @@ +----------------------------------------------------------------------- +-- | +-- Module : Lang.Crucible.Backend.SAWCore +-- Description : Crucible interface for generating SAWCore +-- Copyright : (c) Galois, Inc 2014-2016 +-- License : BSD3 +-- Maintainer : Rob Dockins +-- Stability : provisional +-- +-- This module provides a Crucible backend that produces SAWCore terms. +------------------------------------------------------------------------ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ViewPatterns #-} + +module Lang.Crucible.Backend.SAWCore where + +import Control.Exception ( bracket ) +import Control.Lens +import Control.Monad +import qualified Data.BitVector.Sized as BV +import Data.IORef +import Data.List (elemIndex) +import Data.Foldable (toList) +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Map ( Map ) +import qualified Data.Map as Map +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Nonce +import Data.Parameterized.Some +import Data.Parameterized.TraversableFC +import Data.Ratio +import Data.Sequence (Seq) +import qualified Data.Sequence as Seq +import Data.Word(Word64) +import qualified Data.Text as Text + +import Numeric.Natural + +import What4.BaseTypes +import What4.Config +import What4.Interface +import qualified What4.Expr.ArrayUpdateMap as AUM +import qualified What4.Expr.Builder as B +import qualified What4.Expr.BoolMap as BM +import qualified What4.Expr.WeightedSum as WSum +import What4.ProgramLoc +import What4.Protocol.Online +import What4.Protocol.SMTWriter as SMT +import What4.SatResult +import qualified What4.SemiRing as B +import qualified What4.Solver.Yices as Yices +import What4.Symbol + +import Lang.Crucible.Panic(panic) +import Lang.Crucible.Backend +import Lang.Crucible.Backend.Online hiding (withSolverProcess) +import qualified Lang.Crucible.Backend.AssumptionStack as AS +import Lang.Crucible.Simulator.SimError + +import qualified Verifier.SAW.SharedTerm as SC +import qualified Verifier.SAW.TypedAST as SC + +data SAWCruciblePersonality sym = SAWCruciblePersonality + +-- | The SAWCoreBackend is a crucible backend that represents symbolic values +-- as SAWCore terms. +data SAWCoreState solver fs n + = SAWCoreState + { saw_ctx :: SC.SharedContext -- ^ the main SAWCore datastructure for building shared terms + , saw_inputs :: IORef (Seq (SC.ExtCns SC.Term )) + -- ^ a record of all the symbolic input variables created so far, + -- in the order they were created + + , saw_symMap :: !(Map Word64 (SC.SharedContext -> [SC.Term] -> IO SC.Term)) + -- ^ What to do with uninterpreted functions. + -- The key is the "indexValue" of the "symFunId" for the function + + , saw_elt_cache :: B.IdxCache n SAWExpr + -- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term. + + , saw_elt_cache_r :: IORef (IntMap (Some (B.SymExpr (SAWCoreBackend n solver fs)))) + -- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable. + -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between + -- SAWCore terms and What4 variables. + + , saw_online_state :: OnlineBackendState solver n + } + +data SAWExpr (bt :: BaseType) where + SAWExpr :: !SC.Term -> SAWExpr bt + + -- This is a term that represents an integer, but has an + -- implicit integer-to-real conversion. + IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType + -- This is a SAWCore term that represents a natural number, but has an + -- implicit nat-to-integer conversion. + NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType + +type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState solver fs) fs + + +-- | Run the given IO action with the given SAW backend. +-- While while running the action, the SAW backend is +-- set up with a fresh naming context. This means that all +-- symbolic inputs, symMap entries, element cache entires, +-- assertions and proof obligations start empty while +-- running the action. After the action completes, the +-- state of these fields is restored. +inFreshNamingContext :: SAWCoreBackend n solver fs -> IO a -> IO a +inFreshNamingContext sym f = + do old <- readIORef (B.sbStateManager sym) + bracket (mkNew (B.exprCounter sym) old) (restore old) action + + where + action new = + do writeIORef (B.sbStateManager sym) new + f + + restore old _new = + do writeIORef (B.sbStateManager sym) old + + mkNew _gen old = + do ch <- B.newIdxCache + ch_r <- newIORef IntMap.empty + iref <- newIORef mempty + let new = SAWCoreState + { saw_ctx = saw_ctx old + , saw_inputs = iref + , saw_symMap = mempty + , saw_elt_cache = ch + , saw_elt_cache_r = ch_r + , saw_online_state = saw_online_state old + } + return new + +getInputs :: SAWCoreBackend n solver fs -> IO (Seq (SC.ExtCns SC.Term)) +getInputs sym = + do st <- readIORef (B.sbStateManager sym) + readIORef (saw_inputs st) + +baseSCType :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + BaseTypeRepr tp -> + IO SC.Term +baseSCType sym sc bt = + case bt of + BaseBoolRepr -> SC.scBoolType sc + BaseBVRepr w -> SC.scBitvector sc $ fromIntegral (natValue w) + BaseNatRepr -> SC.scNatType sc + BaseIntegerRepr -> SC.scIntegerType sc + BaseArrayRepr indexTypes range + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + SC.scArrayType sc sc_idx_type sc_elm_type + | otherwise -> + unsupported sym "SAW backend does not support multidimensional Arrays: baseSCType" + BaseFloatRepr _ -> + unsupported sym "SAW backend does not support IEEE-754 floating point values: baseSCType" + BaseStringRepr _ -> + unsupported sym "SAW backend does not support string values: baseSCType" + BaseComplexRepr -> + unsupported sym "SAW backend does not support complex values: baseSCType" + BaseRealRepr -> + unsupported sym "SAW backend does not support real values: baseSCType" + BaseStructRepr ts -> + SC.scTupleType sc =<< baseSCTypes ts + where + baseSCTypes :: Ctx.Assignment BaseTypeRepr args -> IO [SC.Term] + baseSCTypes Ctx.Empty = return [] + baseSCTypes (xs Ctx.:> x) = + do ts <- baseSCTypes xs + t <- baseSCType sym sc x + return (ts ++ [t]) + +-- | Create a new symbolic variable. +sawCreateVar :: SAWCoreBackend n solver fs + -> String -- ^ the name of the variable + -> SC.Term + -> IO SC.Term +sawCreateVar sym nm tp = do + st <- readIORef (B.sbStateManager sym) + let sc = saw_ctx st + ec <- SC.scFreshEC sc nm tp + t <- SC.scFlatTermF sc (SC.ExtCns ec) + modifyIORef (saw_inputs st) (\xs -> xs Seq.|> ec) + return t + +bindSAWTerm :: SAWCoreBackend n solver fs + -> BaseTypeRepr bt + -> SC.Term + -> IO (B.Expr n bt) +bindSAWTerm sym bt t = do + st <- readIORef $ B.sbStateManager sym + ch_r <- readIORef $ saw_elt_cache_r st + let midx = + case t of + SC.STApp { SC.stAppIndex = idx } -> Just idx + SC.Unshared _ -> Nothing + case midx >>= flip IntMap.lookup ch_r of + Just (Some var) -> do + Just Refl <- return $ testEquality bt (B.exprType var) + return var + Nothing -> do + sbVar@(B.BoundVarExpr bv) <- freshConstant sym emptySymbol bt + B.insertIdxValue (saw_elt_cache st) (B.bvarId bv) (SAWExpr t) + case midx of + Just i -> modifyIORef' (saw_elt_cache_r st) $ IntMap.insert i (Some sbVar) + Nothing -> pure () + return sbVar + +newSAWCoreBackend :: + FloatModeRepr fm -> + SC.SharedContext -> + NonceGenerator IO s -> + IO (SAWCoreBackend s Yices.Connection (Flags fm)) +newSAWCoreBackend fm sc gen = do + inpr <- newIORef Seq.empty + ch <- B.newIdxCache + ch_r <- newIORef IntMap.empty + let feats = Yices.yicesDefaultFeatures + ob_st0 <- initialOnlineBackendState gen feats + let st0 = SAWCoreState + { saw_ctx = sc + , saw_inputs = inpr + , saw_symMap = Map.empty + , saw_elt_cache = ch + , saw_elt_cache_r = ch_r + , saw_online_state = ob_st0 + } + sym <- B.newExprBuilder fm st0 gen + let options = backendOptions ++ onlineBackendOptions ob_st0 ++ Yices.yicesOptions + extendConfig options (getConfiguration sym) + + enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) + let st = st0{ saw_online_state = ob_st0{ onlineEnabled = getOpt enableOpt } } + + writeIORef (B.sbStateManager sym) st + return sym + +-- | Register an interpretation for a symbolic function. This is not +-- used during simulation, but rather, when we translate Crucible +-- values back into SAW. The interpretation function takes a list of +-- arguments in regular (left-to-right) order. +sawRegisterSymFunInterp :: + SAWCoreBackend n solver fs -> + B.ExprSymFn n (B.Expr n) args ret -> + (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> + IO () +sawRegisterSymFunInterp sym f i = + modifyIORef (B.sbStateManager sym) $ \s -> + s { saw_symMap = Map.insert (indexValue (B.symFnId f)) i (saw_symMap s) } + + +sawBackendSharedContext :: SAWCoreBackend n solver fs -> IO SC.SharedContext +sawBackendSharedContext sym = + saw_ctx <$> readIORef (B.sbStateManager sym) + + +toSC :: OnlineSolver solver => + SAWCoreBackend n solver fs -> B.Expr n tp -> IO SC.Term +toSC sym elt = + do st <- readIORef $ B.sbStateManager sym + evaluateExpr sym (saw_ctx st) (saw_elt_cache st) elt + + +-- | Return a shared term with type nat from a SAWExpr. +scAsIntExpr :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + IO SC.Term +scAsIntExpr _ sc (IntToRealSAWExpr (NatToIntSAWExpr (SAWExpr t))) = SC.scNatToInt sc t +scAsIntExpr _ _ (IntToRealSAWExpr (SAWExpr t)) = return t +scAsIntExpr sym _ SAWExpr{} = unsupported sym + "SAWbackend does not support real values." + +-- | Create a Real SAWELT value from a Rational. +-- +-- This fails on non-integer expressions. +scRealLit :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + Rational -> + IO (SAWExpr BaseRealType) +scRealLit sym sc r + | denominator r /= 1 = + unsupported sym "SAW backend does not support real values" + | r >= 0 = + IntToRealSAWExpr . NatToIntSAWExpr . SAWExpr <$> SC.scNat sc (fromInteger (numerator r)) + | otherwise = + IntToRealSAWExpr <$> scIntLit sc (numerator r) + +-- | Create a SAWCore term with type 'Integer' from a Haskell Integer. +scIntLit :: SC.SharedContext -> Integer -> IO (SAWExpr BaseIntegerType) +scIntLit sc i + | i >= 0 = + SAWExpr <$> (SC.scNatToInt sc =<< SC.scNat sc (fromInteger i)) + | otherwise = + SAWExpr <$> (SC.scIntNeg sc =<< SC.scNatToInt sc =<< SC.scNat sc (fromInteger (negate i))) + +-- | Create a SAWCore term with type 'Nat' from a Haskell Nat. +scNatLit :: SC.SharedContext -> Natural -> IO (SAWExpr BaseNatType) +scNatLit sc n = SAWExpr <$> SC.scNat sc n + +scBvLit :: SC.SharedContext -> NatRepr w -> BV.BV w -> IO (SAWExpr (BaseBVType w)) +scBvLit sc w bv = SAWExpr <$> SC.scBvConst sc (natValue w) (BV.asUnsigned bv) + + +scRealCmpop :: + OnlineSolver solver => + (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseBoolType)) -> + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealCmpop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = + intOp sc x y +scRealCmpop _ sym _ _ _ = + unsupported sym "SAW backend does not support real values" + +scRealBinop :: + OnlineSolver solver => + (SC.SharedContext -> SAWExpr BaseIntegerType -> SAWExpr BaseIntegerType -> IO (SAWExpr BaseIntegerType)) -> + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scRealBinop intOp _ sc (IntToRealSAWExpr x) (IntToRealSAWExpr y) = + IntToRealSAWExpr <$> intOp sc x y +scRealBinop _ sym _ _ _ = + unsupported sym "SAW backend does not support real values" + + +scIntBinop :: + (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType)) + {- ^ operation on naturals -} -> + (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseIntegerType) +scIntBinop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = + NatToIntSAWExpr <$> natOp sc x y +scIntBinop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = + SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) +scIntBinop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = + SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) +scIntBinop _natOp intOp sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> intOp sc x y + +scIntCmpop :: + (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseBoolType)) + {- ^ operation on naturals -} -> + (SC.SharedContext -> SC.Term -> SC.Term -> IO SC.Term) {- ^ operation on integers -} -> + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseBoolType) +scIntCmpop natOp _intOp sc (NatToIntSAWExpr x) (NatToIntSAWExpr y) = + natOp sc x y +scIntCmpop _natOp intOp sc (NatToIntSAWExpr (SAWExpr x)) (SAWExpr y) = + SAWExpr <$> join (intOp sc <$> SC.scNatToInt sc x <*> pure y) +scIntCmpop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = + SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) +scIntCmpop _natOp intOp sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> intOp sc x y + +scAddReal :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scAddReal = scRealBinop scAddInt + +scAddInt :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scAddInt = scIntBinop scAddNat SC.scIntAdd + +scAddNat :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scAddNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scAddNat sc x y + + +scMulReal :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scMulReal = scRealBinop scMulInt + +scMulInt :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scMulInt = scIntBinop scMulNat SC.scIntMul + +scMulNat :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scMulNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scMulNat sc x y + +scIteReal :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SC.Term -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseRealType) +scIteReal sym sc p = scRealBinop (\sc' -> scIteInt sc' p) sym sc + +scIteInt :: SC.SharedContext + -> SC.Term + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseIntegerType) +scIteInt sc p = scIntBinop + (\sc' -> scIteNat sc' p) + (\sc' x y -> SC.scIntegerType sc >>= \tp -> SC.scIte sc' tp p x y) + sc + +scIteNat :: SC.SharedContext + -> SC.Term + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseNatType) +scIteNat sc p (SAWExpr x) (SAWExpr y) = + SAWExpr <$> (SC.scNatType sc >>= \tp -> SC.scIte sc tp p x y) + +scIte :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + BaseTypeRepr tp -> + SAWExpr BaseBoolType -> + SAWExpr tp -> + SAWExpr tp -> + IO (SAWExpr tp) +scIte sym sc tp (SAWExpr p) x y = + case tp of + BaseRealRepr -> scIteReal sym sc p x y + BaseNatRepr -> scIteNat sc p x y + BaseIntegerRepr -> scIteInt sc p x y + _ -> + do tp' <- baseSCType sym sc tp + x' <- termOfSAWExpr sym sc x + y' <- termOfSAWExpr sym sc y + SAWExpr <$> SC.scIte sc tp' p x' y' + + +scRealEq :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealEq = scRealCmpop scIntEq + +scIntEq :: SC.SharedContext + -> SAWExpr BaseIntegerType + -> SAWExpr BaseIntegerType + -> IO (SAWExpr BaseBoolType) +scIntEq = scIntCmpop scNatEq SC.scIntEq + +scNatEq :: SC.SharedContext + -> SAWExpr BaseNatType + -> SAWExpr BaseNatType + -> IO (SAWExpr BaseBoolType) +scNatEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scEqualNat sc x y + +scBoolEq :: + SC.SharedContext -> + SAWExpr BaseBoolType -> + SAWExpr BaseBoolType -> + IO (SAWExpr BaseBoolType) +scBoolEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scBoolEq sc x y + +scEq :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + BaseTypeRepr tp -> + SAWExpr tp -> + SAWExpr tp -> + IO (SAWExpr BaseBoolType) +scEq sym sc tp x y = + case tp of + BaseBoolRepr -> scBoolEq sc x y + BaseRealRepr -> scRealEq sym sc x y + BaseNatRepr -> scNatEq sc x y + BaseIntegerRepr -> scIntEq sc x y + BaseBVRepr w -> + do let SAWExpr x' = x + let SAWExpr y' = y + w' <- SC.scNat sc $ fromIntegral (natValue w) + SAWExpr <$> SC.scBvEq sc w' x' y' + _ -> unsupported sym ("SAW backend: equality comparison on unsupported type:" ++ show tp) + + +scAllEq :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + Ctx.Assignment BaseTypeRepr ctx -> + Ctx.Assignment SAWExpr ctx -> + Ctx.Assignment SAWExpr ctx -> + IO (SAWExpr BaseBoolType) +scAllEq _sym sc Ctx.Empty _ _ = SAWExpr <$> SC.scBool sc True +scAllEq sym sc (ctx Ctx.:> tp) (xs Ctx.:> x) (ys Ctx.:> y) + | Ctx.null ctx = scEq sym sc tp x y + | otherwise = + do SAWExpr p <- scAllEq sym sc ctx xs ys + SAWExpr q <- scEq sym sc tp x y + SAWExpr <$> SC.scAnd sc p q + +scRealLe, scRealLt :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr BaseRealType -> + SAWExpr BaseRealType -> + IO (SAWExpr BaseBoolType) +scRealLe = scRealCmpop scIntLe +scRealLt = scRealCmpop scIntLt + +scIntLe, scIntLt :: + SC.SharedContext -> + SAWExpr BaseIntegerType -> + SAWExpr BaseIntegerType -> + IO (SAWExpr BaseBoolType) +scIntLe = scIntCmpop scNatLe SC.scIntLe +scIntLt = scIntCmpop scNatLt SC.scIntLt + +scNatLe, scNatLt :: + SC.SharedContext -> + SAWExpr BaseNatType -> + SAWExpr BaseNatType -> + IO (SAWExpr BaseBoolType) +scNatLe sc (SAWExpr x) (SAWExpr y) = + do lt <- SC.scLtNat sc x y + eq <- SC.scEqualNat sc x y + SAWExpr <$> SC.scOr sc lt eq +scNatLt sc (SAWExpr x) (SAWExpr y) = + SAWExpr <$> SC.scLtNat sc x y + +scBvAdd :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvAdd sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvAdd sc n x y + +scBvNot :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvNot sc w (SAWExpr x) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvNot sc n x + +scBvMul :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvMul sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvMul sc n x y + +scBvAnd :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvAnd sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvAnd sc n x y + +scBvXor :: + SC.SharedContext -> + NatRepr w -> + SAWExpr (BaseBVType w) -> + SAWExpr (BaseBVType w) -> + IO (SAWExpr (BaseBVType w)) +scBvXor sc w (SAWExpr x) (SAWExpr y) = + do n <- SC.scNat sc (natValue w) + SAWExpr <$> SC.scBvXor sc n x y + +termOfSAWExpr :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + SAWExpr tp -> IO SC.Term +termOfSAWExpr sym sc expr = + case expr of + SAWExpr t -> return t + NatToIntSAWExpr (SAWExpr t) -> SC.scNatToInt sc t + IntToRealSAWExpr _ + -> unsupported sym "SAW backend does not support real values" + +applyExprSymFn :: + forall n solver fs args ret. + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + B.ExprSymFn n (B.Expr n) args ret -> + Ctx.Assignment SAWExpr args -> + IO (SAWExpr ret) +applyExprSymFn sym sc fn args = + do st <- readIORef (B.sbStateManager sym) + mk <- + case Map.lookup (indexValue (B.symFnId fn)) (saw_symMap st) of + Nothing -> panic "SAWCore.applyExprSymFn" + [ "Unknown symbolic function." + , "*** Name: " ++ show fn + ] + Just mk -> return mk + ts <- evaluateAsgn args + SAWExpr <$> mk sc (reverse ts) + where + evaluateAsgn :: Ctx.Assignment SAWExpr args' -> IO [SC.Term] + evaluateAsgn Ctx.Empty = return [] + evaluateAsgn (xs Ctx.:> x) = + do vs <- evaluateAsgn xs + v <- termOfSAWExpr sym sc x + return (v : vs) + + +considerSatisfiability :: + OnlineSolver solver => + SAWCoreBackend n solver fs -> + Maybe ProgramLoc -> + B.BoolExpr n -> + IO BranchResult +considerSatisfiability sym mbPloc p = + withSolverProcess' + (\sym' -> saw_online_state <$> readIORef (B.sbStateManager sym')) sym + (pure IndeterminateBranchResult) + $ \proc -> + do pnot <- notPred sym p + let locDesc = case mbPloc of + Just ploc -> show (plSourceLoc ploc) + Nothing -> "(unknown location)" + let rsn = "branch sat: " ++ locDesc + p_res <- checkSatisfiable proc rsn p + pnot_res <- checkSatisfiable proc rsn pnot + case (p_res, pnot_res) of + (Unsat{}, Unsat{}) -> return UnsatisfiableContext + (_ , Unsat{}) -> return (NoBranch True) + (Unsat{}, _ ) -> return (NoBranch False) + _ -> return IndeterminateBranchResult + +{- | Declare that we don't support something or other. +This aborts the current path of execution, and adds a proof +obligation to ensure that we won't get there. +These proof obligations are all tagged with "Unsupported", so that +users of the library can choose if they will try to discharge them, +fail in some other way, or just ignore them. -} +unsupported :: OnlineSolver solver => SAWCoreBackend n solver fs -> String -> IO a +unsupported sym x = addFailedAssertion sym (Unsupported x) + +evaluateExpr :: forall n solver tp fs. + OnlineSolver solver => + SAWCoreBackend n solver fs -> + SC.SharedContext -> + B.IdxCache n SAWExpr -> + B.Expr n tp -> + IO SC.Term +evaluateExpr sym sc cache = f [] + where + -- Evaluate the element, and expect the result to have the same type. + f :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO SC.Term + f env elt = termOfSAWExpr sym sc =<< eval env elt + + eval :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') + eval env elt = B.idxCacheEval cache elt (go env elt) + + realFail :: IO a + realFail = unsupported sym "SAW backend does not support real values" + + cplxFail :: IO a + cplxFail = unsupported sym "SAW backend does not support complex values" + + floatFail :: IO a + floatFail = unsupported sym "SAW backend does not support floating-point values" + + stringFail :: IO a + stringFail = unsupported sym "SAW backend does not support string values" + + unimplemented :: String -> IO a + unimplemented x = unsupported sym $ "SAW backend: not implemented: " ++ x + + go :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') + + go _ (B.BoolExpr b _) = SAWExpr <$> SC.scBool sc b + + go _ (B.SemiRingLiteral sr x _) = + case sr of + B.SemiRingNatRepr -> scNatLit sc x + B.SemiRingBVRepr _ w -> scBvLit sc w x + B.SemiRingIntegerRepr -> scIntLit sc x + B.SemiRingRealRepr -> scRealLit sym sc x + + go _ (B.StringExpr{}) = + unsupported sym "SAW backend does not support string values" + + go env (B.BoundVarExpr bv) = + case B.bvarKind bv of + B.UninterpVarKind -> do + tp <- baseSCType sym sc (B.bvarType bv) + SAWExpr <$> sawCreateVar sym nm tp + where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + B.LatchVarKind -> + unsupported sym "SAW backend does not support latch variables" + B.QuantifierVarKind -> do + case elemIndex (Just $ B.bvarName bv) env of + Nothing -> unsupported sym $ "unbound quantifier variable " <> nm + Just idx -> SAWExpr <$> SC.scLocalVar sc idx + where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + + go env (B.NonceAppExpr p) = + case B.nonceExprApp p of + B.Annotation _tpr _n x -> + eval env x + + B.Forall bvar body -> + case B.bvarType bvar of + BaseBVRepr wrepr -> do + w <- SC.scNat sc $ natValue wrepr + ty <- SC.scVecType sc w =<< SC.scBoolType sc + SAWExpr <$> + (SC.scBvForall sc w + =<< SC.scLambda sc nm ty =<< f (Just (B.bvarName bvar):env) body) + where nm = solverSymbolAsText $ B.bvarName bvar + _ -> unsupported sym "SAW backend only supports universal quantifiers over bitvectors" + B.Exists{} -> + unsupported sym "SAW backend does not support existential quantifiers" + B.ArrayFromFn{} -> unimplemented "ArrayFromFn" + B.MapOverArrays{} -> unimplemented "MapOverArrays" + B.ArrayTrueOnEntries{} -> unimplemented "ArrayTrueOnEntries" + B.FnApp fn asgn -> + do args <- traverseFC (eval env) asgn + applyExprSymFn sym sc fn args + + go env a0@(B.AppExpr a) = + let nyi = unsupported sym $ + "Expression form not yet implemented in SAWCore backend:\n" + ++ show a0 + in + case B.appExprApp a of + B.BaseIte bt _ c xe ye -> join (scIte sym sc bt <$> eval env c <*> eval env xe <*> eval env ye) + B.BaseEq bt xe ye -> join (scEq sym sc bt <$> eval env xe <*> eval env ye) + + B.SemiRingLe sr xe ye -> + case sr of + B.OrderedSemiRingRealRepr -> join (scRealLe sym sc <$> eval env xe <*> eval env ye) + B.OrderedSemiRingIntegerRepr -> join (scIntLe sc <$> eval env xe <*> eval env ye) + B.OrderedSemiRingNatRepr -> join (scNatLe sc <$> eval env xe <*> eval env ye) + + B.NotPred x -> + goNeg env x + + B.ConjPred xs -> + case BM.viewBoolMap xs of + BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc True + BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc False + BM.BoolMapTerms (t:|ts) -> + let pol (x,BM.Positive) = f env x + pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x + in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts) + + B.SemiRingProd pd -> + case WSum.prodRepr pd of + B.SemiRingRealRepr -> + do pd' <- WSum.prodEvalM (scMulReal sym sc) (eval env) pd + maybe (scRealLit sym sc 1) return pd' + B.SemiRingIntegerRepr -> + do pd' <- WSum.prodEvalM (scMulInt sc) (eval env) pd + maybe (scIntLit sc 1) return pd' + B.SemiRingNatRepr -> + do pd' <- WSum.prodEvalM (scMulNat sc) (eval env) pd + maybe (scNatLit sc 1) return pd' + B.SemiRingBVRepr B.BVArithRepr w -> + do n <- SC.scNat sc (natValue w) + pd' <- WSum.prodEvalM (SC.scBvMul sc n) (f env) pd + maybe (scBvLit sc w (BV.one w)) (return . SAWExpr) pd' + B.SemiRingBVRepr B.BVBitsRepr w -> + do n <- SC.scNat sc (natValue w) + pd' <- WSum.prodEvalM (SC.scBvAnd sc n) (f env) pd + maybe (scBvLit sc w (BV.maxUnsigned w)) (return . SAWExpr) pd' + + B.SemiRingSum ss -> + case WSum.sumRepr ss of + B.SemiRingRealRepr -> WSum.evalM add smul (scRealLit sym sc) ss + where add x y = scAddReal sym sc x y + smul 1 e = eval env e + smul sm e = join $ scMulReal sym sc <$> scRealLit sym sc sm <*> eval env e + B.SemiRingIntegerRepr -> WSum.evalM add smul (scIntLit sc) ss + where add x y = scAddInt sc x y + smul 1 e = eval env e + smul sm e = join $ scMulInt sc <$> scIntLit sc sm <*> eval env e + B.SemiRingNatRepr -> WSum.evalM add smul (scNatLit sc) ss + where add x y = scAddNat sc x y + smul 1 e = eval env e + smul sm e = join $ scMulNat sc <$> scNatLit sc sm <*> eval env e + B.SemiRingBVRepr B.BVArithRepr w -> WSum.evalM add smul (scBvLit sc w) ss + where add x y = scBvAdd sc w x y + smul (BV.BV 1) e = eval env e + smul sm e = join (scBvMul sc w <$> scBvLit sc w sm <*> eval env e) + B.SemiRingBVRepr B.BVBitsRepr w + | ss^.WSum.sumOffset == one -> scBvNot sc w =<< bitwise_eval (ss & WSum.sumOffset .~ BV.zero w) + | otherwise -> bitwise_eval ss + + where one = BV.maxUnsigned w + bitwise_eval = WSum.evalM add smul (scBvLit sc w) + add x y = scBvXor sc w x y + smul sm e + | sm == one = eval env e + | otherwise = join (scBvAnd sc w <$> scBvLit sc w sm <*> eval env e) + + B.RealIsInteger{} -> unsupported sym "SAW backend does not support real values" + + B.BVOrBits w bs -> + do n <- SC.scNat sc (natValue w) + bs' <- traverse (f env) (B.bvOrToList bs) + case bs' of + [] -> scBvLit sc w (BV.zero w) + x:xs -> SAWExpr <$> foldM (SC.scBvOr sc n) x xs + + B.BVFill w p -> + do bit <- SC.scBoolType sc + n <- SC.scNat sc (natValue w) + x <- f env p + SAWExpr <$> SC.scGlobalApply sc (SC.mkIdent SC.preludeName "replicate") [n, bit, x] + + B.BVTestBit i bv -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth bv)) + bit <- SC.scBoolType sc + -- NB, SAWCore's `scAt` is big endian + let j = natValue (bvWidth bv) - i - 1 + join (SC.scAt sc w bit <$> f env bv <*> SC.scNat sc j) + + B.BVSlt x y -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvSLt sc w <$> f env x <*> f env y) + B.BVUlt x y -> fmap SAWExpr $ do + w <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvULt sc w <$> f env x <*> f env y) + + B.BVUnaryTerm{} -> unsupported sym "SAW backend does not support the unary bitvector representation" + + B.BVUdiv _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvUDiv sc n <$> f env x <*> f env y) + B.BVUrem _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + join (SC.scBvURem sc n <$> f env x <*> f env y) + B.BVSdiv _ x y -> fmap SAWExpr $ do + -- NB: bvSDiv applies 'Succ' to its width argument, so we + -- need to subtract 1 to make the types match. + n <- SC.scNat sc (natValue (bvWidth x) - 1) + join (SC.scBvSDiv sc n <$> f env x <*> f env y) + B.BVSrem _ x y -> fmap SAWExpr $ do + -- NB: bvSDiv applies 'Succ' to its width argument, so we + -- need to subtract 1 to make the types match. + n <- SC.scNat sc (natValue (bvWidth x) - 1) + join (SC.scBvSRem sc n <$> f env x <*> f env y) + B.BVShl _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + n <- SC.scNat sc w + join (SC.scBvShl sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVLshr _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + n <- SC.scNat sc w + join (SC.scBvShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVAshr _ x y -> fmap SAWExpr $ do + let w = natValue (bvWidth x) + -- NB: bvSShr applies a `Succ` to its width argument, so we subtract + -- 1 here to make things match up. + n <- SC.scNat sc (w - 1) + join (SC.scBvSShr sc n <$> f env x <*> (SC.scBvToNat sc w =<< f env y)) + B.BVRol w x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue w) + bit <- SC.scBoolType sc + x' <- f env x + y' <- SC.scBvToNat sc (natValue w) =<< f env y + SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateL") [n,bit,x',y'] + B.BVRor w x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue w) + bit <- SC.scBoolType sc + x' <- f env x + y' <- SC.scBvToNat sc (natValue w) =<< f env y + SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateR") [n,bit,x',y'] + B.BVConcat _ x y -> fmap SAWExpr $ do + n <- SC.scNat sc (natValue (bvWidth x)) + m <- SC.scNat sc (natValue (bvWidth y)) + t <- SC.scBoolType sc + join (SC.scAppend sc t n m <$> f env x <*> f env y) + B.BVSelect start num x -> fmap SAWExpr $ do + i <- SC.scNat sc (natValue (bvWidth x) - natValue num - natValue start) + n <- SC.scNat sc (natValue num) + o <- SC.scNat sc (natValue start) + t <- SC.scBoolType sc + x' <- f env x + SC.scSlice sc t i n o x' + B.BVZext w' x -> fmap SAWExpr $ do + let w = bvWidth x + n <- SC.scNat sc (natValue w) + m <- SC.scNat sc (natValue w' - natValue w) + x' <- f env x + SC.scBvUExt sc m n x' + B.BVSext w' x -> fmap SAWExpr $ do + let w = bvWidth x + -- NB: width - 1 to make SAWCore types work out + n <- SC.scNat sc (natValue w - 1) + m <- SC.scNat sc (natValue w' - natValue w) + x' <- f env x + SC.scBvSExt sc m n x' + B.BVPopcount w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvPopcount sc n x' + B.BVCountLeadingZeros w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvCountLeadingZeros sc n x' + B.BVCountTrailingZeros w x -> + do n <- SC.scNat sc (natValue w) + x' <- f env x + SAWExpr <$> SC.scBvCountTrailingZeros sc n x' + + -- Note: SAWCore supports only unidimensional arrays. As a result, What4 multidimensional + -- arrays cannot be translated to SAWCore. + B.ArrayMap indexTypes range updates arr + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + SAWExpr <$> foldM + (\sc_acc_arr (Ctx.Empty Ctx.:> idx_lit, elm) -> + do sc_idx <- f env =<< indexLit sym idx_lit + sc_elm <- f env elm + SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_acc_arr sc_idx sc_elm) + sc_arr + (AUM.toList updates) + | otherwise -> unimplemented "multidimensional ArrayMap" + + B.ConstantArray indexTypes range v + | Ctx.Empty Ctx.:> idx_type <- indexTypes -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_elm <- f env v + SAWExpr <$> SC.scArrayConstant sc sc_idx_type sc_elm_type sc_elm + | otherwise -> unimplemented "multidimensional ConstantArray" + + B.SelectArray range arr indexTerms + | Ctx.Empty Ctx.:> idx <- indexTerms + , idx_type <- exprType idx -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + sc_idx <- f env idx + SAWExpr <$> SC.scArrayLookup sc sc_idx_type sc_elm_type sc_arr sc_idx + | otherwise -> unimplemented "multidimensional SelectArray" + + B.UpdateArray range indexTypes arr indexTerms v + | Ctx.Empty Ctx.:> idx_type <- indexTypes + , Ctx.Empty Ctx.:> idx <- indexTerms -> + do sc_idx_type <- baseSCType sym sc idx_type + sc_elm_type <- baseSCType sym sc range + sc_arr <- f env arr + sc_idx <- f env idx + sc_elm <- f env v + SAWExpr <$> SC.scArrayUpdate sc sc_idx_type sc_elm_type sc_arr sc_idx sc_elm + | otherwise -> unimplemented "multidimensional UpdateArray" + + B.CopyArray w a_repr dest_arr dest_idx src_arr src_idx len -> + do sc_w <- SC.scNat sc (natValue w) + sc_a <- baseSCType sym sc a_repr + sc_dest_arr <- f env dest_arr + sc_dest_idx <- f env dest_idx + sc_src_arr <- f env src_arr + sc_src_idx <- f env src_idx + sc_len <- f env len + SAWExpr <$> SC.scArrayCopy sc sc_w sc_a sc_dest_arr sc_dest_idx sc_src_arr sc_src_idx sc_len + + B.SetArray w a_repr arr idx val len -> + do sc_w <- SC.scNat sc (natValue w) + sc_a <- baseSCType sym sc a_repr + sc_arr <- f env arr + sc_idx <- f env idx + sc_val <- f env val + sc_len <- f env len + SAWExpr <$> SC.scArraySet sc sc_w sc_a sc_arr sc_idx sc_val sc_len + + B.NatToInteger x -> NatToIntSAWExpr <$> eval env x + B.IntegerToNat x -> + eval env x >>= \case + NatToIntSAWExpr z -> return z + SAWExpr z -> SAWExpr <$> (SC.scIntToNat sc z) + + B.NatDiv x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scDivNat sc x' y' + + B.NatMod x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scModNat sc x' y' + + B.IntDiv x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scIntDiv sc x' y' + B.IntMod x y -> + do x' <- f env x + y' <- f env y + SAWExpr <$> SC.scIntMod sc x' y' + B.IntAbs x -> + eval env x >>= \case + NatToIntSAWExpr z -> return (NatToIntSAWExpr z) + SAWExpr z -> SAWExpr <$> (SC.scIntAbs sc z) + + B.IntDivisible x 0 -> + do x' <- f env x + SAWExpr <$> (SC.scIntEq sc x' =<< SC.scIntegerConst sc 0) + B.IntDivisible x k -> + do x' <- f env x + k' <- SC.scIntegerConst sc (toInteger k) + z <- SC.scIntMod sc x' k' + SAWExpr <$> (SC.scIntEq sc z =<< SC.scIntegerConst sc 0) + + B.BVToNat x -> + let n = natValue (bvWidth x) in + SAWExpr <$> (SC.scBvToNat sc n =<< f env x) + + B.IntegerToBV x w -> + do n <- SC.scNat sc (natValue w) + SAWExpr <$> (SC.scIntToBv sc n =<< f env x) + + B.BVToInteger x -> + do n <- SC.scNat sc (natValue (bvWidth x)) + SAWExpr <$> (SC.scBvToInt sc n =<< f env x) + + B.SBVToInteger x -> + do n <- SC.scNat sc (natValue (bvWidth x)) + SAWExpr <$> (SC.scSbvToInt sc n =<< f env x) + + -- Proper support for real and complex numbers will require additional + -- work on the SAWCore side + B.IntegerToReal x -> IntToRealSAWExpr . SAWExpr <$> f env x + B.RealToInteger x -> + eval env x >>= \case + IntToRealSAWExpr x' -> return x' + _ -> realFail + + ------------------------------------------------------------------------ + -- Floating point operations + + B.FloatPZero{} -> floatFail + B.FloatNZero{} -> floatFail + B.FloatNaN{} -> floatFail + B.FloatPInf{} -> floatFail + B.FloatNInf{} -> floatFail + B.FloatNeg{} -> floatFail + B.FloatAbs{} -> floatFail + B.FloatSqrt{} -> floatFail + B.FloatAdd{} -> floatFail + B.FloatSub{} -> floatFail + B.FloatMul{} -> floatFail + B.FloatDiv{} -> floatFail + B.FloatRem{} -> floatFail + B.FloatMin{} -> floatFail + B.FloatMax{} -> floatFail + B.FloatFMA{} -> floatFail + B.FloatFpEq{} -> floatFail + B.FloatFpNe{} -> floatFail + B.FloatLe{} -> floatFail + B.FloatLt{} -> floatFail + B.FloatIsNaN{} -> floatFail + B.FloatIsInf{} -> floatFail + B.FloatIsZero{} -> floatFail + B.FloatIsPos{} -> floatFail + B.FloatIsNeg{} -> floatFail + B.FloatIsSubnorm{} -> floatFail + B.FloatIsNorm{} -> floatFail + B.FloatCast{} -> floatFail + B.FloatRound{} -> floatFail + B.FloatFromBinary{} -> floatFail + B.BVToFloat{} -> floatFail + B.SBVToFloat{} -> floatFail + B.RealToFloat{} -> floatFail + B.FloatToBV{} -> floatFail + B.FloatToSBV{} -> floatFail + B.FloatToReal{} -> floatFail + B.FloatToBinary{} -> floatFail + + B.RoundReal{} -> realFail + B.RoundEvenReal{} -> realFail + B.FloorReal{} -> realFail + B.CeilReal{} -> realFail + B.RealDiv{} -> realFail + B.RealSqrt{} -> realFail + B.Pi{} -> realFail + B.RealSin{} -> realFail + B.RealCos{} -> realFail + B.RealSinh{} -> realFail + B.RealCosh{} -> realFail + B.RealExp{} -> realFail + B.RealLog{} -> realFail + B.RealATan2{} -> realFail + + B.Cplx{} -> cplxFail + B.RealPart{} -> cplxFail + B.ImagPart{} -> cplxFail + + B.StringLength{} -> stringFail + B.StringAppend{} -> stringFail + B.StringContains{} -> stringFail + B.StringIsPrefixOf{} -> stringFail + B.StringIsSuffixOf{} -> stringFail + B.StringIndexOf{} -> stringFail + B.StringSubstring{} -> stringFail + + B.StructCtor{} -> nyi -- FIXME + B.StructField{} -> nyi -- FIXME + + -- returns the logical negation of the result of 'go' + -- negations are pushed inside conjunctions and less-than-or-equal + goNeg :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) + goNeg env expr = + case expr of + -- negation of (x /\ y) becomes (~x \/ ~y) + B.AppExpr (B.appExprApp -> B.ConjPred xs) -> + case BM.viewBoolMap xs of + BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc False + BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc True + BM.BoolMapTerms (t:|ts) -> + let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x + pol (x, BM.Negative) = f env x + in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts) + _ -> goNegAtom env expr + + -- returns the logical negation of the result of 'go' + -- negations are pushed inside less-than-or-equal + goNegAtom :: [Maybe SolverSymbol] -> B.Expr n BaseBoolType -> IO (SAWExpr BaseBoolType) + goNegAtom env expr = + case expr of + -- negation of (x <= y) becomes (y < x) + B.AppExpr (B.appExprApp -> B.SemiRingLe sr xe ye) -> + case sr of + B.OrderedSemiRingRealRepr -> join (scRealLt sym sc <$> eval env ye <*> eval env xe) + B.OrderedSemiRingIntegerRepr -> join (scIntLt sc <$> eval env ye <*> eval env xe) + B.OrderedSemiRingNatRepr -> join (scNatLt sc <$> eval env ye <*> eval env xe) + _ -> SAWExpr <$> (SC.scNot sc =<< f env expr) + +withSolverProcess :: + OnlineSolver solver => + SAWCoreBackend scope solver fs -> + IO a -> + (SolverProcess scope solver -> IO a) -> + IO a +withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (B.sbStateManager sym')) + +withSolverConn :: + OnlineSolver solver => + SAWCoreBackend scope solver fs -> + (WriterConn scope solver -> IO ()) -> + IO () +withSolverConn sym k = withSolverProcess sym (pure ()) (k . solverConn) + + +getAssumptionStack :: + SAWCoreBackend s solver fs -> + IO (AssumptionStack (B.BoolExpr s) AssumptionReason SimError) +getAssumptionStack sym = + (assumptionStack . saw_online_state) <$> readIORef (B.sbStateManager sym) + + +-- TODO! we should find a better way to share implementations with `OnlineBackend` +instance OnlineSolver solver => IsBoolSolver (SAWCoreBackend n solver fs) where + + addDurableProofObligation sym a = + AS.addProofObligation a =<< getAssumptionStack sym + + addAssumption sym a = + let cond = asConstantPred (a^.labeledPred) + in case cond of + Just False -> abortExecBecause (AssumedFalse (a^.labeledPredMsg)) + _ -> -- Send assertion to the solver, unless it is trivial. + -- NB, don't add the assumption to the assumption stack unless + -- the solver assumptions succeeded + do withSolverConn sym $ \conn -> + case cond of + Just True -> return () + _ -> SMT.assume conn (a^.labeledPred) + + -- Record assumption, even if trivial. + -- This allows us to keep track of the full path we are on. + AS.assume a =<< getAssumptionStack sym + + addAssumptions sym a = + -- NB, don't add the assumption to the assumption stack unless + -- the solver assumptions succeeded + do withSolverConn sym $ \conn -> + -- Tell the solver of assertions + mapM_ (SMT.assume conn . view labeledPred) (toList a) + -- Add assertions to list + stk <- getAssumptionStack sym + AS.appendAssumptions a stk + + getPathCondition sym = + do stk <- getAssumptionStack sym + ps <- AS.collectAssumptions stk + andAllOf sym (folded.labeledPred) ps + + collectAssumptions sym = + AS.collectAssumptions =<< getAssumptionStack sym + + pushAssumptionFrame sym = + do -- NB, don't push a frame in the assumption stack unless + -- pushing to the solver succeeded + withSolverProcess sym (pure ()) push + AS.pushFrame =<< getAssumptionStack sym + + popAssumptionFrame sym ident = + -- NB, pop the frame whether or not the solver pop succeeds + do frm <- AS.popFrame ident =<< getAssumptionStack sym + withSolverProcess sym (pure ()) pop + return frm + + popUntilAssumptionFrame sym ident = + -- NB, pop the frames whether or not the solver pop succeeds + do n <- AS.popFramesUntil ident =<< getAssumptionStack sym + withSolverProcess sym (pure ()) $ \proc -> + forM_ [0..(n-1)] $ \_ -> pop proc + + popAssumptionFrameAndObligations sym ident = do + -- NB, pop the frames whether or not the solver pop succeeds + do frmAndGls <- AS.popFrameAndGoals ident =<< getAssumptionStack sym + withSolverProcess sym (pure ()) pop + return frmAndGls + + getProofObligations sym = + do stk <- getAssumptionStack sym + AS.getProofObligations stk + + clearProofObligations sym = + do stk <- getAssumptionStack sym + AS.clearProofObligations stk + + saveAssumptionState sym = + do stk <- getAssumptionStack sym + AS.saveAssumptionStack stk + + restoreAssumptionState sym gc = + do st <- saw_online_state <$> readIORef (B.sbStateManager sym) + restoreSolverState gc st + + -- restore the previous assumption stack + stk <- getAssumptionStack sym + AS.restoreAssumptionStack gc stk From b204e9edcd0960b775dc9f87d8e4b94c7e0fed88 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 9 Apr 2025 21:40:44 -0400 Subject: [PATCH 07/22] Build changes for adding CompatSAWCore.hs --- saw-script.cabal | 2 ++ src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/saw-script.cabal b/saw-script.cabal index 83a122ac25..8f3b17139b 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -157,6 +157,8 @@ library SAWScript.HeapsterBuiltins + SAWScript.Crucible.CrucibleSAW.SAWCore + SAWScript.Crucible.Common SAWScript.Crucible.Common.MethodSpec SAWScript.Crucible.Common.Override diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index f04f1605a0..53882cf70a 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -20,7 +20,8 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ViewPatterns #-} -module Lang.Crucible.Backend.SAWCore where +--module Lang.Crucible.Backend.SAWCore where +module SAWScript.Crucible.CrucibleSAW.SAWCore where import Control.Exception ( bracket ) import Control.Lens From 8281ad796ee8bd5f3a0e915d1c4fe411bed1f6b3 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 08/22] CrucibleSAW: remove references to What4 nats, which are gone --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 45 +++++++++++++------ 2 files changed, 33 insertions(+), 13 deletions(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 53882cf70a..fe4ad71139 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -105,7 +105,7 @@ data SAWExpr (bt :: BaseType) where IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType -- This is a SAWCore term that represents a natural number, but has an -- implicit nat-to-integer conversion. - NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType + --NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState solver fs) fs @@ -159,7 +159,6 @@ baseSCType sym sc bt = case bt of BaseBoolRepr -> SC.scBoolType sc BaseBVRepr w -> SC.scBitvector sc $ fromIntegral (natValue w) - BaseNatRepr -> SC.scNatType sc BaseIntegerRepr -> SC.scIntegerType sc BaseArrayRepr indexTypes range | Ctx.Empty Ctx.:> idx_type <- indexTypes -> @@ -278,6 +277,7 @@ toSC sym elt = -- | Return a shared term with type nat from a SAWExpr. +{- scAsIntExpr :: OnlineSolver solver => SAWCoreBackend n solver fs -> @@ -288,6 +288,7 @@ scAsIntExpr _ sc (IntToRealSAWExpr (NatToIntSAWExpr (SAWExpr t))) = SC.scNatToIn scAsIntExpr _ _ (IntToRealSAWExpr (SAWExpr t)) = return t scAsIntExpr sym _ SAWExpr{} = unsupported sym "SAWbackend does not support real values." +-} -- | Create a Real SAWELT value from a Rational. -- @@ -301,8 +302,6 @@ scRealLit :: scRealLit sym sc r | denominator r /= 1 = unsupported sym "SAW backend does not support real values" - | r >= 0 = - IntToRealSAWExpr . NatToIntSAWExpr . SAWExpr <$> SC.scNat sc (fromInteger (numerator r)) | otherwise = IntToRealSAWExpr <$> scIntLit sc (numerator r) @@ -315,8 +314,8 @@ scIntLit sc i SAWExpr <$> (SC.scIntNeg sc =<< SC.scNatToInt sc =<< SC.scNat sc (fromInteger (negate i))) -- | Create a SAWCore term with type 'Nat' from a Haskell Nat. -scNatLit :: SC.SharedContext -> Natural -> IO (SAWExpr BaseNatType) -scNatLit sc n = SAWExpr <$> SC.scNat sc n +--scNatLit :: SC.SharedContext -> Natural -> IO (SAWExpr BaseNatType) +--scNatLit sc n = SAWExpr <$> SC.scNat sc n scBvLit :: SC.SharedContext -> NatRepr w -> BV.BV w -> IO (SAWExpr (BaseBVType w)) scBvLit sc w bv = SAWExpr <$> SC.scBvConst sc (natValue w) (BV.asUnsigned bv) @@ -349,6 +348,7 @@ scRealBinop _ sym _ _ _ = unsupported sym "SAW backend does not support real values" +{- scIntBinop :: (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType)) {- ^ operation on naturals -} -> @@ -365,7 +365,9 @@ scIntBinop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) scIntBinop _natOp intOp sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> intOp sc x y +-} +{- scIntCmpop :: (SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseBoolType)) {- ^ operation on naturals -} -> @@ -382,6 +384,7 @@ scIntCmpop _natOp intOp sc (SAWExpr x) (NatToIntSAWExpr (SAWExpr y)) = SAWExpr <$> join (intOp sc <$> pure x <*> SC.scNatToInt sc y) scIntCmpop _natOp intOp sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> intOp sc x y +-} scAddReal :: OnlineSolver solver => @@ -398,11 +401,13 @@ scAddInt :: SC.SharedContext -> IO (SAWExpr BaseIntegerType) scAddInt = scIntBinop scAddNat SC.scIntAdd +{- scAddNat :: SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType) scAddNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scAddNat sc x y +-} scMulReal :: @@ -420,11 +425,13 @@ scMulInt :: SC.SharedContext -> IO (SAWExpr BaseIntegerType) scMulInt = scIntBinop scMulNat SC.scIntMul +{- scMulNat :: SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseNatType) scMulNat sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scMulNat sc x y +-} scIteReal :: OnlineSolver solver => @@ -446,6 +453,7 @@ scIteInt sc p = scIntBinop (\sc' x y -> SC.scIntegerType sc >>= \tp -> SC.scIte sc' tp p x y) sc +{- scIteNat :: SC.SharedContext -> SC.Term -> SAWExpr BaseNatType @@ -453,6 +461,7 @@ scIteNat :: SC.SharedContext -> IO (SAWExpr BaseNatType) scIteNat sc p (SAWExpr x) (SAWExpr y) = SAWExpr <$> (SC.scNatType sc >>= \tp -> SC.scIte sc tp p x y) +-} scIte :: OnlineSolver solver => @@ -466,7 +475,6 @@ scIte :: scIte sym sc tp (SAWExpr p) x y = case tp of BaseRealRepr -> scIteReal sym sc p x y - BaseNatRepr -> scIteNat sc p x y BaseIntegerRepr -> scIteInt sc p x y _ -> do tp' <- baseSCType sym sc tp @@ -490,11 +498,13 @@ scIntEq :: SC.SharedContext -> IO (SAWExpr BaseBoolType) scIntEq = scIntCmpop scNatEq SC.scIntEq +{- scNatEq :: SC.SharedContext -> SAWExpr BaseNatType -> SAWExpr BaseNatType -> IO (SAWExpr BaseBoolType) scNatEq sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scEqualNat sc x y +-} scBoolEq :: SC.SharedContext -> @@ -515,7 +525,6 @@ scEq sym sc tp x y = case tp of BaseBoolRepr -> scBoolEq sc x y BaseRealRepr -> scRealEq sym sc x y - BaseNatRepr -> scNatEq sc x y BaseIntegerRepr -> scIntEq sc x y BaseBVRepr w -> do let SAWExpr x' = x @@ -559,6 +568,7 @@ scIntLe, scIntLt :: scIntLe = scIntCmpop scNatLe SC.scIntLe scIntLt = scIntCmpop scNatLt SC.scIntLt +{- scNatLe, scNatLt :: SC.SharedContext -> SAWExpr BaseNatType -> @@ -570,6 +580,7 @@ scNatLe sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scOr sc lt eq scNatLt sc (SAWExpr x) (SAWExpr y) = SAWExpr <$> SC.scLtNat sc x y +-} scBvAdd :: SC.SharedContext -> @@ -628,7 +639,7 @@ termOfSAWExpr :: termOfSAWExpr sym sc expr = case expr of SAWExpr t -> return t - NatToIntSAWExpr (SAWExpr t) -> SC.scNatToInt sc t + --NatToIntSAWExpr (SAWExpr t) -> SC.scNatToInt sc t IntToRealSAWExpr _ -> unsupported sym "SAW backend does not support real values" @@ -730,7 +741,7 @@ evaluateExpr sym sc cache = f [] go _ (B.SemiRingLiteral sr x _) = case sr of - B.SemiRingNatRepr -> scNatLit sc x + --B.SemiRingNatRepr -> scNatLit sc x B.SemiRingBVRepr _ w -> scBvLit sc w x B.SemiRingIntegerRepr -> scIntLit sc x B.SemiRingRealRepr -> scRealLit sym sc x @@ -789,7 +800,7 @@ evaluateExpr sym sc cache = f [] case sr of B.OrderedSemiRingRealRepr -> join (scRealLe sym sc <$> eval env xe <*> eval env ye) B.OrderedSemiRingIntegerRepr -> join (scIntLe sc <$> eval env xe <*> eval env ye) - B.OrderedSemiRingNatRepr -> join (scNatLe sc <$> eval env xe <*> eval env ye) + --B.OrderedSemiRingNatRepr -> join (scNatLe sc <$> eval env xe <*> eval env ye) B.NotPred x -> goNeg env x @@ -811,9 +822,11 @@ evaluateExpr sym sc cache = f [] B.SemiRingIntegerRepr -> do pd' <- WSum.prodEvalM (scMulInt sc) (eval env) pd maybe (scIntLit sc 1) return pd' +{- B.SemiRingNatRepr -> do pd' <- WSum.prodEvalM (scMulNat sc) (eval env) pd maybe (scNatLit sc 1) return pd' +-} B.SemiRingBVRepr B.BVArithRepr w -> do n <- SC.scNat sc (natValue w) pd' <- WSum.prodEvalM (SC.scBvMul sc n) (f env) pd @@ -833,10 +846,12 @@ evaluateExpr sym sc cache = f [] where add x y = scAddInt sc x y smul 1 e = eval env e smul sm e = join $ scMulInt sc <$> scIntLit sc sm <*> eval env e +{- B.SemiRingNatRepr -> WSum.evalM add smul (scNatLit sc) ss where add x y = scAddNat sc x y smul 1 e = eval env e smul sm e = join $ scMulNat sc <$> scNatLit sc sm <*> eval env e +-} B.SemiRingBVRepr B.BVArithRepr w -> WSum.evalM add smul (scBvLit sc w) ss where add x y = scBvAdd sc w x y smul (BV.BV 1) e = eval env e @@ -1027,6 +1042,7 @@ evaluateExpr sym sc cache = f [] sc_len <- f env len SAWExpr <$> SC.scArraySet sc sc_w sc_a sc_arr sc_idx sc_val sc_len +{- B.NatToInteger x -> NatToIntSAWExpr <$> eval env x B.IntegerToNat x -> eval env x >>= \case @@ -1042,6 +1058,7 @@ evaluateExpr sym sc cache = f [] do x' <- f env x y' <- f env y SAWExpr <$> SC.scModNat sc x' y' +-} B.IntDiv x y -> do x' <- f env x @@ -1053,7 +1070,7 @@ evaluateExpr sym sc cache = f [] SAWExpr <$> SC.scIntMod sc x' y' B.IntAbs x -> eval env x >>= \case - NatToIntSAWExpr z -> return (NatToIntSAWExpr z) + --NatToIntSAWExpr z -> return (NatToIntSAWExpr z) SAWExpr z -> SAWExpr <$> (SC.scIntAbs sc z) B.IntDivisible x 0 -> @@ -1065,9 +1082,11 @@ evaluateExpr sym sc cache = f [] z <- SC.scIntMod sc x' k' SAWExpr <$> (SC.scIntEq sc z =<< SC.scIntegerConst sc 0) +{- B.BVToNat x -> let n = natValue (bvWidth x) in SAWExpr <$> (SC.scBvToNat sc n =<< f env x) +-} B.IntegerToBV x w -> do n <- SC.scNat sc (natValue w) @@ -1186,7 +1205,7 @@ evaluateExpr sym sc cache = f [] case sr of B.OrderedSemiRingRealRepr -> join (scRealLt sym sc <$> eval env ye <*> eval env xe) B.OrderedSemiRingIntegerRepr -> join (scIntLt sc <$> eval env ye <*> eval env xe) - B.OrderedSemiRingNatRepr -> join (scNatLt sc <$> eval env ye <*> eval env xe) + --B.OrderedSemiRingNatRepr -> join (scNatLt sc <$> eval env ye <*> eval env xe) _ -> SAWExpr <$> (SC.scNot sc =<< f env expr) withSolverProcess :: From 8309cf44241e64d86763504ba5d879ddd6e66926 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 09/22] CrucibleSAW: sbStateManager -> userState (What4 interface) --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 30 +++++++++---------- 2 files changed, 15 insertions(+), 16 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index fe4ad71139..1817020aa7 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -119,16 +119,16 @@ type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState solver fs) fs -- state of these fields is restored. inFreshNamingContext :: SAWCoreBackend n solver fs -> IO a -> IO a inFreshNamingContext sym f = - do old <- readIORef (B.sbStateManager sym) + do old <- readIORef (B.userState sym) bracket (mkNew (B.exprCounter sym) old) (restore old) action where action new = - do writeIORef (B.sbStateManager sym) new + do writeIORef (B.userState sym) new f restore old _new = - do writeIORef (B.sbStateManager sym) old + do writeIORef (B.userState sym) old mkNew _gen old = do ch <- B.newIdxCache @@ -146,7 +146,7 @@ inFreshNamingContext sym f = getInputs :: SAWCoreBackend n solver fs -> IO (Seq (SC.ExtCns SC.Term)) getInputs sym = - do st <- readIORef (B.sbStateManager sym) + do st <- readIORef (B.userState sym) readIORef (saw_inputs st) baseSCType :: @@ -191,7 +191,7 @@ sawCreateVar :: SAWCoreBackend n solver fs -> SC.Term -> IO SC.Term sawCreateVar sym nm tp = do - st <- readIORef (B.sbStateManager sym) + st <- readIORef (B.userState sym) let sc = saw_ctx st ec <- SC.scFreshEC sc nm tp t <- SC.scFlatTermF sc (SC.ExtCns ec) @@ -203,7 +203,7 @@ bindSAWTerm :: SAWCoreBackend n solver fs -> SC.Term -> IO (B.Expr n bt) bindSAWTerm sym bt t = do - st <- readIORef $ B.sbStateManager sym + st <- readIORef $ B.userState sym ch_r <- readIORef $ saw_elt_cache_r st let midx = case t of @@ -247,7 +247,7 @@ newSAWCoreBackend fm sc gen = do enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) let st = st0{ saw_online_state = ob_st0{ onlineEnabled = getOpt enableOpt } } - writeIORef (B.sbStateManager sym) st + writeIORef (B.userState sym) st return sym -- | Register an interpretation for a symbolic function. This is not @@ -260,19 +260,19 @@ sawRegisterSymFunInterp :: (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> IO () sawRegisterSymFunInterp sym f i = - modifyIORef (B.sbStateManager sym) $ \s -> + modifyIORef (B.userState sym) $ \s -> s { saw_symMap = Map.insert (indexValue (B.symFnId f)) i (saw_symMap s) } sawBackendSharedContext :: SAWCoreBackend n solver fs -> IO SC.SharedContext sawBackendSharedContext sym = - saw_ctx <$> readIORef (B.sbStateManager sym) + saw_ctx <$> readIORef (B.userState sym) toSC :: OnlineSolver solver => SAWCoreBackend n solver fs -> B.Expr n tp -> IO SC.Term toSC sym elt = - do st <- readIORef $ B.sbStateManager sym + do st <- readIORef $ B.userState sym evaluateExpr sym (saw_ctx st) (saw_elt_cache st) elt @@ -652,7 +652,7 @@ applyExprSymFn :: Ctx.Assignment SAWExpr args -> IO (SAWExpr ret) applyExprSymFn sym sc fn args = - do st <- readIORef (B.sbStateManager sym) + do st <- readIORef (B.userState sym) mk <- case Map.lookup (indexValue (B.symFnId fn)) (saw_symMap st) of Nothing -> panic "SAWCore.applyExprSymFn" @@ -679,7 +679,7 @@ considerSatisfiability :: IO BranchResult considerSatisfiability sym mbPloc p = withSolverProcess' - (\sym' -> saw_online_state <$> readIORef (B.sbStateManager sym')) sym + (\sym' -> saw_online_state <$> readIORef (B.userState sym')) sym (pure IndeterminateBranchResult) $ \proc -> do pnot <- notPred sym p @@ -1214,7 +1214,7 @@ withSolverProcess :: IO a -> (SolverProcess scope solver -> IO a) -> IO a -withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (B.sbStateManager sym')) +withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (B.userState sym')) withSolverConn :: OnlineSolver solver => @@ -1228,7 +1228,7 @@ getAssumptionStack :: SAWCoreBackend s solver fs -> IO (AssumptionStack (B.BoolExpr s) AssumptionReason SimError) getAssumptionStack sym = - (assumptionStack . saw_online_state) <$> readIORef (B.sbStateManager sym) + (assumptionStack . saw_online_state) <$> readIORef (B.userState sym) -- TODO! we should find a better way to share implementations with `OnlineBackend` @@ -1308,7 +1308,7 @@ instance OnlineSolver solver => IsBoolSolver (SAWCoreBackend n solver fs) where AS.saveAssumptionStack stk restoreAssumptionState sym gc = - do st <- saw_online_state <$> readIORef (B.sbStateManager sym) + do st <- saw_online_state <$> readIORef (B.userState sym) restoreSolverState gc st -- restore the previous assumption stack From 78c9083cdbecd28f4ed1a54362b56fc6eed68dd7 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 10/22] CrucibleSAW: the IORef in the What4 ExprBuilder is no longer implicit --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 45 ++++++++++++------- 2 files changed, 30 insertions(+), 16 deletions(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 1817020aa7..6d24609395 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -15,6 +15,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} @@ -97,6 +98,18 @@ data SAWCoreState solver fs n , saw_online_state :: OnlineBackendState solver n } +-- | Wrapper around SAWCoreState that accounts for how the IORef needs +-- to be stuffed into the What4 ExprBuilder. XXX: gross. It looks +-- like the intended model is that the elements of SAWCoreState that +-- need to be mutable should become IORefs instead. +newtype SAWCoreState' solver fs n = SAWCoreState' (IORef (SAWCoreState solver fs n)) + +-- | Accessor to extract the ref +userStateRef :: SAWCoreBackend n solver fs -> IORef (SAWCoreState solver fs n) +userStateRef sym = + let SAWCoreState' ref = sym ^. B.userState in + ref + data SAWExpr (bt :: BaseType) where SAWExpr :: !SC.Term -> SAWExpr bt @@ -107,7 +120,7 @@ data SAWExpr (bt :: BaseType) where -- implicit nat-to-integer conversion. --NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType -type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState solver fs) fs +type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState' solver fs) fs -- | Run the given IO action with the given SAW backend. @@ -119,16 +132,16 @@ type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState solver fs) fs -- state of these fields is restored. inFreshNamingContext :: SAWCoreBackend n solver fs -> IO a -> IO a inFreshNamingContext sym f = - do old <- readIORef (B.userState sym) + do old <- readIORef (userStateRef sym) bracket (mkNew (B.exprCounter sym) old) (restore old) action where action new = - do writeIORef (B.userState sym) new + do writeIORef (userStateRef sym) new f restore old _new = - do writeIORef (B.userState sym) old + do writeIORef (userStateRef sym) old mkNew _gen old = do ch <- B.newIdxCache @@ -146,7 +159,7 @@ inFreshNamingContext sym f = getInputs :: SAWCoreBackend n solver fs -> IO (Seq (SC.ExtCns SC.Term)) getInputs sym = - do st <- readIORef (B.userState sym) + do st <- readIORef (userStateRef sym) readIORef (saw_inputs st) baseSCType :: @@ -191,7 +204,7 @@ sawCreateVar :: SAWCoreBackend n solver fs -> SC.Term -> IO SC.Term sawCreateVar sym nm tp = do - st <- readIORef (B.userState sym) + st <- readIORef (userStateRef sym) let sc = saw_ctx st ec <- SC.scFreshEC sc nm tp t <- SC.scFlatTermF sc (SC.ExtCns ec) @@ -203,7 +216,7 @@ bindSAWTerm :: SAWCoreBackend n solver fs -> SC.Term -> IO (B.Expr n bt) bindSAWTerm sym bt t = do - st <- readIORef $ B.userState sym + st <- readIORef $ userStateRef sym ch_r <- readIORef $ saw_elt_cache_r st let midx = case t of @@ -247,7 +260,7 @@ newSAWCoreBackend fm sc gen = do enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) let st = st0{ saw_online_state = ob_st0{ onlineEnabled = getOpt enableOpt } } - writeIORef (B.userState sym) st + writeIORef (userStateRef sym) st return sym -- | Register an interpretation for a symbolic function. This is not @@ -260,19 +273,19 @@ sawRegisterSymFunInterp :: (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> IO () sawRegisterSymFunInterp sym f i = - modifyIORef (B.userState sym) $ \s -> + modifyIORef (userStateRef sym) $ \s -> s { saw_symMap = Map.insert (indexValue (B.symFnId f)) i (saw_symMap s) } sawBackendSharedContext :: SAWCoreBackend n solver fs -> IO SC.SharedContext sawBackendSharedContext sym = - saw_ctx <$> readIORef (B.userState sym) + saw_ctx <$> readIORef (userStateRef sym) toSC :: OnlineSolver solver => SAWCoreBackend n solver fs -> B.Expr n tp -> IO SC.Term toSC sym elt = - do st <- readIORef $ B.userState sym + do st <- readIORef $ userStateRef sym evaluateExpr sym (saw_ctx st) (saw_elt_cache st) elt @@ -652,7 +665,7 @@ applyExprSymFn :: Ctx.Assignment SAWExpr args -> IO (SAWExpr ret) applyExprSymFn sym sc fn args = - do st <- readIORef (B.userState sym) + do st <- readIORef (userStateRef sym) mk <- case Map.lookup (indexValue (B.symFnId fn)) (saw_symMap st) of Nothing -> panic "SAWCore.applyExprSymFn" @@ -679,7 +692,7 @@ considerSatisfiability :: IO BranchResult considerSatisfiability sym mbPloc p = withSolverProcess' - (\sym' -> saw_online_state <$> readIORef (B.userState sym')) sym + (\sym' -> saw_online_state <$> readIORef (userStateRef sym')) sym (pure IndeterminateBranchResult) $ \proc -> do pnot <- notPred sym p @@ -1214,7 +1227,7 @@ withSolverProcess :: IO a -> (SolverProcess scope solver -> IO a) -> IO a -withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (B.userState sym')) +withSolverProcess = withSolverProcess' (\sym' -> saw_online_state <$> readIORef (userStateRef sym')) withSolverConn :: OnlineSolver solver => @@ -1228,7 +1241,7 @@ getAssumptionStack :: SAWCoreBackend s solver fs -> IO (AssumptionStack (B.BoolExpr s) AssumptionReason SimError) getAssumptionStack sym = - (assumptionStack . saw_online_state) <$> readIORef (B.userState sym) + (assumptionStack . saw_online_state) <$> readIORef (userStateRef sym) -- TODO! we should find a better way to share implementations with `OnlineBackend` @@ -1308,7 +1321,7 @@ instance OnlineSolver solver => IsBoolSolver (SAWCoreBackend n solver fs) where AS.saveAssumptionStack stk restoreAssumptionState sym gc = - do st <- saw_online_state <$> readIORef (B.userState sym) + do st <- saw_online_state <$> readIORef (userStateRef sym) restoreSolverState gc st -- restore the previous assumption stack From 08dc2af5d2a09f5dab56c8513ae8b7691153bce0 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 11/22] CrucibleSAW: need a couple extra module qualifications (not clear why, not worth arguing about) --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 6d24609395..abf9210b55 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -235,10 +235,10 @@ bindSAWTerm sym bt t = do return sbVar newSAWCoreBackend :: - FloatModeRepr fm -> + B.FloatModeRepr fm -> SC.SharedContext -> NonceGenerator IO s -> - IO (SAWCoreBackend s Yices.Connection (Flags fm)) + IO (SAWCoreBackend s Yices.Connection (B.Flags fm)) newSAWCoreBackend fm sc gen = do inpr <- newIORef Seq.empty ch <- B.newIdxCache From 77da6e599a4dd49d805d91f61d29735f5e780d6d Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 12/22] CrucibleSAW: cope with OnlineBackend changes Interface changes have assimilated some of the code that was here into the Crucible OnlineBackend interface. So we don't need that any more. However, those changes also make the initialization we need to do circular. The only viable way to break that cycle without upstream interface changes is to set the initial online state to Nothing and then update it after we've constructed the objects. This means it will always be Just at runtime, so fake out the prior field accessor to unwrap the Maybe and panic if it's Nothing, which it should never be. XXX: This is using the wrong panic interface; clean that up later if XXX: this code sticks around. XXX: This is a hack. If this code sticks around, we should look into XXX: upstream interface changes to avoid the cyclic initialization. --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 34 ++++++++++++++++--- 2 files changed, 31 insertions(+), 4 deletions(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index abf9210b55..e642ea3ffb 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -95,7 +95,7 @@ data SAWCoreState solver fs n -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between -- SAWCore terms and What4 variables. - , saw_online_state :: OnlineBackendState solver n + , saw_online_state_maybe :: Maybe (OnlineBackend solver n (SAWCoreState solver fs) fs) } -- | Wrapper around SAWCoreState that accounts for how the IORef needs @@ -153,7 +153,7 @@ inFreshNamingContext sym f = , saw_symMap = mempty , saw_elt_cache = ch , saw_elt_cache_r = ch_r - , saw_online_state = saw_online_state old + , saw_online_state_maybe = saw_online_state_maybe old } return new @@ -244,25 +244,51 @@ newSAWCoreBackend fm sc gen = do ch <- B.newIdxCache ch_r <- newIORef IntMap.empty let feats = Yices.yicesDefaultFeatures - ob_st0 <- initialOnlineBackendState gen feats + + -- dholland 20250409 this initialization is now circular: + -- the SAWCoreState requires an OnlineBackend + -- the OnlineBackend requires sym + -- sym (the ExprBuilder) requires a SAWCoreState + -- + -- We can't fix this by mucking with the ExprBuilder or + -- OnlineBackend construction as those are controlled by Crucible + -- and What4 interfaces (resp.) so we have to create an initial + -- SAWCoreState with a dummy OnlineBackend. Then we can update the + -- state. However, in order to do this we need to make the state + -- field Maybe, which will be a headache wherever it's used. let st0 = SAWCoreState { saw_ctx = sc , saw_inputs = inpr , saw_symMap = Map.empty , saw_elt_cache = ch , saw_elt_cache_r = ch_r - , saw_online_state = ob_st0 + , saw_online_state_maybe = Nothing } sym <- B.newExprBuilder fm st0 gen + ob_st0 <- newOnlineBackend sym feats + let st = st0 { saw_online_state_maybe = Just ob_st0 } + + -- though on the plus side this goop is now handled inside newOnlineBackend +{- let options = backendOptions ++ onlineBackendOptions ob_st0 ++ Yices.yicesOptions extendConfig options (getConfiguration sym) enableOpt <- getOptionSetting enableOnlineBackend (getConfiguration sym) let st = st0{ saw_online_state = ob_st0{ onlineEnabled = getOpt enableOpt } } +-} writeIORef (userStateRef sym) st return sym +-- | Extract the saw_online_state from the SAWCoreState. This is a +-- pretend field accessor created for compat with code from before +-- the online state needed a Maybe in it. (The Nothing case of said +-- Maybe only exists during initialization; see newSAWCoreBackend. +saw_online_state :: SAWCoreState solver fs n -> OnlineBackend solver n (SAWCoreState' solver fs) fs +saw_online_state st = case saw_online_state_maybe st of + Nothing -> panic "CrucibleSAW.SAWCore" ["saw_online_state: hit Nothing after initialization"] + Just ob_st -> ob_st + -- | Register an interpretation for a symbolic function. This is not -- used during simulation, but rather, when we translate Crucible -- values back into SAW. The interpretation function takes a list of From 2d8240f039e9946dd281ef30f1b0f1e3f29f99b5 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 13/22] CrucibleSAW: More ioref-related changes in previous --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 5 +++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index e642ea3ffb..28da92e301 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -95,7 +95,7 @@ data SAWCoreState solver fs n -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between -- SAWCore terms and What4 variables. - , saw_online_state_maybe :: Maybe (OnlineBackend solver n (SAWCoreState solver fs) fs) + , saw_online_state_maybe :: Maybe (OnlineBackend solver n (SAWCoreState' solver fs) fs) } -- | Wrapper around SAWCoreState that accounts for how the IORef needs @@ -264,7 +264,8 @@ newSAWCoreBackend fm sc gen = do , saw_elt_cache_r = ch_r , saw_online_state_maybe = Nothing } - sym <- B.newExprBuilder fm st0 gen + st0' <- SAWCoreState' <$> newIORef st0 + sym <- B.newExprBuilder fm st0' gen ob_st0 <- newOnlineBackend sym feats let st = st0 { saw_online_state_maybe = Just ob_st0 } From 998225855403f6f4abbd724d9b9d92764ab541e0 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 14/22] CrucibleSAW: catch up to AssumptionStack changes --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 5 +++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 28da92e301..4c05d4cf6e 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -1266,7 +1266,7 @@ withSolverConn sym k = withSolverProcess sym (pure ()) (k . solverConn) getAssumptionStack :: SAWCoreBackend s solver fs -> - IO (AssumptionStack (B.BoolExpr s) AssumptionReason SimError) + IO (AssumptionStack (Assumption (B.BoolExpr s)) SimError) getAssumptionStack sym = (assumptionStack . saw_online_state) <$> readIORef (userStateRef sym) @@ -1291,7 +1291,8 @@ instance OnlineSolver solver => IsBoolSolver (SAWCoreBackend n solver fs) where -- Record assumption, even if trivial. -- This allows us to keep track of the full path we are on. - AS.assume a =<< getAssumptionStack sym + stk <- getAssumptionStack sym + AS.appendAssumptions (Seq.singleton a) stk addAssumptions sym a = -- NB, don't add the assumption to the assumption stack unless From cf6eb1bf07407eaf8ed595a566aa705ab606bc4e Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 15/22] CrucibleSAW: catch up to changes in What4 floats --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 33 ++++++++++--------- 2 files changed, 17 insertions(+), 17 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 4c05d4cf6e..f12ecd1c0e 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -1151,11 +1151,11 @@ evaluateExpr sym sc cache = f [] ------------------------------------------------------------------------ -- Floating point operations - B.FloatPZero{} -> floatFail - B.FloatNZero{} -> floatFail - B.FloatNaN{} -> floatFail - B.FloatPInf{} -> floatFail - B.FloatNInf{} -> floatFail + --B.FloatPZero{} -> floatFail + --B.FloatNZero{} -> floatFail + --B.FloatNaN{} -> floatFail + --B.FloatPInf{} -> floatFail + --B.FloatNInf{} -> floatFail B.FloatNeg{} -> floatFail B.FloatAbs{} -> floatFail B.FloatSqrt{} -> floatFail @@ -1164,11 +1164,11 @@ evaluateExpr sym sc cache = f [] B.FloatMul{} -> floatFail B.FloatDiv{} -> floatFail B.FloatRem{} -> floatFail - B.FloatMin{} -> floatFail - B.FloatMax{} -> floatFail + --B.FloatMin{} -> floatFail + --B.FloatMax{} -> floatFail B.FloatFMA{} -> floatFail B.FloatFpEq{} -> floatFail - B.FloatFpNe{} -> floatFail + --B.FloatFpNe{} -> floatFail B.FloatLe{} -> floatFail B.FloatLt{} -> floatFail B.FloatIsNaN{} -> floatFail @@ -1195,14 +1195,15 @@ evaluateExpr sym sc cache = f [] B.CeilReal{} -> realFail B.RealDiv{} -> realFail B.RealSqrt{} -> realFail - B.Pi{} -> realFail - B.RealSin{} -> realFail - B.RealCos{} -> realFail - B.RealSinh{} -> realFail - B.RealCosh{} -> realFail - B.RealExp{} -> realFail - B.RealLog{} -> realFail - B.RealATan2{} -> realFail + --B.Pi{} -> realFail + --B.RealSin{} -> realFail + --B.RealCos{} -> realFail + --B.RealSinh{} -> realFail + --B.RealCosh{} -> realFail + --B.RealExp{} -> realFail + --B.RealLog{} -> realFail + --B.RealATan2{} -> realFail + B.RealSpecialFunction{} -> realFail B.Cplx{} -> cplxFail B.RealPart{} -> cplxFail From 562c4d5f8a0b9706a0acbe4795bc870815b3d8a1 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 16/22] CrucibleSAW: adjust for IsBoolSolver -> IsSymBackend XXX: this can almost certainly be done better --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index f12ecd1c0e..84e3f19d46 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -1273,7 +1273,12 @@ getAssumptionStack sym = -- TODO! we should find a better way to share implementations with `OnlineBackend` -instance OnlineSolver solver => IsBoolSolver (SAWCoreBackend n solver fs) where +-- +-- XXX: while the first argument here needs to be the ExprBuilder, the second can +-- be something else (AIUI) and if we peel some bits of the state out and put +-- them in the second argument instead we can probably avoid the circular +-- initialization in newSAWCoreBackend. +instance OnlineSolver solver => IsSymBackend (SAWCoreBackend n solver fs) (SAWCoreBackend n solver fs) where addDurableProofObligation sym a = AS.addProofObligation a =<< getAssumptionStack sym From 83582d6d23270a825a5c553ee3c17cedb2e594d4 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 17/22] CrucibleSAW: Adjust to changes in ExprSymFn in What4. --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 84e3f19d46..a963f969a5 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -296,7 +296,7 @@ saw_online_state st = case saw_online_state_maybe st of -- arguments in regular (left-to-right) order. sawRegisterSymFunInterp :: SAWCoreBackend n solver fs -> - B.ExprSymFn n (B.Expr n) args ret -> + B.ExprSymFn n args ret -> (SC.SharedContext -> [SC.Term] -> IO SC.Term) -> IO () sawRegisterSymFunInterp sym f i = @@ -688,7 +688,7 @@ applyExprSymFn :: OnlineSolver solver => SAWCoreBackend n solver fs -> SC.SharedContext -> - B.ExprSymFn n (B.Expr n) args ret -> + B.ExprSymFn n args ret -> Ctx.Assignment SAWExpr args -> IO (SAWExpr ret) applyExprSymFn sym sc fn args = From b3a6648617de3c44fa2b1977a15a7feb7b40c589 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 18/22] CrucibleSAW: adjust to lenses --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index a963f969a5..3ef8ea3158 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -133,7 +133,7 @@ type SAWCoreBackend n solver fs = B.ExprBuilder n (SAWCoreState' solver fs) fs inFreshNamingContext :: SAWCoreBackend n solver fs -> IO a -> IO a inFreshNamingContext sym f = do old <- readIORef (userStateRef sym) - bracket (mkNew (B.exprCounter sym) old) (restore old) action + bracket (mkNew (sym ^. B.exprCounter) old) (restore old) action where action new = From 2f4f80fce96622deae1116ec75867837e0c91b6c Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 19/22] CrucibleSAW: use Text instead of String --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 19 ++++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 3ef8ea3158..88bbd94c68 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -16,6 +16,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} @@ -200,7 +201,7 @@ baseSCType sym sc bt = -- | Create a new symbolic variable. sawCreateVar :: SAWCoreBackend n solver fs - -> String -- ^ the name of the variable + -> Text.Text -- ^ the name of the variable -> SC.Term -> IO SC.Term sawCreateVar sym nm tp = do @@ -571,7 +572,7 @@ scEq sym sc tp x y = let SAWExpr y' = y w' <- SC.scNat sc $ fromIntegral (natValue w) SAWExpr <$> SC.scBvEq sc w' x' y' - _ -> unsupported sym ("SAW backend: equality comparison on unsupported type:" ++ show tp) + _ -> unsupported sym ("SAW backend: equality comparison on unsupported type:" <> Text.pack (show tp)) scAllEq :: @@ -741,8 +742,8 @@ obligation to ensure that we won't get there. These proof obligations are all tagged with "Unsupported", so that users of the library can choose if they will try to discharge them, fail in some other way, or just ignore them. -} -unsupported :: OnlineSolver solver => SAWCoreBackend n solver fs -> String -> IO a -unsupported sym x = addFailedAssertion sym (Unsupported x) +unsupported :: OnlineSolver solver => SAWCoreBackend n solver fs -> Text.Text -> IO a +unsupported sym x = addFailedAssertion sym (Unsupported Text.unpack x) evaluateExpr :: forall n solver tp fs. OnlineSolver solver => @@ -772,8 +773,8 @@ evaluateExpr sym sc cache = f [] stringFail :: IO a stringFail = unsupported sym "SAW backend does not support string values" - unimplemented :: String -> IO a - unimplemented x = unsupported sym $ "SAW backend: not implemented: " ++ x + unimplemented :: Text.Text -> IO a + unimplemented x = unsupported sym $ "SAW backend: not implemented: " <> x go :: [Maybe SolverSymbol] -> B.Expr n tp' -> IO (SAWExpr tp') @@ -794,14 +795,14 @@ evaluateExpr sym sc cache = f [] B.UninterpVarKind -> do tp <- baseSCType sym sc (B.bvarType bv) SAWExpr <$> sawCreateVar sym nm tp - where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + where nm = solverSymbolAsText $ B.bvarName bv B.LatchVarKind -> unsupported sym "SAW backend does not support latch variables" B.QuantifierVarKind -> do case elemIndex (Just $ B.bvarName bv) env of Nothing -> unsupported sym $ "unbound quantifier variable " <> nm Just idx -> SAWExpr <$> SC.scLocalVar sc idx - where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + where nm = solverSymbolAsText $ B.bvarName bv go env (B.NonceAppExpr p) = case B.nonceExprApp p of @@ -830,7 +831,7 @@ evaluateExpr sym sc cache = f [] go env a0@(B.AppExpr a) = let nyi = unsupported sym $ "Expression form not yet implemented in SAWCore backend:\n" - ++ show a0 + <> Text.pack (show a0) in case B.appExprApp a of B.BaseIte bt _ c xe ye -> join (scIte sym sc bt <$> eval env c <*> eval env xe <*> eval env ye) From c67789c765527c3523ed341854188c8ddeec877a Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 20/22] CrucibleSAW: Unsupported has changed, adjust --- cabal.project | 1 + src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index c3d5145639..71900e2a1b 100644 --- a/cabal.project +++ b/cabal.project @@ -64,3 +64,4 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 + diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index 88bbd94c68..fe52dc7753 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -49,6 +49,8 @@ import qualified Data.Text as Text import Numeric.Natural +import GHC.Stack + import What4.BaseTypes import What4.Config import What4.Interface @@ -743,7 +745,7 @@ These proof obligations are all tagged with "Unsupported", so that users of the library can choose if they will try to discharge them, fail in some other way, or just ignore them. -} unsupported :: OnlineSolver solver => SAWCoreBackend n solver fs -> Text.Text -> IO a -unsupported sym x = addFailedAssertion sym (Unsupported Text.unpack x) +unsupported sym x = addFailedAssertion sym (Unsupported callstack $ Text.unpack x) evaluateExpr :: forall n solver tp fs. OnlineSolver solver => From f036ca3e27c8e8809c222d45c26b84363fa2733c Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:01:01 -0400 Subject: [PATCH 21/22] CrucibleSAW: ConjMap changes --- cabal.project | 1 - src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs | 16 ++++++++-------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/cabal.project b/cabal.project index 71900e2a1b..c3d5145639 100644 --- a/cabal.project +++ b/cabal.project @@ -64,4 +64,3 @@ source-repository-package type: git location: https://github.com/eddywestbrook/hobbits.git tag: 70963e0e3eba2b16f6fc030acb582e8100955e47 - diff --git a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs index fe52dc7753..de409b0138 100644 --- a/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs +++ b/src/SAWScript/Crucible/CrucibleSAW/SAWCore.hs @@ -849,10 +849,10 @@ evaluateExpr sym sc cache = f [] goNeg env x B.ConjPred xs -> - case BM.viewBoolMap xs of - BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc True - BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc False - BM.BoolMapTerms (t:|ts) -> + case BM.viewConjMap xs of + BM.ConjTrue -> SAWExpr <$> SC.scBool sc True + BM.ConjFalse -> SAWExpr <$> SC.scBool sc False + BM.Conjuncts (t:|ts) -> let pol (x,BM.Positive) = f env x pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts) @@ -1230,10 +1230,10 @@ evaluateExpr sym sc cache = f [] case expr of -- negation of (x /\ y) becomes (~x \/ ~y) B.AppExpr (B.appExprApp -> B.ConjPred xs) -> - case BM.viewBoolMap xs of - BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc False - BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc True - BM.BoolMapTerms (t:|ts) -> + case BM.viewConjMap xs of + BM.ConjTrue -> SAWExpr <$> SC.scBool sc False + BM.ConjFalse -> SAWExpr <$> SC.scBool sc True + BM.Conjuncts (t:|ts) -> let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x pol (x, BM.Negative) = f env x in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts) From a69913bbcf1e1cb695713e0dbb860d57ee6eba36 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 10 Apr 2025 15:00:53 -0400 Subject: [PATCH 22/22] aarch32: a few preliminary build fixes --- src/SAWScript/Crucible/LLVM/AArch32.hs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/AArch32.hs b/src/SAWScript/Crucible/LLVM/AArch32.hs index 8eb00e7ff1..5e541cf112 100644 --- a/src/SAWScript/Crucible/LLVM/AArch32.hs +++ b/src/SAWScript/Crucible/LLVM/AArch32.hs @@ -75,7 +75,7 @@ import qualified SAWScript.Crucible.Common.Override as O import qualified SAWScript.Crucible.Common.Setup.Type as Setup import SAWScript.Crucible.LLVM.Builtins -import SAWScript.Crucible.LLVM.MethodSpecIR +import SAWScript.Crucible.LLVM.MethodSpecIR (LLVMCrucibleContext(..)) import SAWScript.Crucible.LLVM.ResolveSetupValue import qualified SAWScript.Crucible.LLVM.Override as LO @@ -88,7 +88,7 @@ import qualified What4.Solver.Yices as Yices import qualified Lang.Crucible.Analysis.Postdom as C import qualified Lang.Crucible.Backend as C -import qualified Lang.Crucible.Backend.SAWCore as C +import qualified SAWScript.Crucible.CrucibleSAW.SAWCore as C import qualified Lang.Crucible.CFG.Core as C import qualified Lang.Crucible.FunctionHandle as C import qualified Lang.Crucible.Simulator.EvalStmt as C @@ -130,8 +130,9 @@ import qualified Language.ASL.Globals as ASL type Sym = C.SAWCoreBackend GlobalNonceGenerator Yices.Connection (W4.Flags W4.FloatReal) type LLVMArch = C.LLVM.X86 32 -type LLVM = C.LLVM.LLVM LLVMArch -type LLVMOverrideMatcher = O.OverrideMatcher LLVM +--type LLVM = C.LLVM.LLVM LLVMArch +type LLVM = C.LLVM.LLVM +type LLVMOverrideMatcher rorw a = O.OverrideMatcher LLVM rorw a type Regs = Assignment (C.RegValue' Sym) (Macaw.MacawCrucibleRegTypes Macaw.ARM) type Register = Macaw.ARMReg (Macaw.BVType 32) type Mem = C.LLVM.MemImpl Sym @@ -256,7 +257,7 @@ freshVal sym t ptrOk nm = | ptrOk, Just Refl <- testEquality w (knownNat @64) -> do sn_base <- symName (nm ++ "_base") sn_off <- symName (nm ++ "_off") - base <- W4.freshConstant sym sn_base C.BaseNatRepr + base <- W4.freshNat sym sn_base off <- W4.freshConstant sym sn_off (C.BaseBVRepr w) return (C.LLVM.LLVMPointer base off) | otherwise -> do