From 8acc49b1319473ed2d3859f7afa68abed0e544f6 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 20 Feb 2019 16:59:41 -0800 Subject: [PATCH 1/8] Delete old X86 stuff. It seems that something has bit rotted, so this is still a work in progress. --- saw-script.cabal | 8 - src/SAWScript/X86.hs | 73 ++---- src/SAWScript/X86Spec.hs | 242 ------------------- src/SAWScript/X86Spec/Fresh.hs | 95 -------- src/SAWScript/X86Spec/Literal.hs | 38 --- src/SAWScript/X86Spec/Memory.hs | 211 ----------------- src/SAWScript/X86Spec/Monad.hs | 307 ------------------------ src/SAWScript/X86Spec/Registers.hs | 360 ----------------------------- src/SAWScript/X86Spec/SAW.hs | 30 --- src/SAWScript/X86Spec/Types.hs | 168 -------------- src/SAWScript/X86SpecNew.hs | 37 ++- 11 files changed, 49 insertions(+), 1520 deletions(-) delete mode 100644 src/SAWScript/X86Spec.hs delete mode 100644 src/SAWScript/X86Spec/Fresh.hs delete mode 100644 src/SAWScript/X86Spec/Literal.hs delete mode 100644 src/SAWScript/X86Spec/Memory.hs delete mode 100644 src/SAWScript/X86Spec/Monad.hs delete mode 100644 src/SAWScript/X86Spec/Registers.hs delete mode 100644 src/SAWScript/X86Spec/SAW.hs delete mode 100644 src/SAWScript/X86Spec/Types.hs diff --git a/saw-script.cabal b/saw-script.cabal index fd9e15e9a1..e1af021d3a 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -155,14 +155,6 @@ library SAWScript.X86 SAWScript.X86SpecNew - SAWScript.X86Spec - SAWScript.X86Spec.Memory - SAWScript.X86Spec.Registers - SAWScript.X86Spec.Fresh - SAWScript.X86Spec.Literal - SAWScript.X86Spec.SAW - SAWScript.X86Spec.Monad - SAWScript.X86Spec.Types GHC-options: -O2 -Wall -fno-ignore-asserts -fno-spec-constr-count if impl(ghc == 8.0.1) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 0ecb11e2ac..805bec0017 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -26,22 +26,22 @@ import qualified Data.AIG as AIG import Data.ByteString (ByteString) import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BSC -import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Text as Text import Data.Text.Encoding(decodeUtf8) -import GHC.Natural(Natural) import System.IO(hFlush,stdout) import Data.ElfEdit (Elf, parseElf, ElfGetResult(..)) import Data.Parameterized.Some(Some(..)) import Data.Parameterized.Classes(knownRepr) -import Data.Parameterized.Context(Assignment,EmptyCtx,(::>),singleton) +import Data.Parameterized.Context(EmptyCtx,(::>),singleton) import Data.Parameterized.Nonce(globalNonceGenerator) -- What4 import What4.Interface(asNat,asUnsignedBV) +import qualified What4.Interface as W4 +import qualified What4.Config as W4 import What4.FunctionName(functionNameFromText) import What4.ProgramLoc(ProgramLoc,Position(OtherPos)) @@ -58,7 +58,7 @@ import Lang.Crucible.Simulator.EvalStmt(executeCrucible) import Lang.Crucible.Simulator.ExecutionTree (GlobalPair,gpValue,ExecResult(..),PartialResult(..) , gpGlobals, AbortedResult(..), SimContext(..), FnState(..) - , initSimState, ExecState(InitialState) + , ExecState(InitialState) ) import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason) import Lang.Crucible.Backend @@ -93,7 +93,7 @@ import Data.Macaw.Memory.ElfLoader( LoadOptions(..) , MemSymbol(..) ) import Data.Macaw.Symbolic( ArchRegStruct - , ArchRegContext,mkFunCFG + , mkFunCFG , GlobalMap , MacawSimulatorState(..) , macawExtensions @@ -102,7 +102,7 @@ import qualified Data.Macaw.Symbolic as Macaw ( LookupFunctionHandle(..) ) import Data.Macaw.Symbolic( MacawExt , MacawFunctionArgs ) -import Data.Macaw.Symbolic.Backend(macawAssignToCrucM, MacawSymbolicArchFunctions(..), crucArchRegTypes) +import Data.Macaw.Symbolic.Backend(MacawSymbolicArchFunctions(..), crucArchRegTypes) import Data.Macaw.X86(X86Reg(..), x86_64_linux_info,x86_64_freeBSD_info) import Data.Macaw.X86.ArchTypes(X86_64) import Data.Macaw.X86.Symbolic @@ -121,12 +121,8 @@ import Verifier.SAW.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule) import Verifier.SAW.Cryptol.Prelude(scLoadPreludeModule,scLoadCryptolModule) -- SAWScript -import SAWScript.X86Spec.Types(Sym) -import SAWScript.X86Spec.Monad(runPreSpec,runPostSpec,PreExtra(..)) -import SAWScript.X86Spec.Registers(macawLookup) -import SAWScript.X86Spec (Spec,FunSpec(..),Pre,Post,RegAssign) - import SAWScript.X86SpecNew +import SAWScript.Proof(predicateToProp, Quantification(Universal)) @@ -154,18 +150,6 @@ data Options = Options , memvar :: GlobalVar Mem -- ^ The global variable storing the heap - , funCalls :: Map (Natural,Integer) CallHandler - {- ^ A mapping for function locations to the code to run to handle - function calls. The two integers are the base and offset - pair representing the address of function. - The handler is just some code that will be executed instead of - calling the function. Typeically, it should assert the functions's - precondition and asssume its post condition after. - - Note that his works only when the call is completely known - (i.e., no symbolic stuff, etc.) - -} - , cryEnv :: CryptolEnv , extraGlobals :: [(ByteString,Integer,Unit)] @@ -197,18 +181,15 @@ proof :: (AIG.IsAIG l g) => FilePath {- ^ ELF binary -} -> Maybe FilePath {- ^ Cryptol spec, if any -} -> [(ByteString,Integer,Unit)] -> - (Sym -> CryptolEnv -> IO (Map (Natural,Integer) CallHandler)) - {- ^ Funciton call handler; used only for OldStyle -} -> Fun -> IO (SharedContext,Integer,[Goal]) -proof proxy archi file mbCry globs mkCallMap fun = +proof proxy archi file mbCry globs fun = do sc <- mkSharedContext halloc <- newHandleAllocator scLoadPreludeModule sc scLoadCryptolModule sc sym <- newSAWCoreBackend proxy sc globalNonceGenerator cenv <- loadCry sym mbCry - callMap <- mkCallMap sym cenv mvar <- stToIO (mkMemVar halloc) proofWithOptions Options { fileName = file @@ -217,7 +198,6 @@ proof proxy archi file mbCry globs mkCallMap fun = , backend = sym , allocator = halloc , memvar = mvar - , funCalls = callMap , cryEnv = cenv , extraGlobals = globs } @@ -410,14 +390,12 @@ translate opts elf fun = (globs,st,checkPost) <- case funSpec fun of - OldStyle spec -> doSpecOldStyle opts spec NewStyle mkSpec debug -> do gss <- mapM (loadGlobal elf) (extraGlobals opts) spec0 <- mkSpec (cryEnv opts) let spec = spec0 {specGlobsRO = concat (specGlobsRO spec0:gss)} (gs,st,po) <- verifyMode spec sopts debug st - let _oldStyle = (fst gs, funCalls opts) return (gs,st,\st1 -> debug st1 >> po st1) (addr, st1) <- doSim opts elf sfs name globs st @@ -429,27 +407,11 @@ translate opts elf fun = return (ctx, addr, gs) -doSpecOldStyle :: - Options -> - Spec Pre (RegAssign, Spec Post ()) -> - IO ((GlobalMap Sym 64, Overrides), State, State -> IO ()) -doSpecOldStyle opts spec = - do let sym = backend opts - - ((initRegs,post), extra) <- - statusBlock " Setting up pre-conditions... " $ - runPreSpec sym (cryEnv opts) spec - - regs <- macawAssignToCrucM (return . macawLookup initRegs) genRegAssign - - return ( (mkGlobalMap (theRegions extra), funCalls opts) - , State { stateMem = theMem extra, stateRegs = regs } - , \st1 -> statusBlock " Setting-up post-conditions... " $ - runPostSpec sym (cryEnv opts) - (stateRegs st1) - (stateMem st1) - post - ) +setSimulatorVerbosity :: (W4.IsSymExprBuilder sym) => Int -> sym -> IO () +setSimulatorVerbosity verbosity sym = do + verbSetting <- W4.getOptionSetting W4.verbosity (W4.getConfiguration sym) + _ <- W4.setOpt verbSetting (toInteger verbosity) + return () @@ -479,6 +441,7 @@ doSim opts elf sfs name (globs,overs) st = let sym = backend opts mvar = memvar opts + setSimulatorVerbosity 4 sym execResult <- statusBlock " Simulating... " $ do let crucRegTypes = crucArchRegTypes x86 @@ -587,11 +550,11 @@ data Goal = Goal -- | The boolean term that needs proving (i.e., assumptions imply conclusion) gGoal :: SharedContext -> Goal -> IO Term -gGoal ctx g = go (gAssumes g) +gGoal sc g = predicateToProp sc Universal [] =<< go (gAssumes g) where go xs = case xs of [] -> return (gShows g) - a : as -> scImplies ctx a =<< go as + a : as -> scImplies sc a =<< go as getGoals :: Sym -> IO [Goal] getGoals sym = @@ -624,10 +587,6 @@ instance Show Goal where x86 :: MacawSymbolicArchFunctions X86_64 x86 = x86_64MacawSymbolicFns -genRegAssign :: Assignment X86Reg (ArchRegContext X86_64) -genRegAssign = crucGenRegAssignment x86 - - -------------------------------------------------------------------------------- diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs deleted file mode 100644 index e67d3ee1c2..0000000000 --- a/src/SAWScript/X86Spec.hs +++ /dev/null @@ -1,242 +0,0 @@ -{-# Language DataKinds, TypeFamilies, TypeOperators, GADTs #-} -{-# Language FlexibleContexts #-} -{-# Language ImplicitParams #-} -{-# Language TypeApplications #-} -{-# Language PatternSynonyms #-} -{-# Language UndecidableInstances #-} -{-# Language TypeSynonymInstances #-} -{-# Language AllowAmbiguousTypes #-} -{-# Language ScopedTypeVariables #-} -{-# Language FlexibleInstances #-} -{-# Language RankNTypes #-} -{-# Language RecordWildCards #-} -module SAWScript.X86Spec - ( -- * Specifications - FunSpec(..) - , Spec - , SpecType - - -- ** Pre conditions - , Pre - , fresh - , assume - , freshRegs - , freshGP - , setupGPRegs, GPSetup(..), GPValue, gpUse - , setupVecRegs - , GetReg(..) - , allocBytes - , allocArray - , freshArray - , Mutability(..) - , WriteMem(..) - , registerRegion - - -- ** Post conditions - , Post - , readMem - , readArray - , assert - - -- * Types - , X86Type - , Bits, APtr, ABool, ABigFloat - , pattern Byte - , pattern Word - , pattern DWord - , pattern QWord - , pattern V128 - , pattern V256 - - , X86(..) - , Infer(..) - , MemType - , SizeOf(..) - , Bytes - , toBytes - , bytesToInteger - , BitSize - , bitSize - - -- * Values - , Value - , SAW(..), showTerm, withSharedContext - , Literal(..), literal - , SameVal(..) - , expectSame - , preserveGP - , ptrAdd - , (.*) - - -- * Registers - , IP(..) - , GPReg(..), GPRegUse(..) - , VecReg(..) - , FPReg(..) - - , Flag(..) - , X87Status(..) - , X87Top(..) - , X87Tag(..) - - , RegAssign(..), GPRegVal(..) - - -- * Cryptol specs - , cryTerm - , cryConst - - -- * Misc - , debug - , ppVal - - ) where - -import qualified Data.Vector as Vector - -import What4.Interface (falsePred, isEq, printSymExpr) -import SAWScript.CrucibleLLVM (ptrEq, ppPtr) - -import Verifier.SAW.Term.Pretty(showTerm) -import Verifier.SAW.CryptolEnv(CryptolEnv) - -import SAWScript.X86Spec.Types -import SAWScript.X86Spec.Registers -import SAWScript.X86Spec.Monad -import SAWScript.X86Spec.Fresh -import SAWScript.X86Spec.SAW -import SAWScript.X86Spec.Literal -import SAWScript.X86Spec.Memory - -import SAWScript.X86SpecNew(Specification,State) - - - - -debug :: String -> Spec p () -debug x = io (putStrLn x) - -ppValAt :: X86 t -> Value t -> String -ppValAt ty (Value v) = - case ty of - Bits _ -> show (ppPtr v) - Ptr -> show (ppPtr v) - BigFloat -> show (ppPtr v) - Bool -> show (printSymExpr v) - -ppVal :: Infer t => Value t -> String -ppVal = ppValAt infer - --- | Assert that two values are the same. -expectSame :: (Infer t) => - String {- ^ A label to use if the assertion fails" -} -> - Value t -> Value t -> Spec Post () -expectSame s x y = - do ok <- sameVal x y - assert ok $ unlines [ s ++ " values are not the same:" - , "*** Expected: " ++ ppVal x - , "*** Actual : " ++ ppVal y - ] - --- | Assert that a given general purpose register is preserved. -preserveGP :: RegAssign {- ^ Initial register assignment -} -> - GPReg {- ^ Register to preserve -} -> - Spec Post () -preserveGP r g = - case valGPReg r g of - GPBits oldV -> expectSame (show g) oldV =<< getReg (g,AsBits) - GPPtr oldV -> expectSame (show g) oldV =<< getReg (g,AsPtr) - - - -class SameVal t where - sameVal :: t -> t -> Spec p (Value ABool) - -sameValAt :: X86 t -> Value t -> Value t -> Spec p (Value ABool) -sameValAt t (Value x) (Value y) = - withSym $ \sym -> - Value <$> ( - let w = bitSize t - in case t of - Bits _ -> ptrEq sym w x y - Ptr -> ptrEq sym w x y - BigFloat -> ptrEq sym w x y - Bool -> isEq sym x y) - - -instance Infer t => SameVal (Value t) where - sameVal = sameValAt infer - -instance SameVal GPRegVal where - sameVal x y = - case (x,y) of - (GPBits a, GPBits b) -> sameVal a b - (GPPtr a, GPPtr b) -> sameVal a b - _ -> withSym $ \sym -> return (Value (falsePred sym)) - - -{- | A specifiction for a function. -The outer, "Pre", computiation sets up the initial state of the -computation (i.e., the pre-condition for the function). -As a result, we return the inital register assignemtn, -and the post-condition for the function). -} -data FunSpec = - OldStyle (Spec Pre (RegAssign, Spec Post ())) - | NewStyle (CryptolEnv -> IO Specification) - (State -> IO ()) - -- Debug: Run this to print some stuff at interesting times. - - - --- | Generate fresh values for all general purpose registers. -setupGPRegs :: - (GPReg -> GPSetup) - {- ^ Specifies how to initialize the given GP register -} -> - Spec Pre (GPReg -> GPRegVal) -setupGPRegs ty = - do vs <- Vector.fromList <$> mapM mk elemList - return (\x -> vs Vector.! fromEnum x) - where - mk r = case ty r of - GPFresh AsBits -> GPBits <$> fresh infer (show r) - GPFresh AsPtr -> GPPtr <$> fresh infer (show r) - GPUse x -> return x - --- | A boolean tag to classify the use of a register. -data GPSetup = forall t. GPFresh (GPRegUse t) - | GPUse GPRegVal - - --- | Use the given value to initalize a general purpose register -gpUse :: GPValue t => Value t -> GPSetup -gpUse = GPUse . gpValue - -setupVecRegs :: - (VecReg -> Maybe (Value (Bits 256))) -> - Spec Pre (VecReg -> Value (Bits 256)) -setupVecRegs ty = - do vs <- Vector.fromList <$> mapM mk elemList - return (\x -> vs Vector.! fromEnum x) - where - mk r = case ty r of - Just x -> return x - Nothing -> fresh V256 (show r) - - - --- | Allocate an array initialized with fresh values. -freshArray :: - MemType t => - String {- ^ Name -} -> - Integer {- ^ Number of elemnts -} -> - X86 t {- ^ Type of elements -} -> - Mutability {- ^ Read/write? -} -> - Spec Pre (Value APtr, [Value t]) - -- ^ Returns the pointer and the values in the array. -freshArray name size ty mut = - do vs <- mapM el (take (fromIntegral size) [ 0 .. ]) - p <- allocArrayOf ty name mut vs - return (p, vs) - where - el n = fresh ty (name ++ "_at_" ++ show (n::Int)) - - diff --git a/src/SAWScript/X86Spec/Fresh.hs b/src/SAWScript/X86Spec/Fresh.hs deleted file mode 100644 index f62a88600b..0000000000 --- a/src/SAWScript/X86Spec/Fresh.hs +++ /dev/null @@ -1,95 +0,0 @@ -{-# Language DataKinds #-} -{-# Language TypeFamilies #-} -{-# Language TypeOperators #-} -{-# Language ScopedTypeVariables #-} -{-# Language FlexibleContexts #-} -{-# Language PatternSynonyms #-} -module SAWScript.X86Spec.Fresh (fresh, freshGP, freshRegs, elemList) where - -import GHC.TypeLits (type (<=)) -import qualified Data.Vector as Vector - -import Data.Parameterized.NatRepr(knownNat) - -import What4.BaseTypes (BaseTypeRepr(BaseBVRepr,BaseNatRepr,BaseBoolRepr)) -import What4.Symbol(SolverSymbol,userSymbol) -import What4.Interface(freshConstant) - -import SAWScript.CrucibleLLVM (LLVMPointerType, pattern LLVMPointer, llvmPointer_bv) - -import SAWScript.X86Spec.Types -import SAWScript.X86Spec.Monad -import SAWScript.X86Spec.Registers - - --- | Generate an unknonw value of the given type. -fresh :: X86 t -> String -> Spec Pre (Value t) -fresh x str = - case x of - Bits n -> freshBits str (Bits n) - Ptr -> freshPtr str - Bool -> freshBool str - BigFloat -> freshBits str x - - --- | An uninitialized boolean value. -freshBool :: String -> Spec Pre (Value ABool) -freshBool str = - withSym $ \sym -> - do nm <- symName str - Value <$> freshConstant sym nm BaseBoolRepr - - - --- | Generate a fresh bit-vector thing. -freshBits :: - (Rep t ~ LLVMPointerType (BitSize t), 1 <= BitSize t) => - String -> - X86 t -> - Spec Pre (Value t) -freshBits str x = - withSym $ \sym -> - do nm <- symName str - bv <- freshConstant sym nm (BaseBVRepr (bitSize x)) - value x <$> llvmPointer_bv sym bv - - - --- | An uninitialized pointer value. -freshPtr :: String -> Spec Pre (Value APtr) -freshPtr str = - do ptr <- withSym $ \sym -> - do base_nm <- symName (str ++ "_base") - off_nm <- symName (str ++ "_offset") - base <- freshConstant sym base_nm BaseNatRepr - offs <- freshConstant sym off_nm (BaseBVRepr knownNat) - return (Value (LLVMPointer base offs)) - isPtr ptr True - return ptr - --- | Generate a fresh value for a general purpose register. -freshGP :: GPReg -> GPRegUse t -> Spec Pre (Value t) -freshGP x u = - case u of - AsBits -> fresh QWord (show x) - AsPtr -> fresh Ptr (show x) - - --- | Generate fresh values for a class of registers. -freshRegs :: - forall a. - (Show a, Enum a, Bounded a, Infer (RegType a)) => - Spec Pre (a -> Value (RegType a)) -freshRegs = - do vs <- Vector.fromList <$> - mapM (\a -> fresh infer (show (a :: a))) elemList - return (\x -> vs Vector.! fromEnum x) - -symName :: String -> IO SolverSymbol -symName s = case userSymbol s of - Left err -> fail (show err) - Right a -> return a - - -elemList :: (Enum a, Bounded a) => [a] -elemList = [ minBound .. maxBound ] diff --git a/src/SAWScript/X86Spec/Literal.hs b/src/SAWScript/X86Spec/Literal.hs deleted file mode 100644 index 63f511dbb5..0000000000 --- a/src/SAWScript/X86Spec/Literal.hs +++ /dev/null @@ -1,38 +0,0 @@ -{-# Language DataKinds #-} -{-# Language TypeOperators #-} -{-# Language TypeFamilies #-} -{-# Language TypeSynonymInstances #-} -module SAWScript.X86Spec.Literal (literal, Literal(..)) where - -import GHC.TypeLits (type (<=)) - -import What4.Interface(bvLit, truePred, falsePred) -import SAWScript.CrucibleLLVM (llvmPointer_bv) - -import SAWScript.X86Spec.Types -import SAWScript.X86Spec.Monad - --- | Types that support literals. -class Literal t where - type Lit t - literalAt :: X86 t -> Lit t -> Spec p (Value t) - -literal :: (Literal t, Infer t) => Lit t -> Spec p (Value t) -literal = literalAt infer - -instance Literal ABool where - type Lit ABool = Bool - literalAt _ b = - do sym <- getSym - return (Value (if b then truePred sym else falsePred sym)) - -instance (1 <= n) => Literal (Bits n) where - type Lit (Bits n) = Integer - literalAt (Bits w) val = - withSym $ \sym -> - value (Bits w) <$> (llvmPointer_bv sym =<< bvLit sym w val) - --- XXX: Big float? - - - diff --git a/src/SAWScript/X86Spec/Memory.hs b/src/SAWScript/X86Spec/Memory.hs deleted file mode 100644 index 4b0d626543..0000000000 --- a/src/SAWScript/X86Spec/Memory.hs +++ /dev/null @@ -1,211 +0,0 @@ -{-# Language ImplicitParams #-} -{-# Language DataKinds #-} -{-# Language TypeFamilies #-} -{-# Language TypeSynonymInstances #-} -{-# Language FlexibleInstances #-} -module SAWScript.X86Spec.Memory - ( MemType(..) - , SizeOf(..) - , WriteMem(..) - , AllocBytes(..) - , allocArray - , allocArrayOf - , readMem - , readArray - , PtrAdd(..) - , Bytes - , toBytes - , bytesToInteger - , Mutability(..) - , (.*) - ) where - -import GHC.TypeLits(Nat) - -import Data.Parameterized.NatRepr(NatRepr,knownNat,natValue) - -import SAWScript.CrucibleLLVM - ( AllocType(HeapAlloc), Mutability(..) - , storeConstRaw, doLoad, doMalloc, doPtrAddOffset, packMemValue - , Bytes, toBytes, bytesToInteger - , projectLLVM_bv, bitvectorType - , StorageType - , noAlignment - ) - -import SAWScript.X86Spec.Types -import SAWScript.X86Spec.Monad -import SAWScript.X86Spec.Literal - --- | Types that can be stored in memory. -class MemType (t :: X86Type) where - -- | Size of the type, in bytes. - type ByteSize t :: Nat - byteSizeNat :: X86 t -> NatRepr (ByteSize t) - -instance MemType (Bits 8) where - type ByteSize (Bits 8) = 1 - byteSizeNat _ = knownNat - -instance MemType (Bits 16) where - type ByteSize (Bits 16) = 2 - byteSizeNat _ = knownNat - -instance MemType (Bits 32) where - type ByteSize (Bits 32) = 4 - byteSizeNat _ = knownNat - -instance MemType (Bits 64) where - type ByteSize (Bits 64) = 8 - byteSizeNat _ = knownNat - -instance MemType (Bits 128) where - type ByteSize (Bits 128) = 16 - byteSizeNat _ = knownNat - -instance MemType (Bits 256) where - type ByteSize (Bits 256) = 32 - byteSizeNat _ = knownNat - -instance MemType APtr where - type ByteSize APtr = 8 - byteSizeNat _ = knownNat - - -class SizeOf t where - sizeOf :: t -> Bytes - -instance MemType t => SizeOf (X86 t) where - sizeOf = toBytes . natValue . byteSizeNat - -instance (MemType t, Infer t) => SizeOf (Value t) where - sizeOf = sizeOf . typeOf - --- | Multiply a size by a constant. --- Useful for working with arrays (sizes, advnacing, etc.) -(.*) :: SizeOf t => Integer -> t -> Bytes -n .* t = toBytes (n * bytesToInteger (sizeOf t)) - --- | The LLVM type used when manipulating values of the given type in memory. -llvmType :: SizeOf t => t -> StorageType -llvmType x = bitvectorType (sizeOf x) - - -class WriteMem t where - writeMem :: Value APtr -> t -> Spec Pre () - -instance (MemType t, a ~ X86 t) => WriteMem (a, Value t) where - writeMem (Value p) (w,Value x) = - updMem_ $ \sym mem -> - do let ?ptrWidth = knownNat - let ty = llvmType w - val <- packMemValue sym ty (crucRepr w) x - -- Here we use the write that ignores mutability. - -- This is because we are writing initialization code. - let alignment = noAlignment -- default to byte-aligned (FIXME) - storeConstRaw sym mem p ty alignment val - -instance (MemType t, Infer t) => WriteMem (Value t) where - writeMem p x = writeMem p (infer, x) - -instance (MemType t, a ~ X86 t) => WriteMem (a, [Value t]) where - writeMem p (t,xs) = - case xs of - [] -> return () - v : vs -> do writeMem p (t,v) - p1 <- ptrAdd p (sizeOf t) - writeMem p1 (t,vs) - - - -instance (SizeOf t, WriteMem t) => WriteMem [t] where - writeMem p xs = - case xs of - [] -> return () - v : vs -> do writeMem p v - p1 <- ptrAdd p (sizeOf v) - writeMem p1 vs - - - --- | Read a value from memory. --- Currently this is an unaligned read (i.e., any alignment will do). --- We probably want to have an aligned read also. -readMem :: MemType t => X86 t -> Value APtr -> Spec Post (Value t) -readMem w (Value p) = - withMem $ \sym mem -> - do let ?ptrWidth = knownNat - Value <$> doLoad sym mem p (llvmType w) (crucRepr w) noAlignment - - - --- | Allocate a pointer that points to the given number of bytes (on the heap). --- The allocated memory is not initialized, so it should not be read until --- it has been initialized. -class AllocBytes t where - allocBytes :: String -> Mutability -> t -> Spec Pre (Value APtr) - -instance (t ~ Bits 64) => AllocBytes (Value t) where - allocBytes str mut (Value n) = - let ?ptrWidth = knownNat in - updMem $ \sym m -> - do sz <- projectLLVM_bv sym n - let alignment = noAlignment -- default to byte-aligned (FIXME) - (v,mem1) <- doMalloc sym HeapAlloc mut str m sz alignment - return (Value v, mem1) - -instance AllocBytes Bytes where - allocBytes str mut b = allocBytes str mut =<< literal (bytesToInteger b) - - -class PtrAdd t where - ptrAdd :: Value APtr -> t -> Spec p (Value APtr) - -instance (t ~ Bits 64) => PtrAdd (Value t) where - ptrAdd (Value p) (Value o) = withMem $ \sym mem -> - let ?ptrWidth = knownNat - in Value <$> (doPtrAddOffset sym Nothing mem p =<< projectLLVM_bv sym o) - -instance PtrAdd Bytes where - ptrAdd p x = ptrAdd p =<< literal (bytesToInteger x) - - - - --- | Allocate an array, an initialize it with the given values. -allocArray :: - (Infer t, MemType t) => - String -> - Mutability -> - [ Value t ] -> - Spec Pre (Value APtr) -allocArray = allocArrayOf infer - --- | Allocate an array with elements of the given type. --- Initialize it with the given values. -allocArrayOf :: - MemType t => - X86 t -> String -> Mutability -> [Value t] -> Spec Pre (Value APtr) -allocArrayOf ty str mut xs = - do let n = fromIntegral (length xs) - bs = bytesToInteger (sizeOf ty) - sz <- literal (n * bs) - ptr <- allocBytes str mut sz - writeMem ptr (ty,xs) - return ptr - - - --- | Read out an array of values of the given type. -readArray :: - MemType t => - X86 t -> - Value APtr -> - Integer -> - Spec Post [ Value t ] -readArray ty p n - | n > 0 = do v <- readMem ty p - p1 <- ptrAdd p (sizeOf ty) - vs <- readArray ty p1 (n-1) - return (v : vs) - | otherwise = return [] diff --git a/src/SAWScript/X86Spec/Monad.hs b/src/SAWScript/X86Spec/Monad.hs deleted file mode 100644 index c45d5e66c1..0000000000 --- a/src/SAWScript/X86Spec/Monad.hs +++ /dev/null @@ -1,307 +0,0 @@ -{-# Language DataKinds #-} -{-# Language TypeFamilies #-} -{-# Language UndecidableInstances #-} -{-# Language TypeSynonymInstances #-} -{-# Language PatternSynonyms #-} -module SAWScript.X86Spec.Monad - ( SpecType, Pre, Post - , Spec - , runPreSpec, runPostSpec - , io - , getSym - , withSym - , updMem - , updMem_ - , withMem - , registerRegion - , lookupReg - , InPre(..) - , isPtr - , assume - , assert - , getSharedContext - , withSharedContext - , cryTerm - , cryConst - , PreExtra(..) - -- , registerSymFuns - -- , SymFunTerms(..) - , lookupCry - ) where - -import Control.Monad(liftM,ap) -import Data.Map ( Map ) -import qualified Data.Map as Map - -import Data.Parameterized.Context(Assignment) - -import What4.Interface - (natLit,notPred,natEq,getCurrentProgramLoc) - -import SAWScript.CrucibleLLVM - ( EndianForm(LittleEndian) - , Mem, emptyMem, LLVMPointerType - , pattern LLVMPointer, LLVMPtr, ppPtr - ) -import Lang.Crucible.Simulator.RegValue(RegValue,RegValue'(..)) -import Lang.Crucible.Simulator.SimError(SimErrorReason(..), SimError(..)) -import Lang.Crucible.Backend - (addAssertion,addAssumption,AssumptionReason(..),LabeledPred(..)) -import Lang.Crucible.Backend.SAWCore (sawBackendSharedContext) - -import Verifier.SAW.SharedTerm(Term,SharedContext,scApplyAll) - -import Verifier.SAW.CryptolEnv(CryptolEnv(..), lookupIn, getAllIfaceDecls) - -import Cryptol.ModuleSystem.Name(Name) -import Cryptol.ModuleSystem.Interface(ifTySyns) -import Cryptol.TypeCheck.AST(TySyn(tsDef)) -import Cryptol.TypeCheck.TypePat(aNat) -import Cryptol.Utils.PP(alwaysQualify,runDoc,pp) -import Cryptol.Utils.Patterns(matchMaybe) - -import Data.Macaw.Memory(RegionIndex) -import Data.Macaw.Symbolic(MacawCrucibleRegTypes, ToCrucibleType) -import Data.Macaw.X86.ArchTypes(X86_64) -import Data.Macaw.X86.Symbolic(lookupX86Reg) -import Data.Macaw.X86.X86Reg(X86Reg) - - -import SAWScript.X86Spec.Types - --- | Is this a pre- or post-condition specificiation. -data {- kind -} SpecType = Pre | Post - --- | We are specifying a pre-condition. -type Pre = 'Pre - --- | We are specifying a post-condition. -type Post = 'Post - - --- | A monad for definingin specifications. -newtype Spec (p :: SpecType) a = - Spec ((Sym, CryptolEnv) -> - RR p -> - (RegValue Sym Mem, SS p) -> IO (a, (RegValue Sym Mem, SS p))) - --- | Interanl state to be passed from the pre-spec to the post-spec -data PreExtra = PreExtra { theMem :: RegValue Sym Mem - , theRegions :: Map RegionIndex (LLVMPtr Sym 64) - } - --- | Execute a pre-condition specification. -runPreSpec :: - Sym -> - CryptolEnv {- ^ Contains Cryptol declarations we may use -} -> - Spec Pre a -> IO (a, PreExtra) -runPreSpec sym cs (Spec f) = - do m0 <- emptyMem LittleEndian - (a,(m,rs)) <- f (sym,cs) () (m0, Map.empty) - return (a, PreExtra { theMem = m, theRegions = rs }) - - - --- | Execute a post-condition specification. -runPostSpec :: - Sym -> - CryptolEnv -> - Assignment (RegValue' Sym) (MacawCrucibleRegTypes X86_64) -> - RegValue Sym Mem -> - Spec Post () -> - IO () -runPostSpec sym cry rs mem (Spec f) = fst <$> f (sym, cry) rs (mem, ()) - -type family RR (x :: SpecType) where - RR Pre = () - RR Post = Assignment (RegValue' Sym) (MacawCrucibleRegTypes X86_64) - -type family SS (x :: SpecType) where - SS Pre = Map RegionIndex (LLVMPtr Sym 64) - SS Post = () - -instance Functor (Spec p) where fmap = liftM - -instance Applicative (Spec p) where - pure a = Spec (\_ _ m -> return (a,m)) - (<*>) = ap - -instance Monad (Spec p) where - Spec m >>= k = Spec (\r x s -> do (a, s1) <- m r x s - let Spec m1 = k a - m1 r x s1) - -io :: IO a -> Spec p a -io m = Spec (\_ _ s -> do a <- m - return (a,s)) - -getSym :: Spec p Sym -getSym = Spec (\(r,_) _ s -> return (r,s)) - -withSym :: (Sym -> IO a) -> Spec p a -withSym f = - do s <- getSym - io (f s) - -getSharedContext :: Spec p SharedContext -getSharedContext = withSym sawBackendSharedContext - -withSharedContext :: (SharedContext -> IO a) -> Spec p a -withSharedContext f = - do s <- getSharedContext - io (f s) - --- | Lookup a cryptol term, and apply it to the given arguments, --- returning the result. -cryTerm :: String -> [Term] -> Spec p Term -cryTerm x xs = Spec (\(sym,cs) _ s -> - do t <- lookupCry x (eTermEnv cs) - sc <- sawBackendSharedContext sym - t1 <- scApplyAll sc t xs - return (t1,s)) - --- | Lookup a Crytpol type synonym, which should resolve to a constant. -cryConst :: String -> Spec p Integer -cryConst x = Spec (\(_,cs) _ s -> - do let mp = ifTySyns (getAllIfaceDecls (eModuleEnv cs)) - t <- lookupCry x mp - case matchMaybe (aNat (tsDef t)) of - Just n -> return (n,s) - Nothing -> fail (x ++ " is not a fixed constant type synonym.") - ) - --- | Lookup a name in a map indexed by Cryptol names. -lookupCry :: String -> Map Name a -> IO a -lookupCry x mp = - case x `lookupIn` mp of - Left [] -> fail $ unlines $ ("Missing Cryptol name: " ++ show x) - : [ "*** " ++ ppName y | y <- Map.keys mp ] - Left ys -> fail $ unlines ( "Ambiguous Cryptol name:" - : [ "*** " ++ ppName y | y <- ys ] - ) - Right a -> return a - - where ppName = show . runDoc alwaysQualify . pp - - -updMem :: (Sym -> RegValue Sym Mem -> IO (a, RegValue Sym Mem)) -> Spec Pre a -updMem f = Spec (\r _ (s1,s2) -> do (a,s1') <- f (fst r) s1 - return (a, (s1',s2))) - -updMem_ :: (Sym -> RegValue Sym Mem -> IO (RegValue Sym Mem)) -> Spec Pre () -updMem_ f = updMem (\sym mem -> do mem1 <- f sym mem - return ((),mem1)) - -withMem :: (Sym -> RegValue Sym Mem -> IO a) -> Spec p a -withMem f = Spec (\r _ s -> f (fst r) (fst s) >>= \a -> return (a,s)) - -lookupReg :: - (ToCrucibleType t ~ Rep ty) => X86Reg t -> Spec Post (Value ty) -lookupReg r = Spec (\_ regs s -> - case lookupX86Reg r regs of - Nothing -> fail ("Unknown register: " ++ show r) - Just (RV v) -> return (Value v,s)) - -registerRegion :: RegionIndex -> Value APtr -> Spec Pre () -registerRegion r (Value x) = Spec (\_ _ (s1,s2) -> - if Map.member r s2 - then fail ("Multiple declarations for global region: " ++ show r) - else return ((), (s1, Map.insert r x s2))) - -class InPre p where - inPre :: Spec p Bool - -instance InPre Pre where - inPre = return True - -instance InPre Post where - inPre = return False - --- | State if this value should be a pointer. --- In pre-condition we assume it, in post-conditions we assert it. -isPtr :: (Rep t ~ LLVMPointerType 64, InPre p) => - Value t -> - Bool -> - Spec p () -isPtr (Value pt@(LLVMPointer base _off)) yes = - do sym <- getSym - ok <- io $ do isBits <- natEq sym base =<< natLit sym 0 - if yes then notPred sym isBits else return isBits - - pre <- inPre - loc <- io $ getCurrentProgramLoc sym - io $ if pre - then addAssumption sym (LabeledPred ok (AssumptionReason loc "precondition")) - else addAssertion sym (LabeledPred ok (SimError loc (AssertFailureSimError msg))) - where - msg' | yes = "Expected a pointer, but encounterd a bit value." - | otherwise = "Expected a bit value, but encounterd a pointer." - - msg = unlines [ msg', show (ppPtr pt) ] - --- The input should be a boolean SAW Core term. -assume :: Value ABool {- ^ Boolean assumption -} -> Spec Pre () -assume (Value p) = - do sym <- getSym - loc <- io $ getCurrentProgramLoc sym - io $ addAssumption sym (LabeledPred p (AssumptionReason loc "assumption")) - --- | Add an assertion to the post-condition. -assert :: - Value ABool {- ^ Boolean assertion, should be true -} -> - String {- ^ A message to show if the assrtion fails -} -> - Spec Post () -assert (Value p) msg = - do sym <- getSym - loc <- io $ getCurrentProgramLoc sym - io $ addAssertion sym (LabeledPred p (SimError loc (AssertFailureSimError msg))) - - --------------------------------------------------------------------------------- --- Symbolic terms - -{- -{- | The SAW core terms used to implement the given instructions. -During simulation, these instructions are threated as uninterpred -functions, but in the post conditions we use these intepretations. -For the types, plase have a look at "SymFuns" in "Data.Macaw.X86.Crucible" -from the "macaw-x86-symbolic" pacakge. -} -data SymFunTerms = SymFunTerms - { termAesEnc :: - SharedContext -> Term{-128-} -> Term{-128-} -> IO Term{-128-} - - , termAesEncLast :: - SharedContext -> Term{-128-} -> Term{-128-} -> IO Term{-128-} - - , termClMul :: - SharedContext -> Term{- 64-} -> Term{- 64-} -> IO Term{-128-} - } - --- | Add interpretations for the symbolic functions. -registerSymFuns :: SymFunTerms -> Spec Pre () -registerSymFuns defs = Spec $ \(sym,_) symFs st -> - do let mk2 nm f = \sc xs -> case xs of - [a,b] -> f defs sc a b - _ -> fail (err nm xs) - - sawRegisterSymFunInterp sym (fnAesEnc symFs) $ - mk2 "aesenc" termAesEnc - - sawRegisterSymFunInterp sym (fnAesEncLast symFs) $ - mk2 "aesenclast" termAesEncLast - - sawRegisterSymFunInterp sym (fnClMul symFs) $ - mk2 "clmul" termClMul - - return ((),st) - - where - err nm xs = - unlines [ "Type error in call to " ++ show (nm::String) ++ ":" - , "*** Expected: 2 arguments" - , "*** Given: " ++ show (length xs) ++ " arguments" - ] - - - --} diff --git a/src/SAWScript/X86Spec/Registers.hs b/src/SAWScript/X86Spec/Registers.hs deleted file mode 100644 index bef944a28f..0000000000 --- a/src/SAWScript/X86Spec/Registers.hs +++ /dev/null @@ -1,360 +0,0 @@ -{-# Language RecordWildCards #-} -{-# Language TypeSynonymInstances #-} -{-# Language GADTs #-} -{-# Language TypeFamilies #-} -{-# Language ScopedTypeVariables #-} -{-# Language TypeApplications #-} -{-# Language DataKinds #-} -{-# Language FlexibleInstances #-} -{-# Language FlexibleContexts #-} -module SAWScript.X86Spec.Registers - ( -- * Register names - IP(..) - , GPReg(..) - , Flag(..) - , VecReg(..) - , X87Status(..) - , X87Top(..) - , X87Tag(..) - , FPReg(..) - - -- * Accessing Register - , RegType - , GetReg(..) - - -- * Register assignment - , RegAssign(..) - , GPRegVal(..), GPValue(..), GPRegUse(..) - , macawLookup - ) where - -import qualified Flexdis86 as F - -import Lang.Crucible.Simulator.RegValue(RegValue'(RV)) - -import Data.Macaw.Symbolic(ToCrucibleType) -import qualified Data.Macaw.X86.X86Reg as R - -import SAWScript.X86Spec.Types -import SAWScript.X86Spec.Monad - - --- | Instruciotn pointer. -data IP = IP - deriving (Show,Eq,Ord,Enum,Bounded) - --- | General purpose register. -data GPReg = RAX | RBX | RCX | RDX | RSI | RDI | RSP | RBP - | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 - deriving (Show,Eq,Ord,Enum,Bounded) - --- | General purpose reigsters may contain either a bit-value or a pointer. --- This type specifies which form we want to access. -data GPRegUse t where - AsBits :: GPRegUse (Bits 64) - AsPtr :: GPRegUse APtr - --- | The value of a general purpose register. -data GPRegVal = GPBits (Value (Bits 64)) | GPPtr (Value APtr) - --- | A convenient way to construct general purpose values, based on their type. -class GPValue t where - gpValue :: Value t -> GPRegVal - -instance (n ~ 64) => GPValue (Bits n) where gpValue = GPBits -instance GPValue APtr where gpValue = GPPtr - - --- | CPU flags -data Flag = CF | PF | AF | ZF | SF | TF | IF | DF | OF - deriving (Show,Eq,Ord,Enum,Bounded) - - --- | Vector registers. -data VecReg = - YMM0 | YMM1 | YMM2 | YMM3 | YMM4 | YMM5 | YMM6 | YMM7 - | YMM8 | YMM9 | YMM10 | YMM11 | YMM12 | YMM13 | YMM14 | YMM15 - deriving (Show,Eq,Ord,Enum,Bounded) - - --- | X87 status registers. -data X87Status = X87_IE | X87_DE | X87_ZE | X87_OE - | X87_UE | X87_PE | X87_EF | X87_ES - | X87_C0 | X87_C1 | X87_C2 | X87_C3 - deriving (Show,Eq,Ord,Enum,Bounded) - - --- | Top of X87 register stack. -data X87Top = X87Top - deriving (Show,Eq,Ord,Enum,Bounded) - --- | X87 tags. -data X87Tag = Tag0 | Tag1 | Tag2 | Tag3 - | Tag4 | Tag5 | Tag6 | Tag7 - deriving (Show,Eq,Ord,Enum,Bounded) - --- | 80-bit floating point registers. -data FPReg = FP0 | FP1 | FP2 | FP3 | FP4 | FP5 | FP6 | FP7 - deriving (Show,Eq,Ord,Enum,Bounded) - - --- | A register assignment. -data RegAssign = RegAssign - { valIP :: Value (Bits 64) - , valGPReg :: GPReg -> GPRegVal - , valVecReg :: VecReg -> Value (Bits 256) - , valFPReg :: FPReg -> Value ABigFloat - , valFlag :: Flag -> Value ABool - , valX87Status :: X87Status -> Value ABool - , valX87Top :: Value (Bits 3) - , valX87Tag :: X87Tag -> Value (Bits 2) - } - - --- | Convert a register assignment to a form suitable for Macaw CFG generation. -macawLookup :: RegAssign -> R.X86Reg t -> RegValue' Sym (ToCrucibleType t) -macawLookup RegAssign { .. } reg = - case reg of - R.X86_IP -> toRV valIP - - R.RAX -> gp RAX - R.RBX -> gp RBX - R.RCX -> gp RCX - R.RDX -> gp RDX - R.RSI -> gp RSI - R.RDI -> gp RDI - R.RSP -> gp RSP - R.RBP -> gp RBP - R.R8 -> gp R8 - R.R9 -> gp R9 - R.R10 -> gp R10 - R.R11 -> gp R11 - R.R12 -> gp R12 - R.R13 -> gp R13 - R.R14 -> gp R14 - R.R15 -> gp R15 - R.X86_GP _ -> error "[bug] Unexpecet general purpose register." - - R.YMM 0 -> vec YMM0 - R.YMM 1 -> vec YMM1 - R.YMM 2 -> vec YMM2 - R.YMM 3 -> vec YMM3 - R.YMM 4 -> vec YMM4 - R.YMM 5 -> vec YMM5 - R.YMM 6 -> vec YMM6 - R.YMM 7 -> vec YMM7 - R.YMM 8 -> vec YMM8 - R.YMM 9 -> vec YMM9 - R.YMM 10 -> vec YMM10 - R.YMM 11 -> vec YMM11 - R.YMM 12 -> vec YMM12 - R.YMM 13 -> vec YMM13 - R.YMM 14 -> vec YMM14 - R.YMM 15 -> vec YMM15 - R.X86_YMMReg _ -> error "[bug] Unexpected YMM register." - - R.X87_FPUReg (F.MMXR 0) -> fp FP0 - R.X87_FPUReg (F.MMXR 1) -> fp FP1 - R.X87_FPUReg (F.MMXR 2) -> fp FP2 - R.X87_FPUReg (F.MMXR 3) -> fp FP3 - R.X87_FPUReg (F.MMXR 4) -> fp FP4 - R.X87_FPUReg (F.MMXR 5) -> fp FP5 - R.X87_FPUReg (F.MMXR 6) -> fp FP6 - R.X87_FPUReg (F.MMXR 7) -> fp FP7 - R.X87_FPUReg _ -> error "[bug] Unexpected FPUReg register." - - R.CF -> flag CF - R.PF -> flag PF - R.AF -> flag AF - R.ZF -> flag ZF - R.SF -> flag SF - R.TF -> flag TF - R.IF -> flag IF - R.DF -> flag DF - R.OF -> flag OF - R.X86_FlagReg _ -> error "[bug] Unexpected flag register." - - R.X87_IE -> x87_status X87_IE - R.X87_DE -> x87_status X87_DE - R.X87_ZE -> x87_status X87_ZE - R.X87_OE -> x87_status X87_OE - R.X87_UE -> x87_status X87_UE - R.X87_PE -> x87_status X87_PE - R.X87_EF -> x87_status X87_EF - R.X87_ES -> x87_status X87_ES - R.X87_C0 -> x87_status X87_C0 - R.X87_C1 -> x87_status X87_C1 - R.X87_C2 -> x87_status X87_C2 - R.X87_C3 -> x87_status X87_C3 - - R.X87_StatusReg n -> - error ("[bug] Unexpected X87 status register: " ++ show n) - - R.X87_TopReg -> toRV valX87Top - - R.X87_TagReg 0 -> tag Tag0 - R.X87_TagReg 1 -> tag Tag1 - R.X87_TagReg 2 -> tag Tag2 - R.X87_TagReg 3 -> tag Tag3 - R.X87_TagReg 4 -> tag Tag4 - R.X87_TagReg 5 -> tag Tag5 - R.X87_TagReg 6 -> tag Tag6 - R.X87_TagReg 7 -> tag Tag7 - R.X87_TagReg _ -> error "[bug] Unexpecte X87 tag" - - - where - gp r = case valGPReg r of - GPBits x -> toRV x - GPPtr x -> toRV x - vec r = toRV (valVecReg r) - fp r = toRV (valFPReg r) - flag r = toRV (valFlag r) - x87_status r = toRV (valX87Status r) - tag r = toRV (valX87Tag r) - - - -toRV :: Value t -> RegValue' Sym (Rep t) -toRV (Value x) = RV x - - - --- | The type of value stored in a register. Used for reading registers. -type family RegType a where - RegType IP = Bits 64 - RegType (GPReg,GPRegUse t) = t - RegType Flag = ABool - RegType VecReg = Bits 256 - RegType X87Status = ABool - RegType X87Top = Bits 3 - RegType X87Tag = Bits 2 - RegType FPReg = ABigFloat - - - - - --- | Get the value of a register. -class GetReg a where - getReg :: a -> Spec Post (Value (RegType a)) - - -lookupRegGP :: R.X86Reg R.GP -> GPRegUse t -> Spec Post (Value t) -lookupRegGP r how = - case how of - AsBits -> do v <- lookupReg r - isPtr v False - return v - AsPtr -> do v <- lookupReg r - isPtr v True - return v - - - -instance GetReg IP where - getReg _ = lookupReg R.X86_IP - -instance GetReg (GPReg,GPRegUse t) where - getReg (x,use) = - case x of - RAX -> lookupRegGP R.RAX use - RBX -> lookupRegGP R.RBX use - RCX -> lookupRegGP R.RCX use - RDX -> lookupRegGP R.RDX use - RSI -> lookupRegGP R.RSI use - RDI -> lookupRegGP R.RDI use - RSP -> lookupRegGP R.RSP use - RBP -> lookupRegGP R.RBP use - R8 -> lookupRegGP R.R8 use - R9 -> lookupRegGP R.R9 use - R10 -> lookupRegGP R.R10 use - R11 -> lookupRegGP R.R11 use - R12 -> lookupRegGP R.R12 use - R13 -> lookupRegGP R.R13 use - R14 -> lookupRegGP R.R14 use - R15 -> lookupRegGP R.R15 use - - -instance GetReg Flag where - getReg f = - case f of - CF -> lookupReg R.CF - PF -> lookupReg R.PF - AF -> lookupReg R.AF - ZF -> lookupReg R.ZF - SF -> lookupReg R.SF - TF -> lookupReg R.TF - IF -> lookupReg R.IF - DF -> lookupReg R.DF - OF -> lookupReg R.OF - - -instance GetReg VecReg where - getReg f = - case f of - YMM0 -> lookupReg (R.YMM 0) - YMM1 -> lookupReg (R.YMM 1) - YMM2 -> lookupReg (R.YMM 2) - YMM3 -> lookupReg (R.YMM 3) - YMM4 -> lookupReg (R.YMM 4) - YMM5 -> lookupReg (R.YMM 5) - YMM6 -> lookupReg (R.YMM 6) - YMM7 -> lookupReg (R.YMM 7) - YMM8 -> lookupReg (R.YMM 8) - YMM9 -> lookupReg (R.YMM 9) - YMM10 -> lookupReg (R.YMM 10) - YMM11 -> lookupReg (R.YMM 11) - YMM12 -> lookupReg (R.YMM 12) - YMM13 -> lookupReg (R.YMM 13) - YMM14 -> lookupReg (R.YMM 14) - YMM15 -> lookupReg (R.YMM 15) - - -instance GetReg X87Status where - getReg f = - case f of - X87_IE -> lookupReg R.X87_IE - X87_DE -> lookupReg R.X87_DE - X87_ZE -> lookupReg R.X87_ZE - X87_OE -> lookupReg R.X87_OE - X87_UE -> lookupReg R.X87_UE - X87_PE -> lookupReg R.X87_PE - X87_EF -> lookupReg R.X87_EF - X87_ES -> lookupReg R.X87_ES - X87_C0 -> lookupReg R.X87_C0 - X87_C1 -> lookupReg R.X87_C1 - X87_C2 -> lookupReg R.X87_C2 - X87_C3 -> lookupReg R.X87_C3 - -instance GetReg X87Top where - getReg _ = lookupReg R.X87_TopReg - - -instance GetReg X87Tag where - getReg t = - case t of - Tag0 -> lookupReg (R.X87_TagReg 0) - Tag1 -> lookupReg (R.X87_TagReg 1) - Tag2 -> lookupReg (R.X87_TagReg 2) - Tag3 -> lookupReg (R.X87_TagReg 3) - Tag4 -> lookupReg (R.X87_TagReg 4) - Tag5 -> lookupReg (R.X87_TagReg 5) - Tag6 -> lookupReg (R.X87_TagReg 6) - Tag7 -> lookupReg (R.X87_TagReg 7) - - - -instance GetReg FPReg where - getReg t = - case t of - FP0 -> lookupReg (fp 0) - FP1 -> lookupReg (fp 1) - FP2 -> lookupReg (fp 2) - FP3 -> lookupReg (fp 3) - FP4 -> lookupReg (fp 4) - FP5 -> lookupReg (fp 5) - FP6 -> lookupReg (fp 6) - FP7 -> lookupReg (fp 7) - where fp = R.X87_FPUReg . F.mmxReg - diff --git a/src/SAWScript/X86Spec/SAW.hs b/src/SAWScript/X86Spec/SAW.hs deleted file mode 100644 index 69bf49dd30..0000000000 --- a/src/SAWScript/X86Spec/SAW.hs +++ /dev/null @@ -1,30 +0,0 @@ -{-# Language DataKinds #-} -{-# Language TypeOperators #-} -{-# Language TypeSynonymInstances #-} -{-# Language TypeFamilies #-} -module SAWScript.X86Spec.SAW (SAW(..)) where - -import What4.BaseTypes (BaseTypeRepr(BaseBVRepr,BaseBoolRepr)) -import SAWScript.CrucibleLLVM (llvmPointer_bv, projectLLVM_bv) -import Lang.Crucible.Backend.SAWCore(bindSAWTerm, toSC) - -import Verifier.SAW.SharedTerm(Term) - -import SAWScript.X86Spec.Types -import SAWScript.X86Spec.Monad - --- | Convert between values and SAW Core terms. -class SAW t where - saw :: X86 t -> Term -> Spec p (Value t) - toSAW :: Value t -> Spec p Term - -instance SAW ABool where - saw _ val = withSym $ \sym -> Value <$> bindSAWTerm sym BaseBoolRepr val - toSAW (Value v) = withSym $ \sym -> toSC sym v - -instance SAW (Bits n) where - saw (Bits w) val = - withSym $ \sym -> do bv <- bindSAWTerm sym (BaseBVRepr w) val - value (Bits w) <$> llvmPointer_bv sym bv - toSAW (Value v) = withSym $ \sym -> toSC sym =<< projectLLVM_bv sym v - diff --git a/src/SAWScript/X86Spec/Types.hs b/src/SAWScript/X86Spec/Types.hs deleted file mode 100644 index 14dbc0f8ef..0000000000 --- a/src/SAWScript/X86Spec/Types.hs +++ /dev/null @@ -1,168 +0,0 @@ -{-# Language DataKinds #-} -{-# Language GADTs #-} -{-# Language KindSignatures #-} -{-# Language TypeApplications #-} -{-# Language ScopedTypeVariables #-} -{-# Language TypeFamilies #-} -{-# Language TypeSynonymInstances #-} -{-# Language PatternSynonyms #-} -{-# Language ViewPatterns #-} -{-# Language TypeOperators #-} - -module SAWScript.X86Spec.Types - ( X86Type - , Bits, APtr, ABool, ABigFloat - , X86(..) - , Infer(..) - , typeOf - , BitSize, bitSize - - , pattern Byte - , pattern Word - , pattern DWord - , pattern QWord - , pattern V128 - , pattern V256 - - -- * Mapping to Crucible - , Sym, Rep, crucRepr - - -- * Values - , Value(..), value - ) where - -import Data.Kind(Type) -import GHC.TypeLits(Nat,KnownNat) - -import Data.Parameterized.NatRepr -import Data.Parameterized.Classes(knownRepr) -import Data.Parameterized.Nonce(GlobalNonceGenerator) - -import Lang.Crucible.Backend.SAWCore(SAWCoreBackend) -import Lang.Crucible.Simulator.RegValue(RegValue) -import Lang.Crucible.Types(CrucibleType,TypeRepr,BoolType) - -import SAWScript.CrucibleLLVM (LLVMPointerType, pattern LLVMPointerRepr) - -import qualified What4.Expr.Builder as B - --- | The kind of X86 types. -data {- kind -} X86Type = APtr | ABits Nat | ABool | ABigFloat - -type Bits = 'ABits -type APtr = 'APtr -type ABool = 'ABool -type ABigFloat = 'ABigFloat - -pattern Byte :: () => (t ~ Bits 8) => X86 t -pattern Byte <- Bits (testEquality n8 -> Just Refl) - where Byte = Bits n8 - -pattern Word :: () => (t ~ Bits 16) => X86 t -pattern Word <- Bits (testEquality n16 -> Just Refl) - where Word = Bits n16 - -pattern DWord :: () => (t ~ Bits 32) => X86 t -pattern DWord <- Bits (testEquality n32 -> Just Refl) - where DWord = Bits n32 - -pattern QWord :: () => (t ~ Bits 64) => X86 t -pattern QWord <- Bits (testEquality n64 -> Just Refl) - where QWord = Bits n64 - -pattern V128 :: () => (t ~ Bits 128) => X86 t -pattern V128 <- Bits (testEquality n128 -> Just Refl) - where V128 = Bits n128 - -pattern V256 :: () => (t ~ Bits 256) => X86 t -pattern V256 <- Bits (testEquality n256 -> Just Refl) - where V256 = Bits n256 - - -n8 :: NatRepr 8 -n8 = knownNat - -n16 :: NatRepr 16 -n16 = knownNat - -n32 :: NatRepr 32 -n32 = knownNat - -n64 :: NatRepr 64 -n64 = knownNat - -n128 :: NatRepr 128 -n128 = knownNat - -n256 :: NatRepr 256 -n256 = knownNat - - --- | This type is used to specify types explicitly. -data X86 :: X86Type -> Type where - Bits :: (1 <= n) => NatRepr n -> X86 (Bits n) - Ptr :: X86 APtr - Bool :: X86 ABool - BigFloat :: X86 ABigFloat - --- | This type may be used to specify types implicitly --- (i.e., in contexts where the type can be inferred automatically). -class Infer t where - infer :: X86 t - -instance (1 <= n, KnownNat n) => - Infer (Bits n) where infer = Bits knownNat -instance Infer APtr where infer = Ptr -instance Infer ABool where infer = Bool -instance Infer ABigFloat where infer = BigFloat - --- | Get the type of something with at ype. -typeOf :: Infer t => p t -> X86 t -typeOf _ = infer - - --- | Mapping from X86 types to the Crucible types used to implement them. -type family Rep (x :: X86Type) :: CrucibleType where - Rep (Bits n) = LLVMPointerType n -- or just BVType? - Rep APtr = LLVMPointerType 64 - Rep ABool = BoolType - Rep ABigFloat = LLVMPointerType 80 -- or something eles? - --- | Specify a crucible type expclitily. -crucRepr :: X86 t -> TypeRepr (Rep t) -crucRepr x = - case x of - Bits n -> LLVMPointerRepr n - Ptr -> knownRepr - Bool -> knownRepr - BigFloat -> knownRepr - --- | Size of types in bits. -type family BitSize (x :: X86Type) :: Nat where - BitSize (Bits n) = n - BitSize APtr = 64 - BitSize ABool = 1 - BitSize ABigFloat = 80 - --- | A value level nubmer for the size of the type. -bitSize :: forall t. X86 t -> NatRepr (BitSize t) -bitSize x = - case x of - Bits n -> n - Ptr -> knownNat @(BitSize t) - Bool -> knownNat @(BitSize t) - BigFloat -> knownNat @(BitSize t) - - - --- | The Crucible backend used for speicifcations. -type Sym = SAWCoreBackend GlobalNonceGenerator (B.Flags B.FloatReal) - --- | A value in a X86 specification. -newtype Value t = Value (RegValue Sym (Rep t)) - --- | A helper for constructing values of a specific type. -value :: proxy t -> RegValue Sym (Rep t) -> Value t -value _ x = Value x - - diff --git a/src/SAWScript/X86SpecNew.hs b/src/SAWScript/X86SpecNew.hs index c5b1c95124..4d2776c91d 100644 --- a/src/SAWScript/X86SpecNew.hs +++ b/src/SAWScript/X86SpecNew.hs @@ -15,6 +15,8 @@ #endif module SAWScript.X86SpecNew ( Specification(..) + , SpecType, Pre, Post + , FunSpec(..) , verifyMode , overrideMode , State(..) @@ -42,6 +44,8 @@ module SAWScript.X86SpecNew , Overrides , debugPPReg + , Sym + -- * Cryptol , CryArg(..) , cryPre @@ -66,8 +70,11 @@ import Data.IORef(newIORef,atomicModifyIORef') import Data.String import Control.Monad.Reader +import qualified What4.Expr.Builder as B + import Data.Parameterized.NatRepr import Data.Parameterized.Classes +import Data.Parameterized.Nonce(GlobalNonceGenerator) import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF import Data.Parameterized.Pair @@ -106,7 +113,7 @@ import Lang.Crucible.CFG.Common import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Backend.SAWCore - (bindSAWTerm,sawBackendSharedContext,toSC) + (bindSAWTerm,sawBackendSharedContext,toSC,SAWCoreBackend) import Lang.Crucible.Types (TypeRepr(..),BaseTypeRepr(..),BaseToType,CrucibleType) @@ -123,6 +130,7 @@ import qualified Data.Macaw.Types as M import Verifier.SAW.CryptolEnv(CryptolEnv(..), lookupIn, getAllIfaceDecls) + import Cryptol.ModuleSystem.Name(Name) import Cryptol.ModuleSystem.Interface(ifTySyns) import Cryptol.TypeCheck.AST(TySyn(tsDef)) @@ -131,9 +139,6 @@ import Cryptol.Utils.PP(alwaysQualify,runDoc,pp) import Cryptol.Utils.Patterns(matchMaybe) -import SAWScript.X86Spec.Types(Sym) -import SAWScript.X86Spec.Monad(SpecType,Pre,Post) - data Specification = Specification { specAllocs :: ![Alloc] , specPres :: ![(String, Prop Pre)] @@ -150,6 +155,30 @@ data Specification = Specification data Unit = Bytes | Words | DWords | QWords | V128s | V256s deriving Show +{- | A specifiction for a function. +The outer, "Pre", computiation sets up the initial state of the +computation (i.e., the pre-condition for the function). +As a result, we return the inital register assignemtn, +and the post-condition for the function). -} +data FunSpec = + NewStyle (CryptolEnv -> IO Specification) + (State -> IO ()) + -- Debug: Run this to print some stuff at interesting times. + +-- | Is this a pre- or post-condition specificiation. +data {- kind -} SpecType = Pre | Post + +-- | We are specifying a pre-condition. +type Pre = 'Pre + +-- | We are specifying a post-condition. +type Post = 'Post + + + + +-- | The Crucible backend used for speicifcations. +type Sym = SAWCoreBackend GlobalNonceGenerator (B.Flags B.FloatReal) data Opts = Opts { optsSym :: Sym From c2be833312f1ce6a24654b798c15fc0a806feedd Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 21 Feb 2019 16:04:04 -0800 Subject: [PATCH 2/8] Check post condition while simulating (at the very end). --- src/SAWScript/X86.hs | 83 ++++++++++++++------------------------------ 1 file changed, 27 insertions(+), 56 deletions(-) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 805bec0017..c2b87ef4a5 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -21,6 +21,7 @@ module SAWScript.X86 import Control.Lens (toListOf, folded, (^.)) import Control.Exception(Exception(..),throwIO) import Control.Monad.ST(ST,stToIO,RealWorld) +import Control.Monad.IO.Class(liftIO) import qualified Data.AIG as AIG import Data.ByteString (ByteString) @@ -53,7 +54,7 @@ import Lang.Crucible.Simulator.RegMap(regValue, RegMap(..), RegEntry(..)) import Lang.Crucible.Simulator.RegValue(RegValue,RegValue'(..)) import Lang.Crucible.Simulator.GlobalState(lookupGlobal,insertGlobal,emptyGlobals) import Lang.Crucible.Simulator.Operations(defaultAbortHandler) -import Lang.Crucible.Simulator.OverrideSim(runOverrideSim, callCFG) +import Lang.Crucible.Simulator.OverrideSim(runOverrideSim, callCFG, readGlobal) import Lang.Crucible.Simulator.EvalStmt(executeCrucible) import Lang.Crucible.Simulator.ExecutionTree (GlobalPair,gpValue,ExecResult(..),PartialResult(..) @@ -398,9 +399,7 @@ translate opts elf fun = debug st return (gs,st,\st1 -> debug st1 >> po st1) - (addr, st1) <- doSim opts elf sfs name globs st - - checkPost st1 + addr <- doSim opts elf sfs name globs st checkPost gs <- getGoals sym ctx <- sawBackendSharedContext sym @@ -422,8 +421,9 @@ doSim :: ByteString -> (GlobalMap Sym 64, Overrides) -> State -> - IO (Integer,State) -doSim opts elf sfs name (globs,overs) st = + (State -> IO ()) -> + IO Integer +doSim opts elf sfs name (globs,overs) st checkPost = do say " Looking for address... " addr <- findSymbol (symMap elf) name let addrInt = @@ -441,7 +441,7 @@ doSim opts elf sfs name (globs,overs) st = let sym = backend opts mvar = memvar opts - setSimulatorVerbosity 4 sym + setSimulatorVerbosity 0 sym execResult <- statusBlock " Simulating... " $ do let crucRegTypes = crucArchRegTypes x86 @@ -460,56 +460,27 @@ doSim opts elf sfs name (globs,overs) st = , _profilingMetrics = Map.empty } let initGlobals = insertGlobal mvar (stateMem st) emptyGlobals - let initExecState = - InitialState ctx initGlobals defaultAbortHandler $ - runOverrideSim macawStructRepr $ do - let args :: RegMap Sym (MacawFunctionArgs X86_64) - args = RegMap (singleton (RegEntry macawStructRepr (stateRegs st))) - crucGenArchConstraints x86 $ - regValue <$> callCFG cfg args - executeCrucible [] initExecState - - gp <- case execResult of - FinishedResult _ res -> - case res of - TotalRes gp -> return gp - PartialRes _pre gp _ab -> return gp - -- XXX: we ignore the _pre, as it should be subsumed - -- by the assertions in the backend. Ask Rob D. for details. - AbortedResult _ctx res -> - malformed $ unlines [ "Failed to finish execution" - , ppAbort mvar res - ] - TimeoutResult _ctx -> - malformed $ unlines [ "Execution timed out" ] - - mem <- getMem gp mvar - return ( addrInt - , State { stateMem = mem, stateRegs = regValue (gp ^. gpValue) } - ) - -ppAbort :: GlobalVar Mem -> AbortedResult Sym b -> String -ppAbort mvar x = - case x of - AbortedExec e gp -> - case lookupGlobal mvar (gp ^. gpGlobals) of - Just mem -> unlines [ "Aborted execution: " ++ show e - , show (ppMem mem) ] - Nothing -> "Aborted exexution (no memory?)" - AbortedExit {} -> "Aborted exit" - AbortedBranch {} -> "Aborted branch" - - - --- | Get the current model of the memory. -getMem :: GlobalPair Sym a -> - GlobalVar Mem -> - IO (RegValue Sym Mem) -getMem st mvar = - case lookupGlobal mvar (st ^. gpGlobals) of - Just mem -> return mem - Nothing -> fail ("Global heap value not initialized: " ++ show mvar) + executeCrucible [] + $ InitialState ctx initGlobals defaultAbortHandler + $ runOverrideSim macawStructRepr + $ do let args :: RegMap Sym (MacawFunctionArgs X86_64) + args = RegMap (singleton (RegEntry macawStructRepr + (stateRegs st))) + crucGenArchConstraints x86 $ + do r <- callCFG cfg args + mem <- readGlobal mvar + let regs = regValue r + let sta = State { stateMem = mem, stateRegs = regs } + liftIO (checkPost sta) + pure regs + + case execResult of + FinishedResult {} -> pure () + AbortedResult {} -> sayLn "[Warning] Function never returns" + TimeoutResult {} -> malformed $ unlines [ "Execution timed out" ] + + return addrInt type TheCFG = SomeCFG (MacawExt X86_64) From bfe098c7518337b7c19ad79c17eeff831c4c9781 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 21 Feb 2019 16:42:32 -0800 Subject: [PATCH 3/8] Fix deprecated warnings and add some debug code --- src/SAWScript/X86.hs | 41 ++++++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index c2b87ef4a5..df85ccba0e 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -20,7 +20,7 @@ module SAWScript.X86 import Control.Lens (toListOf, folded, (^.)) import Control.Exception(Exception(..),throwIO) -import Control.Monad.ST(ST,stToIO,RealWorld) +import Control.Monad.ST(stToIO,RealWorld) import Control.Monad.IO.Class(liftIO) import qualified Data.AIG as AIG @@ -32,6 +32,8 @@ import qualified Data.Text as Text import Data.Text.Encoding(decodeUtf8) import System.IO(hFlush,stdout) +-- import Text.PrettyPrint.ANSI.Leijen(pretty) + import Data.ElfEdit (Elf, parseElf, ElfGetResult(..)) import Data.Parameterized.Some(Some(..)) @@ -51,14 +53,13 @@ import Lang.Crucible.Analysis.Postdom (postdomInfo) import Lang.Crucible.CFG.Core(SomeCFG(..), TypeRepr(..), cfgHandle) import Lang.Crucible.CFG.Common(freshGlobalVar,GlobalVar) import Lang.Crucible.Simulator.RegMap(regValue, RegMap(..), RegEntry(..)) -import Lang.Crucible.Simulator.RegValue(RegValue,RegValue'(..)) -import Lang.Crucible.Simulator.GlobalState(lookupGlobal,insertGlobal,emptyGlobals) +import Lang.Crucible.Simulator.RegValue(RegValue'(..)) +import Lang.Crucible.Simulator.GlobalState(insertGlobal,emptyGlobals) import Lang.Crucible.Simulator.Operations(defaultAbortHandler) import Lang.Crucible.Simulator.OverrideSim(runOverrideSim, callCFG, readGlobal) import Lang.Crucible.Simulator.EvalStmt(executeCrucible) import Lang.Crucible.Simulator.ExecutionTree - (GlobalPair,gpValue,ExecResult(..),PartialResult(..) - , gpGlobals, AbortedResult(..), SimContext(..), FnState(..) + (ExecResult(..), SimContext(..), FnState(..) , ExecState(InitialState) ) import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason) @@ -69,7 +70,7 @@ import Lang.Crucible.FunctionHandle(HandleAllocator,newHandleAllocator,insertHan -- Crucible LLVM import SAWScript.CrucibleLLVM - (Mem, ppMem, ppPtr, pattern LLVMPointer, bytesToInteger) + (Mem, ppPtr, pattern LLVMPointer, bytesToInteger) import Lang.Crucible.LLVM.Intrinsics(llvmIntrinsicTypes) import Lang.Crucible.LLVM.MemModel (mkMemVar) @@ -83,11 +84,10 @@ import Data.Macaw.Architecture.Info(ArchitectureInfo) import Data.Macaw.Discovery(analyzeFunction) import Data.Macaw.Discovery.State(FunctionExploreReason(UserRequest) , emptyDiscoveryState, AddrSymMap) -import Data.Macaw.Memory( Memory, MemSegmentOff(..) +import Data.Macaw.Memory( Memory, MemSegment(..), MemSegmentOff(..) , segmentBase, segmentOffset - , msegSegment, msegOffset - , addrOffset, memWordInteger - , relativeSegmentAddr, incAddr + , addrOffset, memWordToUnsigned + , segoffAddr, incAddr , readWord8, readWord16le, readWord32le, readWord64le) import Data.Macaw.Memory.ElfLoader( LoadOptions(..) , memoryForElfAllSymbols @@ -327,8 +327,8 @@ loadGlobal elf (nm,n,u) = Right a -> return (fromIntegral a) - loadLoc off = do let start = relativeSegmentAddr off - a = memWordInteger (addrOffset start) + loadLoc off = do let start = segoffAddr off + a = memWordToUnsigned (addrOffset start) is <- mapM readOne (addrsFor start) return (sname, a, u, is) @@ -426,16 +426,18 @@ doSim :: doSim opts elf sfs name (globs,overs) st checkPost = do say " Looking for address... " addr <- findSymbol (symMap elf) name + -- addr :: MemSegmentOff 64 let addrInt = - let seg = msegSegment addr + let seg :: MemSegment 64 + seg = segoffSegment addr in if segmentBase seg == 0 - then toInteger (segmentOffset seg + msegOffset addr) + then toInteger (segmentOffset seg + segoffOffset addr) else error " Not an absolute address" sayLn (show addr) SomeCFG cfg <- statusBlock " Constructing CFG... " - $ stToIO (makeCFG opts elf name addr) + $ makeCFG opts elf name addr -- writeFile "XXX.hs" (show cfg) @@ -494,12 +496,13 @@ makeCFG :: RelevantElf -> ByteString -> MemSegmentOff 64 -> - ST RealWorld TheCFG + IO TheCFG makeCFG opts elf name addr = - do (_,Some funInfo) <- analyzeFunction quiet addr UserRequest empty - baseVar <- freshGlobalVar (allocator opts) baseName knownRepr + do (_,Some funInfo) <- stToIO $ analyzeFunction quiet addr UserRequest empty + -- writeFile "MACAW.cfg" (show (pretty funInfo)) + baseVar <- stToIO $ freshGlobalVar (allocator opts) baseName knownRepr let memBaseVarMap = Map.singleton 1 baseVar - mkFunCFG x86 (allocator opts) memBaseVarMap cruxName posFn funInfo + stToIO $ mkFunCFG x86 (allocator opts) memBaseVarMap cruxName posFn funInfo where txtName = decodeUtf8 name cruxName = functionNameFromText txtName From 3cb110c15f3fd5673fd0f9595118c4f0787a4b5a Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 21 Feb 2019 16:45:38 -0800 Subject: [PATCH 4/8] Rename X86SpecNew to X86Spec --- saw-script.cabal | 2 +- src/SAWScript/X86.hs | 2 +- src/SAWScript/{X86SpecNew.hs => X86Spec.hs} | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) rename src/SAWScript/{X86SpecNew.hs => X86Spec.hs} (99%) diff --git a/saw-script.cabal b/saw-script.cabal index e1af021d3a..710c104ef3 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -154,7 +154,7 @@ library SAWScript.Prover.Exporter SAWScript.X86 - SAWScript.X86SpecNew + SAWScript.X86Spec GHC-options: -O2 -Wall -fno-ignore-asserts -fno-spec-constr-count if impl(ghc == 8.0.1) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index df85ccba0e..2fddcb1698 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -122,7 +122,7 @@ import Verifier.SAW.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule) import Verifier.SAW.Cryptol.Prelude(scLoadPreludeModule,scLoadCryptolModule) -- SAWScript -import SAWScript.X86SpecNew +import SAWScript.X86Spec import SAWScript.Proof(predicateToProp, Quantification(Universal)) diff --git a/src/SAWScript/X86SpecNew.hs b/src/SAWScript/X86Spec.hs similarity index 99% rename from src/SAWScript/X86SpecNew.hs rename to src/SAWScript/X86Spec.hs index 4d2776c91d..c46e31156d 100644 --- a/src/SAWScript/X86SpecNew.hs +++ b/src/SAWScript/X86Spec.hs @@ -13,7 +13,7 @@ #if __GLASGOW_HASKELL__ >= 806 {-# Language NoStarIsType #-} #endif -module SAWScript.X86SpecNew +module SAWScript.X86Spec ( Specification(..) , SpecType, Pre, Post , FunSpec(..) From 23f76f96a5d816871631f7903bd8d112578dd512 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 22 Feb 2019 09:24:12 -0800 Subject: [PATCH 5/8] Depend on latest `macaw` --- deps/macaw | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/macaw b/deps/macaw index 636693e522..731d68df40 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 636693e522ac84894288076dffb0f51b7c1bb1f9 +Subproject commit 731d68df40fe1f9c1e384f5a1746de8650a891ae From 79cf3f16d1df7757d13678e5120986ea7b502e9f Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 22 Feb 2019 13:23:42 -0800 Subject: [PATCH 6/8] Use two separate symbol maps: one with functions, one with all things. --- src/SAWScript/X86.hs | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 2fddcb1698..b8cfb062c0 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -91,6 +91,7 @@ import Data.Macaw.Memory( Memory, MemSegment(..), MemSegmentOff(..) , readWord8, readWord16le, readWord32le, readWord64le) import Data.Macaw.Memory.ElfLoader( LoadOptions(..) , memoryForElfAllSymbols + , memoryForElf , MemSymbol(..) ) import Data.Macaw.Symbolic( ArchRegStruct @@ -240,8 +241,9 @@ registerSymFuns opts = -- | These are the parts of the ELF file that we care about. data RelevantElf = RelevantElf - { memory :: Memory 64 - , symMap :: AddrSymMap 64 + { memory :: Memory 64 + , funSymMap :: AddrSymMap 64 + , symMap :: AddrSymMap 64 } -- | Parse an elf file. @@ -259,17 +261,13 @@ getElf path = -- | Extract a Macaw "memory" from an ELF file and resolve symbols. getRelevant :: Elf 64 -> IO RelevantElf getRelevant elf = - case memoryForElfAllSymbols opts elf of - Left err -> malformed err - Right (mem, addrs, _warnings, _errs) -> - do -{- - unless (null errs) - $ malformed $ unlines $ "Failed to resolve ELF symbols:" - : map show errs --} - let toEntry msym = (memSymbolStart msym, memSymbolName msym) + case (memoryForElf opts elf, memoryForElfAllSymbols opts elf) of + (Left err, _) -> malformed err + (_, Left err) -> malformed err + (Right (mem, faddrs, _warnings, _errs), Right (_, addrs, _, _)) -> + do let toEntry msym = (memSymbolStart msym, memSymbolName msym) return RelevantElf { memory = mem + , funSymMap = Map.fromList (map toEntry faddrs) , symMap = Map.fromList (map toEntry addrs) } @@ -508,7 +506,7 @@ makeCFG opts elf name addr = cruxName = functionNameFromText txtName baseName = Text.append "mem_base_" txtName - empty = emptyDiscoveryState (memory elf) (symMap elf) (archInfo opts) + empty = emptyDiscoveryState (memory elf) (funSymMap elf) (archInfo opts) From 9702e4649ff3eacfd6d68dcc626761ca34556372 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 22 Feb 2019 14:34:21 -0800 Subject: [PATCH 7/8] Clean-up goals and some debug printing. --- src/SAWScript/X86.hs | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index b8cfb062c0..879a01d08e 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -31,6 +31,7 @@ import qualified Data.Map as Map import qualified Data.Text as Text import Data.Text.Encoding(decodeUtf8) import System.IO(hFlush,stdout) +import Data.Maybe(mapMaybe) -- import Text.PrettyPrint.ANSI.Leijen(pretty) @@ -117,6 +118,7 @@ import Data.Macaw.X86.Crucible(SymFuns(..)) -- Saw Core import Verifier.SAW.SharedTerm(Term, mkSharedContext, SharedContext, scImplies) import Verifier.SAW.Term.Pretty(showTerm) +import Verifier.SAW.Recognizer(asBool) -- Cryptol Verifier import Verifier.SAW.CryptolEnv(CryptolEnv,initCryptolEnv,loadCryptolModule) @@ -522,8 +524,22 @@ data Goal = Goal -- | The boolean term that needs proving (i.e., assumptions imply conclusion) gGoal :: SharedContext -> Goal -> IO Term -gGoal sc g = predicateToProp sc Universal [] =<< go (gAssumes g) +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 From 16915f7a1e639b5c6ed22c5debe164244fa3e003 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 28 Feb 2019 10:11:45 -0800 Subject: [PATCH 8/8] Bump dependencies to latest versions. --- deps/crucible | 2 +- deps/macaw | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps/crucible b/deps/crucible index 874f1a9aa9..d0c8f1e1a7 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 874f1a9aa9c38b6731cbbb1ccbfe09a58f0c3eeb +Subproject commit d0c8f1e1a712e779f9995363689b352ce10b17dd diff --git a/deps/macaw b/deps/macaw index 731d68df40..65ca5447ea 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 731d68df40fe1f9c1e384f5a1746de8650a891ae +Subproject commit 65ca5447ea83ae66d85c8df0710b1d8ec905ef1d