diff --git a/.travis.yml b/.travis.yml index 6fda79c1..06b368ac 100644 --- a/.travis.yml +++ b/.travis.yml @@ -29,6 +29,8 @@ install: # Here starts the actual work to be performed for the package under test; # any command which exits with a non-zero exit code causes the build to fail. script: + # Build crucible with no -Werror + - stack build crucible # Build packages - stack build --ghc-options="-Wall -Werror" # Run tests diff --git a/base/macaw-base.cabal b/base/macaw-base.cabal index 9f1d590a..f570be16 100644 --- a/base/macaw-base.cabal +++ b/base/macaw-base.cabal @@ -1,5 +1,5 @@ name: macaw-base -version: 0.3.4 +version: 0.3.5 author: Galois, Inc. maintainer: jhendrix@galois.com build-type: Simple diff --git a/base/src/Data/Macaw/AbsDomain/AbsState.hs b/base/src/Data/Macaw/AbsDomain/AbsState.hs index d384716b..12aee0f2 100644 --- a/base/src/Data/Macaw/AbsDomain/AbsState.hs +++ b/base/src/Data/Macaw/AbsDomain/AbsState.hs @@ -50,6 +50,7 @@ module Data.Macaw.AbsDomain.AbsState , stridedInterval , finalAbsBlockState , addMemWrite + , addCondMemWrite , transferValue , abstractULt , abstractULeq @@ -1240,38 +1241,71 @@ addMemWrite :: ( RegisterInfo (ArchReg arch) -- ^ Current processor state. -> AbsProcessorState (ArchReg arch) ids addMemWrite a memRepr v r = - case (transferValue r a, transferValue r v) of + addCondMemWrite (\new _ -> new) a memRepr (transferValue r v) r + +-- | Update the processor state with a potential memory write. +addCondMemWrite :: ( RegisterInfo r + , MemWidth (RegAddrWidth r) + , HasCallStack + , r ~ ArchReg arch + ) + => (AbsValue (RegAddrWidth r) tp + -> AbsValue (RegAddrWidth r) tp + -> AbsValue (RegAddrWidth r) tp) + -- ^ Updaete function that takes new value, old value and returns value to insert. + -> Value arch ids (BVType (RegAddrWidth r)) + -- ^ Address that we are writing to. + -> MemRepr tp + -- ^ Information about how value should be represented in memory. + -> AbsValue (RegAddrWidth r) tp + -- ^ Value to write to memory + -> AbsProcessorState r ids + -- ^ Current processor state. + -> AbsProcessorState r ids +addCondMemWrite f a memRepr v_abs r = + case transferValue r a of -- (_,TopV) -> r -- We overwrite _some_ stack location. An alternative would be to -- update everything with v. - (SomeStackOffset _, _) -> do + SomeStackOffset _ -> do let cur_ip = r^.absInitialRegs^.curIP debug DAbsInt ("addMemWrite: dropping stack at " ++ show (pretty cur_ip) ++ " via " ++ show (pretty a) ++" in SomeStackOffset case") $ r & curAbsStack %~ pruneStack - (StackOffset _ s, v_abs) -> + StackOffset _ s -> let w = fromInteger (memReprBytes memRepr) - e = StackEntry memRepr v_abs stk0 = r^.curAbsStack -- Delete information about old assignment stk1 = Set.fold (\o m -> deleteRange o (o+w) m) stk0 s -- Add information about new assignment stk2 = case Set.toList s of - [o] | v_abs /= TopV -> Map.insert o e stk1 + [o] | -- Skip if new value is top + v_abs /= TopV + -- Lookup existing value at tack + , oldAbs <- + case Map.lookup o stk0 of + Just (StackEntry oldMemRepr old) + | Just Refl <- testEquality memRepr oldMemRepr -> old + _ -> top + -- Computed merged value + , mergedValue <- f v_abs oldAbs + -- Insert only non-top values + , mergedValue /= TopV -> + Map.insert o (StackEntry memRepr mergedValue) stk1 _ -> stk1 in r & curAbsStack .~ stk2 -- FIXME: nuke stack on an unknown address or Top? _ -> r +-- | Returns true if return address is known to sit on stack. absStackHasReturnAddr :: AbsBlockState r -> Bool absStackHasReturnAddr s = isJust $ find isReturnAddr (Map.elems (s^.startAbsStack)) where isReturnAddr (StackEntry _ ReturnAddr) = True isReturnAddr _ = False - -- | Return state for after value has run. finalAbsBlockState :: forall a ids . ( RegisterInfo (ArchReg a) diff --git a/base/src/Data/Macaw/Analysis/FunctionArgs.hs b/base/src/Data/Macaw/Analysis/FunctionArgs.hs index ddaddf17..d50ed208 100644 --- a/base/src/Data/Macaw/Analysis/FunctionArgs.hs +++ b/base/src/Data/Macaw/Analysis/FunctionArgs.hs @@ -520,6 +520,7 @@ stmtDemandedValues ctx stmt = demandConstraints ctx $ | otherwise -> [] WriteMem addr _ v -> [Some addr, Some v] + CondWriteMem cond addr _ v -> [Some cond, Some addr, Some v] InstructionStart _ _ -> [] -- Comment statements have no specific value. Comment _ -> [] diff --git a/base/src/Data/Macaw/CFG/Block.hs b/base/src/Data/Macaw/CFG/Block.hs index 105d4d55..7c3c11d4 100644 --- a/base/src/Data/Macaw/CFG/Block.hs +++ b/base/src/Data/Macaw/CFG/Block.hs @@ -44,8 +44,6 @@ data TermStmt arch ids -- -- The registers include the state of registers just before the terminal statement -- executes. - -- The address returns the address within the current function that this terminal - -- statement could return to (if any) | ArchTermStmt !(ArchTermStmt arch ids) !(RegState (ArchReg arch) (Value arch ids)) diff --git a/base/src/Data/Macaw/CFG/Core.hs b/base/src/Data/Macaw/CFG/Core.hs index 2682ce31..a85cc20b 100644 --- a/base/src/Data/Macaw/CFG/Core.hs +++ b/base/src/Data/Macaw/CFG/Core.hs @@ -1,7 +1,4 @@ {-| -Copyright : (c) Galois, Inc 2015-2017 -Maintainer : Joe Hendrix - Defines data types needed to represent values, assignments, and statements from Machine code. This is a low-level CFG representation where the entire program is a @@ -23,7 +20,6 @@ single CFG. {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} - module Data.Macaw.CFG.Core ( -- * Stmt level declarations Stmt(..) @@ -55,6 +51,7 @@ module Data.Macaw.CFG.Core , mkRegStateM , mapRegsWith , traverseRegsWith + , traverseRegsWith_ , zipWithRegState , ppRegMap -- * Pretty printing @@ -416,6 +413,13 @@ traverseRegsWith :: Applicative m -> m (RegState r g) traverseRegsWith f (RegState m) = RegState <$> MapF.traverseWithKey f m +-- | Traverse the register state with the name of each register and value. +traverseRegsWith_ :: Applicative m + => (forall tp. r tp -> f tp -> m ()) + -> RegState r f + -> m () +traverseRegsWith_ f (RegState m) = MapF.traverseWithKey_ f m + -- | Traverse the register state with the name of each register and value. mapRegsWith :: Applicative m => (forall tp. r tp -> f tp -> g tp) @@ -713,21 +717,30 @@ instance ( RegisterInfo r data Stmt arch ids = forall tp . AssignStmt !(Assignment arch ids tp) | forall tp . WriteMem !(ArchAddrValue arch ids) !(MemRepr tp) !(Value arch ids tp) - -- ^ This denotes a write to memory, and consists of an address to write to, a `MemRepr` defining - -- how the value should be stored in memory, and the value to be written. + -- ^ This denotes a write to memory, and consists of an address + -- to write to, a `MemRepr` defining how the value should be + -- stored in memory, and the value to be written. + | forall tp . + CondWriteMem !(Value arch ids BoolType) + !(ArchAddrValue arch ids) + !(MemRepr tp) + !(Value arch ids tp) + -- ^ This denotes a write to memory that only executes if the + -- condition is true. | InstructionStart !(ArchAddrWord arch) !Text -- ^ The start of an instruction -- - -- The information includes the offset relative to the start of the block and the - -- disassembler output if available (or empty string if unavailable) + -- The information includes the offset relative to the start of + -- the block and the disassembler output if available (or empty + -- string if unavailable) | Comment !Text -- ^ A user-level comment | ExecArchStmt !(ArchStmt arch (Value arch ids)) -- ^ Execute an architecture specific statement | ArchState !(ArchMemAddr arch) !(MapF.MapF (ArchReg arch) (Value arch ids)) - -- ^ Address of an instruction and the *machine* registers that it updates - -- (with their associated macaw values after the execution of the - -- instruction). + -- ^ Address of an instruction and the *machine* registers that + -- it updates (with their associated macaw values after the + -- execution of the instruction). ppStmt :: ArchConstraints arch => (ArchAddrWord arch -> Doc) @@ -737,7 +750,10 @@ ppStmt :: ArchConstraints arch ppStmt ppOff stmt = case stmt of AssignStmt a -> pretty a - WriteMem a _ rhs -> text "write_mem" <+> prettyPrec 11 a <+> ppValue 0 rhs + WriteMem a _ rhs -> + text "write_mem" <+> prettyPrec 11 a <+> ppValue 0 rhs + CondWriteMem c a _ rhs -> + text "cond_write_mem" <+> prettyPrec 11 c <+> prettyPrec 11 a <+> ppValue 0 rhs InstructionStart off mnem -> text "#" <+> ppOff off <+> text (Text.unpack mnem) Comment s -> text $ "# " ++ Text.unpack s ExecArchStmt s -> ppArchStmt (ppValue 10) s diff --git a/base/src/Data/Macaw/CFG/DemandSet.hs b/base/src/Data/Macaw/CFG/DemandSet.hs index b0f22c07..998d6b46 100644 --- a/base/src/Data/Macaw/CFG/DemandSet.hs +++ b/base/src/Data/Macaw/CFG/DemandSet.hs @@ -110,6 +110,10 @@ addStmtDemands s = WriteMem addr _repr val -> do addValueDemands addr addValueDemands val + CondWriteMem cond addr _repr val -> do + addValueDemands cond + addValueDemands addr + addValueDemands val InstructionStart{} -> pure () Comment _ -> @@ -129,6 +133,7 @@ stmtNeeded :: AssignIdSet ids -> Stmt arch ids -> Bool stmtNeeded demandSet stmt = case stmt of AssignStmt a -> Set.member (Some (assignId a)) demandSet + CondWriteMem{} -> True WriteMem{} -> True InstructionStart{} -> True Comment{} -> True diff --git a/base/src/Data/Macaw/CFG/Rewriter.hs b/base/src/Data/Macaw/CFG/Rewriter.hs index 1bd163ea..5d7743f0 100644 --- a/base/src/Data/Macaw/CFG/Rewriter.hs +++ b/base/src/Data/Macaw/CFG/Rewriter.hs @@ -716,6 +716,11 @@ rewriteStmt s = tgtAddr <- rewriteValue addr tgtVal <- rewriteValue val appendRewrittenStmt $ WriteMem tgtAddr repr tgtVal + CondWriteMem cond addr repr val -> do + tgtCond <- rewriteValue cond + tgtAddr <- rewriteValue addr + tgtVal <- rewriteValue val + appendRewrittenStmt $ CondWriteMem tgtCond tgtAddr repr tgtVal Comment cmt -> appendRewrittenStmt $ Comment cmt InstructionStart off mnem -> diff --git a/base/src/Data/Macaw/Discovery/AbsEval.hs b/base/src/Data/Macaw/Discovery/AbsEval.hs index e1a29c0d..00eb4cf4 100644 --- a/base/src/Data/Macaw/Discovery/AbsEval.hs +++ b/base/src/Data/Macaw/Discovery/AbsEval.hs @@ -76,8 +76,10 @@ absEvalStmt info stmt = withArchConstraints info $ case stmt of AssignStmt a -> modify $ addAssignment info a - WriteMem addr memRepr v -> - modify $ addMemWrite addr memRepr v + WriteMem addr memRepr v -> do + modify $ \s -> addMemWrite addr memRepr v s + CondWriteMem _cond addr memRepr v -> + modify $ \s -> addCondMemWrite lub addr memRepr (transferValue s v) s InstructionStart _ _ -> pure () Comment{} -> diff --git a/deps/crucible b/deps/crucible index 75343267..4908e206 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 75343267ccacfa9fdb71c82efdce12908ba5ca33 +Subproject commit 4908e20654a753f7f5799a062070ecd6fba44359 diff --git a/deps/parameterized-utils b/deps/parameterized-utils index 05fa5d2a..e4fc7f5a 160000 --- a/deps/parameterized-utils +++ b/deps/parameterized-utils @@ -1 +1 @@ -Subproject commit 05fa5d2a58dfd531ffab97b913ea108d910349d6 +Subproject commit e4fc7f5a7d58ce28b8b59c0d27358058fe096751 diff --git a/submodules/dismantle b/submodules/dismantle index 8be3748b..13979c7b 160000 --- a/submodules/dismantle +++ b/submodules/dismantle @@ -1 +1 @@ -Subproject commit 8be3748b74daa44b11195203569ba91a3ac6b4fd +Subproject commit 13979c7b863b0afc5cebdeaf7f3d94a929d07524 diff --git a/submodules/semmc b/submodules/semmc index 1cb5a6d1..6b045557 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 1cb5a6d182fcadbac2296893b713f3fedaaa408c +Subproject commit 6b045557e3714d5c4037015b9ec1cf88558f239e diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 7e60a20a..440a247d 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -843,6 +843,12 @@ execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar globs (MO.LookupFunc ptr <- tryGlobPtr sym mem globs (C.regValue ptr0) mem1 <- doWriteMem sym mem addrWidth memRep ptr (C.regValue v) pure ((), setMem st mvar mem1) + MacawCondWriteMem addrWidth memRep cond ptr0 v -> do + let sym = st^.C.stateSymInterface + mem <- getMem st mvar + ptr <- tryGlobPtr sym mem globs (C.regValue ptr0) + mem1 <- doCondWriteMem sym mem addrWidth memRep (C.regValue cond) ptr (C.regValue v) + pure ((), setMem st mvar mem1) MacawGlobalPtr w addr -> M.addrWidthClass w $ doGetGlobal st mvar globs addr diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs index 5a2fc0d0..8db056bb 100644 --- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs +++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs @@ -359,6 +359,16 @@ data MacawStmtExtension (arch :: K.Type) -> !(f (ToCrucibleType tp)) -> MacawStmtExtension arch f C.UnitType + -- | Write to memory id xonsiriob is true + MacawCondWriteMem + :: !(ArchAddrWidthRepr arch) + -> !(M.MemRepr tp) + -- Condition + -> !(f C.BoolType) + -> !(f (ArchAddrCrucibleType arch)) + -> !(f (ToCrucibleType tp)) + -> MacawStmtExtension arch f C.UnitType + -- | Convert a literal address (from Macaw) into a pointer in the LLVM memory model MacawGlobalPtr :: !(ArchAddrWidthRepr arch) @@ -489,9 +499,10 @@ instance (C.PrettyApp (MacawArchStmtExtension arch), -> (forall (x :: C.CrucibleType) . MacawStmtExtension arch f x -> Doc) ppApp f a0 = case a0 of - MacawReadMem _ r a -> sexpr "macawReadMem" [pretty r, f a] - MacawCondReadMem _ r c a d -> sexpr "macawCondReadMem" [pretty r, f c, f a, f d ] - MacawWriteMem _ r a v -> sexpr "macawWriteMem" [pretty r, f a, f v] + MacawReadMem _ r a -> sexpr "macawReadMem" [pretty r, f a] + MacawCondReadMem _ r c a d -> sexpr "macawCondReadMem" [pretty r, f c, f a, f d ] + MacawWriteMem _ r a v -> sexpr "macawWriteMem" [pretty r, f a, f v] + MacawCondWriteMem _ r c a v -> sexpr "macawCondWriteMem" [f c, pretty r, f a, f v] MacawGlobalPtr _ x -> sexpr "global" [ text (show x) ] MacawFreshSymbolic r -> sexpr "macawFreshSymbolic" [ text (show r) ] @@ -519,6 +530,7 @@ instance C.TypeApp (MacawArchStmtExtension arch) appType (MacawReadMem _ r _) = memReprToCrucible r appType (MacawCondReadMem _ r _ _ _) = memReprToCrucible r appType (MacawWriteMem _ _ _ _) = C.knownRepr + appType MacawCondWriteMem{} = C.knownRepr appType (MacawGlobalPtr w _) | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w) appType (MacawFreshSymbolic r) = typeToCrucible r @@ -1178,6 +1190,12 @@ addMacawStmt baddr stmt = cval <- valueToCrucible val w <- archAddrWidth void $ evalMacawStmt (MacawWriteMem w repr caddr cval) + M.CondWriteMem cond addr repr val -> do + ccond <- valueToCrucible cond + caddr <- valueToCrucible addr + cval <- valueToCrucible val + w <- archAddrWidth + void $ evalMacawStmt (MacawCondWriteMem w repr ccond caddr cval) M.InstructionStart off t -> do -- Update the position modify' $ \s -> s { codeOff = off diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs index f34d068c..5a1c7354 100644 --- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs +++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs @@ -23,6 +23,7 @@ module Data.Macaw.Symbolic.MemOps , doReadMem , doCondReadMem , doWriteMem + , doCondWriteMem , doGetGlobal , doLookupFunctionHandle , doPtrToBits @@ -805,3 +806,35 @@ doWriteMem sym mem ptrWidth memRep ptr val = hasPtrClass ptrWidth $ let alignment = noAlignment -- default to byte alignment (FIXME) let memVal = resolveMemVal memRep ty val Mem.storeRaw sym mem ptr ty alignment memVal + + +-- | Write a Macaw value to memory if a condition holds. +-- +-- arg1 : Symbolic Interface +-- arg2 : Heap prior to write +-- arg3 : Width of ptr +-- arg4 : What/how we are writing +-- arg5 : Condition that must hold if we write. +-- arg6 : Address to write to +-- arg7 : Value to write +doCondWriteMem :: + IsSymInterface sym => + sym -> + MemImpl sym -> + M.AddrWidthRepr ptrW -> + MemRepr ty -> + Pred sym -> + LLVMPtr sym ptrW -> + RegValue sym (ToCrucibleType ty) -> + IO (MemImpl sym) +doCondWriteMem sym mem ptrWidth memRep cond ptr val = hasPtrClass ptrWidth $ + do ok <- isValidPtr sym mem ptrWidth ptr + condOk <- impliesPred sym cond ok + check sym condOk "doWriteMem" $ + "Write to an invalid location: " ++ show (Mem.ppPtr ptr) + ty <- case memReprToStorageType (getEnd mem) memRep of + Left msg -> throwIO $ userError msg + Right tp -> pure tp + let alignment = noAlignment -- default to byte alignment (FIXME) + let memVal = resolveMemVal memRep ty val + Mem.condStoreRaw sym mem cond ptr ty alignment memVal diff --git a/x86/src/Data/Macaw/X86.hs b/x86/src/Data/Macaw/X86.hs index 5b135c82..cf406d86 100644 --- a/x86/src/Data/Macaw/X86.hs +++ b/x86/src/Data/Macaw/X86.hs @@ -580,6 +580,8 @@ x86DemandContext = , archFnHasSideEffects = x86PrimFnHasSideEffects } +-- | Get the next IP that may run after this terminal and the abstract +-- state denoting possible starting conditions when that code runs. postX86TermStmtAbsState :: (forall tp . X86Reg tp -> Bool) -> Memory 64 -> AbsBlockState X86Reg