Skip to content

Commit

Permalink
Merge branch 'master' into term-model-fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@robdockins
robdockins authored Jul 22, 2021
2 parents 047e7b7 + d2b99ca commit fa9cc39
Show file tree
Hide file tree
Showing 25 changed files with 577 additions and 212 deletions.
2 changes: 1 addition & 1 deletion deps/crucible
Submodule crucible updated 73 files
+1 −1 .github/ci.sh
+6 −7 .github/workflows/crux-llvm-build.yml
+6 −5 crucible-concurrency/crucibles/Main.hs
+7 −4 crucible-concurrency/src/Cruces/CrucesMain.hs
+10 −6 crucible-concurrency/src/Cruces/ExploreCrux.hs
+6 −10 crucible-concurrency/src/Crucibles/Explore.hs
+0 −6 crucible-concurrency/src/Crucibles/ExploreTypes.hs
+1 −2 crucible-go/src/Lang/Crucible/Go/Overrides.hs
+8 −3 crucible-go/tool/Main.hs
+8 −5 crucible-jvm/tool/Main.hs
+70 −1 crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs
+5 −5 crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+1 −1 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+46 −3 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+0 −1 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs
+1 −2 crucible-llvm/test/TestMemory.hs
+4 −5 crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+3 −5 crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
+3 −3 crucible-syntax/test-data/simulator-tests/override-test2.out.good
+8 −8 crucible-syntax/test-data/simulator-tests/seq-test3.out.good
+11 −9 crucible-wasm/tool/Main.hs
+1 −0 crucible/crucible.cabal
+275 −81 crucible/src/Lang/Crucible/Backend.hs
+30 −111 crucible/src/Lang/Crucible/Backend/AssumptionStack.hs
+41 −38 crucible/src/Lang/Crucible/Backend/Online.hs
+32 −34 crucible/src/Lang/Crucible/Backend/ProofGoals.hs
+10 −8 crucible/src/Lang/Crucible/Backend/Simple.hs
+1 −1 crucible/src/Lang/Crucible/Simulator/BoundedExec.hs
+1 −1 crucible/src/Lang/Crucible/Simulator/BoundedRecursion.hs
+2 −1 crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
+2 −3 crucible/src/Lang/Crucible/Simulator/ExecutionTree.hs
+6 −30 crucible/src/Lang/Crucible/Simulator/Operations.hs
+5 −4 crucible/src/Lang/Crucible/Simulator/PathSatisfiability.hs
+2 −2 crucible/src/Lang/Crucible/Simulator/PathSplitting.hs
+50 −0 crucible/src/Lang/Crucible/Simulator/PositionTracking.hs
+2 −0 crux-llvm/crux-llvm.cabal
+66 −36 crux-llvm/src/Crux/LLVM/Compile.hs
+61 −0 crux-llvm/src/Crux/LLVM/Log.hs
+20 −23 crux-llvm/src/Crux/LLVM/Overrides.hs
+18 −16 crux-llvm/src/Crux/LLVM/Simulate.hs
+28 −7 crux-llvm/src/CruxLLVMMain.hs
+63 −65 crux-llvm/svcomp/Main.hs
+123 −0 crux-llvm/svcomp/SVComp/Log.hs
+22 −0 crux-llvm/test-data/golden/cex-test.c
+3 −0 crux-llvm/test-data/golden/cex-test.config
+9 −0 crux-llvm/test-data/golden/cex-test.good
+1 −1 crux-llvm/test/Test.hs
+2 −0 crux-mir/crux-mir.cabal
+1 −10 crux-mir/src/Mir/Intrinsics.hs
+75 −44 crux-mir/src/Mir/Language.hs
+39 −0 crux-mir/src/Mir/Log.hs
+13 −12 crux-mir/src/Mir/Overrides.hs
+6 −4 crux-mir/test/Test.hs
+2 −1 crux/crux.cabal
+79 −78 crux/src/Crux.hs
+29 −7 crux/src/Crux/Config/Common.hs
+48 −30 crux/src/Crux/FormatOut.hs
+180 −164 crux/src/Crux/Goal.hs
+225 −27 crux/src/Crux/Log.hs
+4 −56 crux/src/Crux/Model.hs
+25 −6 crux/src/Crux/ProgressBar.hs
+109 −70 crux/src/Crux/Report.hs
+1 −2 crux/src/Crux/SVCOMP.hs
+25 −51 crux/src/Crux/Types.hs
+3 −3 crux/src/Crux/UI/JS.hs
+44 −2 uc-crux-llvm/src/UCCrux/LLVM/Logging.hs
+52 −13 uc-crux-llvm/src/UCCrux/LLVM/Main.hs
+4 −6 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+1 −4 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs
+7 −8 uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs
+6 −6 uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs
+11 −12 uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+108 −49 uc-crux-llvm/test/Test.hs
2 changes: 1 addition & 1 deletion deps/flexdis86
Submodule flexdis86 updated 12 files
+3 −3 .github/workflows/ci.yaml
+2 −2 data/optable.xml
+2 −1 flexdis86.cabal
+3 −2 src/Flexdis86/Assembler.hs
+125 −75 src/Flexdis86/Disassembler.hs
+4 −3 src/Flexdis86/InstructionSet.hs
+39 −22 src/Flexdis86/OpTable.hs
+12 −3 src/Flexdis86/Operand.hs
+99 −77 src/Flexdis86/Prefixes.hs
+15 −4 src/Flexdis86/Register.hs
+7 −1 src/Flexdis86/Segment.hs
+19 −5 src/Flexdis86/Sizes.hs
2 changes: 1 addition & 1 deletion deps/macaw
Submodule macaw updated 39 files
+37 −12 .github/workflows/ci.yaml
+3 −1 base/macaw-base.cabal
+0 −9 base/src/Data/Macaw/AbsDomain/StackAnalysis.hs
+11 −16 base/src/Data/Macaw/Analysis/FunctionArgs.hs
+116 −58 base/src/Data/Macaw/Analysis/RegisterUse.hs
+46 −28 base/src/Data/Macaw/Discovery.hs
+11 −10 base/src/Data/Macaw/Discovery/State.hs
+718 −639 base/src/Data/Macaw/Dwarf.hs
+4 −4 base/src/Data/Macaw/Memory/ElfLoader.hs
+14 −3 base/src/Data/Macaw/Utils/IncComp.hs
+1 −1 deps/crucible
+1 −1 deps/dismantle
+1 −1 deps/dwarf
+1 −1 deps/elf-edit
+1 −1 deps/flexdis86
+1 −1 deps/llvm-pretty-bc-parser
+1 −1 deps/macaw-loader
+1 −1 deps/what4
+1 −1 deps/what4-serialize
+1 −0 macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
+1 −1 macaw-semmc/macaw-semmc.cabal
+0 −1 macaw-semmc/src/Data/Macaw/SemMC/Operands.hs
+0 −2 macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
+3 −4 refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+1 −1 symbolic/macaw-symbolic.cabal
+22 −23 symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+1 −2 symbolic/src/Data/Macaw/Symbolic/Memory.hs
+1 −1 x86/macaw-x86.cabal
+12 −4 x86/src/Data/Macaw/X86/ArchTypes.hs
+30 −25 x86/src/Data/Macaw/X86/InstructionDef.hs
+47 −57 x86/src/Data/Macaw/X86/Semantics.hs
+1 −0 x86/src/Data/Macaw/X86/Semantics/ADX.hs
+3 −3 x86/src/Data/Macaw/X86/Semantics/AESNI.hs
+21 −20 x86/src/Data/Macaw/X86/Semantics/AVX.hs
+1 −0 x86/src/Data/Macaw/X86/Semantics/BMI2.hs
+1 −1 x86/src/Data/Macaw/X86/Semantics/SHA.hs
+34 −0 x86_symbolic/tests/pass/bitscan.c
+ − x86_symbolic/tests/pass/bitscan.opt.exe
+ − x86_symbolic/tests/pass/bitscan.unopt.exe
Binary file modified examples/salsa20/salsa20.bc
View file
Binary file not shown.
1 change: 1 addition & 0 deletions heapster-saw/heapster-saw.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ library
Verifier.SAW.Heapster.Parser
Verifier.SAW.Heapster.Permissions
Verifier.SAW.Heapster.PermParser
Verifier.SAW.Heapster.NamePropagation
Verifier.SAW.Heapster.RustTypes
Verifier.SAW.Heapster.SAWTranslation
Verifier.SAW.Heapster.Token
Expand Down
65 changes: 65 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
{-# Language ScopedTypeVariables #-}
{-# Language GADTs #-}
module Verifier.SAW.Heapster.NamePropagation where

import Data.Functor.Constant
import Data.Parameterized.TraversableFC ( FoldableFC(toListFC), FunctorFC(fmapFC) )
import Lang.Crucible.Analysis.Fixpoint
import Lang.Crucible.CFG.Core ( Some(Some), CFG(cfgHandle) )
import Lang.Crucible.FunctionHandle ( FnHandle(handleArgTypes) )
import Lang.Crucible.LLVM.Extension ( LLVM, LLVMStmt(..), LLVM_Dbg(..) )
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Map as PM
import qualified Text.LLVM.AST as L

type NameDom = Pointed (Constant String)

nameJoin :: Constant String a -> Constant String a -> NameDom a
nameJoin (Constant x) (Constant y) | x == y = Pointed (Constant x)
nameJoin _ _ = Top

nameDomain :: Domain (Pointed (Constant String))
nameDomain = pointed nameJoin (==) WTO

nameInterpretation :: Interpretation LLVM NameDom
nameInterpretation = Interpretation
{ interpExpr = \_ _ _ names -> (Just names, Bottom)
, interpCall = \_ _ _ _ _ names -> (Just names, Bottom)
, interpReadGlobal = \_ names -> (Just names, Bottom)
, interpWriteGlobal = \_ _ names -> Just names
, interpBr = \_ _ _ _ names -> (Just names, Just names)
, interpMaybe = \_ _ _ names -> (Just names, Bottom, Just names)
, interpExt = \_ stmt names ->
let names' =
case stmt of
LLVM_Debug (LLVM_Dbg_Declare ptr di _) | Just n <- L.dilvName di ->
modifyAbstractRegValue names ptr (\_ -> Pointed (Constant ("&" ++ n)))
LLVM_Debug (LLVM_Dbg_Addr ptr di _) | Just n <- L.dilvName di ->
modifyAbstractRegValue names ptr (\_ -> Pointed (Constant ("&" ++ n)))
LLVM_Debug (LLVM_Dbg_Value _ val di _) | Just n <- L.dilvName di ->
modifyAbstractRegValue names val (\_ -> Pointed (Constant n))
_ -> names
in (Just names', Bottom)
}

computeNames ::
forall blocks init ret.
CFG LLVM blocks init ret ->
Ctx.Assignment (Constant [Maybe String]) blocks
computeNames cfg =
case alg of
(_, end, _) -> fmapFC (\(Ignore (Some p)) -> Constant (toListFC flatten (_paRegisters p))) end
where
flatten :: NameDom a -> Maybe String
flatten Top = Nothing
flatten Bottom = Nothing
flatten (Pointed (Constant x)) = Just x

sz = Ctx.size (handleArgTypes (cfgHandle cfg))
alg =
forwardFixpoint'
nameDomain
nameInterpretation
cfg
PM.empty
(Ctx.replicate sz Bottom)
2 changes: 2 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -599,6 +599,8 @@ instance TransInfo info =>
return $ error "translate: RealValRepr"
[nuMP| ComplexRealRepr |] ->
return $ error "translate: ComplexRealRepr"
[nuMP| SequenceRepr{} |] ->
return $ error "translate: SequenceRepr"
[nuMP| BVRepr w |] ->
returnType1 =<< bitvectorTransM (translate w)

Expand Down
1 change: 1 addition & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -331,6 +331,7 @@ tcExpr WordMapRepr {} e = tcError (pos e) "Expected wordmap"
tcExpr StringMapRepr {} e = tcError (pos e) "Expected stringmap"
tcExpr SymbolicArrayRepr {} e = tcError (pos e) "Expected symbolicarray"
tcExpr SymbolicStructRepr{} e = tcError (pos e) "Expected symbolicstruct"
tcExpr SequenceRepr {} e = tcError (pos e) "Expected sequencerepr"

-- | Check for a unit literal
tcUnit :: AstExpr -> Tc (PermExpr UnitType)
Expand Down
Loading

0 comments on commit fa9cc39

Please sign in to comment.