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

Bump what4 submodule (and friends) to bring in GaloisInc/what4#277 changes #2226

Merged
merged 2 commits into from
Feb 17, 2025
Merged

Bump what4 submodule (and friends) to bring in GaloisInc/what4#277 changes #2226

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5e6d62e
Bump macaw submodule to bring in GaloisInc/macaw#459 changes
RyanGlScott Feb 17, 2025
a6c47f2
Bump what4 submodule (and friends) to bring in GaloisInc/what4#277 ch…
RyanGlScott Feb 17, 2025
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: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,3 +52,6 @@
[submodule "deps/mir-json"]
path = deps/mir-json
url = https://github.com/GaloisInc/mir-json.git
[submodule "deps/macaw-loader"]
path = deps/macaw-loader
url = https://github.com/GaloisInc/macaw-loader.git
3 changes: 3 additions & 0 deletions cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,12 @@ packages:
deps/lmdb/lmdb
deps/lmdb/lmdb-simple
deps/macaw/base
deps/macaw/macaw-dump
deps/macaw/symbolic
deps/macaw/x86
deps/macaw/x86_symbolic
deps/macaw-loader/macaw-loader
deps/macaw-loader/macaw-loader-x86
deps/elf-edit
deps/dwarf
deps/argo/argo
Expand Down
2 changes: 1 addition & 1 deletion deps/crucible
Open in desktop
Submodule crucible updated 2 files
+2 −2 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+1 −1 dependencies/what4
2 changes: 1 addition & 1 deletion deps/macaw
Open in desktop
Submodule macaw updated 118 files
1 change: 1 addition & 0 deletions deps/macaw-loader
Open in desktop
Submodule macaw-loader added at 57ebde
2 changes: 1 addition & 1 deletion deps/what4
Open in desktop
Submodule what4 updated 14 files
+7 −0 what4/CHANGES.md
+26 −23 what4/src/What4/Expr/App.hs
+108 −14 what4/src/What4/Expr/BoolMap.hs
+34 −18 what4/src/What4/Expr/Builder.hs
+1 −10 what4/src/What4/Expr/GroundEval.hs
+5 −5 what4/src/What4/Expr/VarIdentification.hs
+5 −5 what4/src/What4/Protocol/SMTWriter.hs
+1 −1 what4/src/What4/Protocol/VerilogWriter/Backend.hs
+1 −1 what4/src/What4/Serialize/Printer.hs
+295 −0 what4/test/Bool.hs
+62 −0 what4/test/BoolNormalization.hs
+3 −0 what4/test/ExprsTest.hs
+4 −1 what4/test/OnlineSolverTest.hs
+11 −0 what4/what4.cabal
18 changes: 9 additions & 9 deletions saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ data SAWExpr (bt :: BaseType) where
getInputs :: SAWCoreState n -> IO (Seq (SC.ExtCns SC.Term))
getInputs st = readIORef (saw_inputs st)

baseSCType ::
baseSCType ::
sym ->
SC.SharedContext ->
BaseTypeRepr tp ->
Expand Down Expand Up @@ -600,10 +600,10 @@ evaluateExpr sym st sc cache = f []
goNeg env x

B.ConjPred xs ->
case BM.viewBoolMap xs of
BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc True
BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc False
BM.BoolMapTerms (t:|ts) ->
case BM.viewConjMap xs of
BM.ConjTrue -> SAWExpr <$> SC.scBool sc True
BM.ConjFalse -> SAWExpr <$> SC.scBool sc False
BM.Conjuncts (t:|ts) ->
let pol (x,BM.Positive) = f env x
pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x
in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts)
Expand Down Expand Up @@ -940,10 +940,10 @@ evaluateExpr sym st sc cache = f []
case expr of
-- negation of (x /\ y) becomes (~x \/ ~y)
B.AppExpr (B.appExprApp -> B.ConjPred xs) ->
case BM.viewBoolMap xs of
BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc False
BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc True
BM.BoolMapTerms (t:|ts) ->
case BM.viewConjMap xs of
BM.ConjTrue -> SAWExpr <$> SC.scBool sc False
BM.ConjFalse -> SAWExpr <$> SC.scBool sc True
BM.Conjuncts (t:|ts) ->
let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x
pol (x, BM.Negative) = f env x
in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts)
Expand Down
Loading