Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Print concrete override precondition failures #416

Merged
merged 15 commits into from
May 14, 2019
Merged

Print concrete override precondition failures #416

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
4fecf3d
[WIP] use labeled predicates
langston-barrett Apr 19, 2019
cb3cf32
Print concretely failing override preconditions
langston-barrett Apr 22, 2019
dec81cd
Prettier printing of override matching failure
langston-barrett Apr 22, 2019
66af2c2
More specific error messages for preconditions involving globals
langston-barrett Apr 22, 2019
f123d08
Update Crucible submodule (for What4.LabeledPred)
langston-barrett Apr 22, 2019
4395c17
Update Crucible submodule: Pretty instance for LLVMVal
langston-barrett Apr 22, 2019
ec8220c
Show both expected and actual values on equality preconditions
langston-barrett Apr 22, 2019
12a1190
Add some newlines (the actual value may be a large, complex struct)
langston-barrett Apr 22, 2019
66c9fbc
Show symbolically failing override preconditions when possible
langston-barrett Apr 22, 2019
97ce94c
Add a message when no preconditions symbolically _or_ concretely fail
langston-barrett Apr 22, 2019
40b63dc
Merge remote-tracking branch 'upstream/master' into override-matching
langston-barrett May 14, 2019
f0ec300
fix merge conflict
langston-barrett May 14, 2019
a09ad89
Don't print symbolic override matching failures
langston-barrett May 14, 2019
fe054b4
fix logging bug: null -> not null
langston-barrett May 14, 2019
e7c8b89
Allow the user to see all overrides with --sim-verbose=3
langston-barrett May 14, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/SAWScript/CrucibleBuiltins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@ import Data.Parameterized.Some

import qualified What4.Config as W4
import qualified What4.FunctionName as W4
import qualified What4.LabeledPred as W4
import qualified What4.ProgramLoc as W4
import qualified What4.Interface as W4
import qualified What4.Expr.Builder as W4
Expand Down Expand Up @@ -832,7 +833,7 @@ verifyPoststate opts sc cc mspec env0 globals ret =
st <- case matchPost of
Left err -> fail (show err)
Right (_, st) -> return st
io $ for_ (view osAsserts st) $ \(p, r) ->
io $ for_ (view osAsserts st) $ \(W4.LabeledPred p r) ->
Crucible.addAssertion sym (Crucible.LabeledPred p r)

obligations <- io $ Crucible.getProofObligations sym
Expand Down
35 changes: 24 additions & 11 deletions src/SAWScript/CrucibleMethodSpecIR.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE DeriveFunctor #-}
{- |
Module : SAWScript.CrucibleMethodSpecIR
Description : Provides type-checked representation for Crucible/LLVM function
Expand Down Expand Up @@ -31,17 +32,17 @@ import qualified Data.Map as Map
import Control.Monad.Trans.Maybe
import Control.Monad.Trans (lift)
import Control.Lens
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))

import qualified Text.LLVM.AST as L
import qualified Text.LLVM.PP as L
import Data.IORef
import Data.Monoid ((<>))
import qualified Text.LLVM.AST as L
import qualified Text.LLVM.PP as L

import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.Nonce as Crucible

import SAWScript.Prover.SolverStats
import SAWScript.Prover.SolverStats

import qualified What4.Expr.Builder as B
import What4.ProgramLoc (ProgramLoc)
Expand All @@ -58,12 +59,13 @@ import qualified Lang.Crucible.Simulator.GlobalState as Crucible (SymGlobalState
--import qualified Lang.Crucible.LLVM.Translation as CL
import qualified Lang.Crucible.Simulator.Intrinsics as Crucible
(IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn))
import qualified What4.ProgramLoc as W4 (plSourceLoc)

import qualified SAWScript.CrucibleLLVM as CL

import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedTerm
import SAWScript.Options
import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedTerm
import SAWScript.Options

newtype AllocIndex = AllocIndex Int
deriving (Eq, Ord, Show)
Expand Down Expand Up @@ -181,14 +183,26 @@ data CrucibleMethodSpecIR' t =
, _csSolverStats :: SolverStats -- ^ statistics about the proof that produced this
, _csLoc :: ProgramLoc
}
deriving (Show)

type CrucibleMethodSpecIR = CrucibleMethodSpecIR' CL.MemType
deriving (Functor, Show)

type GhostValue = "GhostValue"
type GhostType = Crucible.IntrinsicType GhostValue Crucible.EmptyCtx
type GhostGlobal = Crucible.GlobalVar GhostType

makeLenses ''CrucibleMethodSpecIR'

type CrucibleMethodSpecIR = CrucibleMethodSpecIR' CL.MemType

ppMethodSpec :: CrucibleMethodSpecIR -> PP.Doc
ppMethodSpec methodSpec =
PP.text "Name: " <> PP.text (methodSpec ^. csName)
PP.<$$> PP.text "Location: " <> PP.pretty (W4.plSourceLoc (methodSpec ^. csLoc))
PP.<$$> PP.text "Argument types: "
PP.<$$> PP.indent 2 (PP.vcat (map (PP.text . show) (methodSpec ^. csArgs)))
PP.<$$> PP.text "Return type: " <> case methodSpec ^. csRet of
Nothing -> PP.text "<void>"
Just ret -> PP.text (show ret)

instance Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) GhostValue where
type Intrinsic (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) GhostValue ctx = TypedTerm
muxIntrinsic sym _ _namerep _ctx prd thn els =
Expand All @@ -199,7 +213,6 @@ instance Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.Fl
res <- scIte sc typ prd' (ttTerm thn) (ttTerm els)
return thn { ttTerm = res }

makeLenses ''CrucibleMethodSpecIR'
makeLenses ''StateSpec'

csAllocations :: CrucibleMethodSpecIR -> Map AllocIndex (ProgramLoc, CL.MemType)
Expand Down
Loading