Skip to content

Commit 03e1382

Browse files
author
ed sandberg
committed
Add vacuity detection in MIR and JVM backends
* Extracted vacuity logic (checkAssumptionsForContradictions, etc.) into a new backend independent module: SAWCentral.Crucible.Common.Vacuity. * Hooked vacuity checks into: * mir_verify in SAWCentral.Crucible.MIR.Builtins * jvm_verify in SAWCentral.Crucible.JVM.Builtins * verifyMethodSpec and refineMethodSpec in SAWCentral.Crucible.LLVM.Builtins Fixes #2028
1 parent ceb9151 commit 03e1382

File tree

16 files changed

+202
-85
lines changed

16 files changed

+202
-85
lines changed

‎CHANGES.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,11 @@ Note that build.sh is in any case the recommended way to build.
3636

3737
* Support `bmux` gates in exported Yosys directly to avoid reliance on `bmuxmap`
3838

39+
* Vacuity checking (`--detect-vacuity`) now correctly reports contradictions in specifications
40+
for all Crucible backends: LLVM, MIR, and JVM. Previously, vacuous proofs in MIR and JVM
41+
code could go undetected.
42+
43+
3944
## Bug fixes
4045

4146
* The `head` and `tail` primitives are now implemented in the SAW-Core

‎intTests/test2028_vacuity_detect/Makefile

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
all: test.bc test.linked-mir.json Test.class
2+
3+
test.bc: test.c
4+
clang -emit-llvm -c -o $@ $<
5+
6+
test.linked-mir.json: test.rs
7+
saw-rustc $<
8+
9+
Test.class: Test.java
10+
javac -g $<

‎intTests/test2028_vacuity_detect/README

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
This test checks for vacuous proofs across LLVM, MIR, and JVM backends.
2+
3+
It corresponds to issue https://github.com/GaloisInc/saw-script/issues/2028
4+
5+
Each function includes a contradictory precondition (e.g., x != x), and SAW should detect this
6+
and emit a vacuity warning before successfully proving the function.

‎intTests/test2028_vacuity_detect/Test.class

286 Bytes
Binary file not shown.

‎intTests/test2028_vacuity_detect/Test.java

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
public class Test {
2+
public static void fun_jvm() {
3+
}
4+
}

‎intTests/test2028_vacuity_detect/test.bc

2.11 KB
Binary file not shown.

‎intTests/test2028_vacuity_detect/test.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
// test.c
2+
void fun_c() {}

‎intTests/test2028_vacuity_detect/test.linked-mir.json

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{"version":1,"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:2:19: 2:19"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/648686db::fun_rs","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/648686db::fun_rs","kind":"Item","substs":[]},"name":"test/648686db::fun_rs"}],"tys":[{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}}],"roots":["test/648686db::fun_rs"]}

‎intTests/test2028_vacuity_detect/test.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
// test.rs
2+
pub fn fun_rs() {}

‎intTests/test2028_vacuity_detect/test.saw

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// test.saw
2+
enable_experimental;
3+
4+
let fun_c_spec = do {
5+
x <- llvm_fresh_var "x" (llvm_int 32);
6+
llvm_precond {{ x != x }};
7+
llvm_execute_func [];
8+
};
9+
llvm_mod <- llvm_load_module "test.bc";
10+
llvm_verify llvm_mod "fun_c" [] false fun_c_spec z3;
11+
12+
let fun_rs_spec = do {
13+
x <- mir_fresh_var "x" mir_u32;
14+
mir_precond {{ x != x }};
15+
mir_execute_func [];
16+
};
17+
mir_mod <- mir_load_module "test.linked-mir.json";
18+
mir_verify mir_mod "test::fun_rs" [] false fun_rs_spec z3;
19+
20+
let fun_jvm_spec = do {
21+
x <- jvm_fresh_var "x" java_int;
22+
jvm_precond {{ x != x }}; // Always false
23+
jvm_execute_func [];
24+
};
25+
26+
cls <- java_load_class "Test";
27+
jvm_verify cls "fun_jvm" [] false fun_jvm_spec z3;

‎intTests/test2028_vacuity_detect/test.sh

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#!/bin/bash
2+
3+
n=$( "$SAW" --detect-vacuity test.saw 2>&1 | tee /dev/stderr | grep -c "Contradiction detected" )
4+
5+
if [ "$n" -eq 3 ]; then
6+
echo "Found 3 expected contradictions"
7+
exit 0
8+
else
9+
echo "Expected 3 contradictions, found $n"
10+
exit 1
11+
fi

‎saw-central/src/SAWCentral/Crucible/Common/Vacuity.hs

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
{-# LANGUAGE RankNTypes #-}
2+
{-# LANGUAGE FlexibleContexts #-}
3+
{-# LANGUAGE LambdaCase #-}
4+
{-# LANGUAGE OverloadedStrings #-}
5+
6+
module SAWCentral.Crucible.Common.Vacuity (
7+
checkAssumptionsForContradictions
8+
) where
9+
10+
import Prelude hiding (fail)
11+
12+
import Control.Lens
13+
import Control.Monad (forM_)
14+
import Control.Monad.Extra (findM, whenM)
15+
import Data.Function
16+
import Data.List
17+
import qualified What4.ProgramLoc as W4
18+
import qualified What4.Interface as W4
19+
import qualified Lang.Crucible.Backend as Crucible
20+
import SAWCore.SharedTerm
21+
import SAWCoreWhat4.ReturnTrip
22+
import SAWCentral.Proof
23+
import SAWCentral.TopLevel
24+
import SAWCentral.Value
25+
import SAWCentral.Options
26+
import qualified SAWCentral.Crucible.Common as Common
27+
import SAWCentral.Crucible.Common.MethodSpec (CrucibleMethodSpecIR)
28+
import qualified SAWCentral.Crucible.Common.MethodSpec as MS
29+
30+
type AssumptionReason = (MS.ConditionMetadata, String)
31+
32+
-- | Checks whether the given list of assumptions contains a contradiction, and
33+
-- if so, computes and displays a minimal set of contradictory assumptions.
34+
checkAssumptionsForContradictions ::
35+
Show (MS.MethodId ext) =>
36+
Common.Sym ->
37+
CrucibleMethodSpecIR ext ->
38+
ProofScript () ->
39+
[Crucible.LabeledPred Term AssumptionReason] ->
40+
TopLevel ()
41+
checkAssumptionsForContradictions sym methodSpec tactic assumptions =
42+
whenM
43+
(assumptionsContainContradiction sym methodSpec tactic assumptions)
44+
(computeMinimalContradictingCore sym methodSpec tactic assumptions)
45+
46+
-- | Checks for contradictions within the given list of assumptions, by asking
47+
-- the solver about whether their conjunction entails falsehood.
48+
assumptionsContainContradiction ::
49+
Show (MS.MethodId ext) =>
50+
Common.Sym ->
51+
CrucibleMethodSpecIR ext ->
52+
ProofScript () ->
53+
[Crucible.LabeledPred Term AssumptionReason] ->
54+
TopLevel Bool
55+
assumptionsContainContradiction sym methodSpec tactic assumptions =
56+
do
57+
st <- io $ Common.sawCoreState sym
58+
let sc = saw_ctx st
59+
let ploc = methodSpec^.MS.csLoc
60+
(goal',pgl) <- io $
61+
do
62+
-- conjunction of all assumptions
63+
assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
64+
-- implies falsehood
65+
goal <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
66+
goal' <- boolToProp sc [] goal
67+
return $ (goal',
68+
ProofGoal
69+
{ goalNum = 0
70+
, goalType = "vacuousness check"
71+
, goalName = show (methodSpec^.MS.csMethod)
72+
, goalLoc = show (W4.plSourceLoc ploc) ++ " in " ++ show (W4.plFunction ploc)
73+
, goalDesc = "vacuousness check"
74+
, goalSequent = propToSequent goal'
75+
, goalTags = mempty
76+
})
77+
res <- runProofScript tactic goal' pgl Nothing
78+
"vacuousness check" False False
79+
case res of
80+
ValidProof _ _ -> return True
81+
InvalidProof _ _ _ -> return False
82+
UnfinishedProof _ ->
83+
-- TODO? is this the right behavior?
84+
do printOutLnTop Warn "Could not determine if preconditions are vacuous"
85+
return True
86+
87+
-- | Given a list of assumptions, computes and displays a smallest subset of
88+
-- them that are contradictory among each themselves. This is **not**
89+
-- implemented efficiently.
90+
computeMinimalContradictingCore ::
91+
Show (MS.MethodId ext) =>
92+
Common.Sym ->
93+
CrucibleMethodSpecIR ext ->
94+
ProofScript () ->
95+
[Crucible.LabeledPred Term AssumptionReason] ->
96+
TopLevel ()
97+
computeMinimalContradictingCore sym methodSpec tactic assumes =
98+
do
99+
printOutLnTop Warn "Contradiction detected! Computing minimal core of contradictory assumptions:"
100+
-- test subsets of assumptions of increasing sizes until we find a
101+
-- contradictory one
102+
let cores = sortBy (compare `on` length) (subsequences assumes)
103+
findM (assumptionsContainContradiction sym methodSpec tactic) cores >>= \case
104+
Nothing ->
105+
printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction."
106+
Just core ->
107+
forM_ core $ \assume ->
108+
case assume^.Crucible.labeledPredMsg of
109+
(loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason)
110+
printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous."

‎saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,7 @@ import qualified SAWCentral.Crucible.Common as Common
133133
import SAWCentral.Crucible.Common
134134
import SAWCentral.Crucible.Common.Override (MetadataMap)
135135
import SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..), nextAllocIndex, PrePost(..))
136+
import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
136137

137138
import qualified SAWCentral.Crucible.Common.MethodSpec as MS
138139
import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
@@ -247,6 +248,14 @@ jvm_verify cls nm lemmas checkSat setup tactic =
247248
-- construct the initial state for verifications
248249
(args, assumes, env, globals2) <- io $ verifyPrestate cc methodSpec globals1
249250

251+
-- check for contradictory preconditions
252+
when (detectVacuity opts) $
253+
Vacuity.checkAssumptionsForContradictions
254+
sym
255+
methodSpec
256+
tactic
257+
assumes
258+
250259
-- save initial path conditions
251260
frameIdent <- io $ Crucible.pushAssumptionFrame bak
252261

‎saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs

Lines changed: 5 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -94,8 +94,7 @@ import Prelude hiding (fail)
9494
import qualified Control.Exception as X
9595
import Control.Lens
9696

97-
import Control.Monad (foldM, forM, forM_, replicateM, unless, when)
98-
import Control.Monad.Extra (findM, whenM)
97+
import Control.Monad (foldM, forM, replicateM, unless, when)
9998
import Control.Monad.Fail (MonadFail(..))
10099
import Control.Monad.IO.Class (MonadIO(..))
101100
import Control.Monad.Reader (runReaderT)
@@ -104,7 +103,6 @@ import Control.Monad.Trans.Class (MonadTrans(..))
104103
import qualified Data.Bimap as Bimap
105104
import Data.Char (isDigit)
106105
import Data.Foldable (for_, toList, fold)
107-
import Data.Function
108106
import Data.Functor (void)
109107
import Data.IORef
110108
import Data.List
@@ -177,6 +175,8 @@ import qualified Lang.Crucible.LLVM.Translation as Crucible
177175

178176
import qualified SAWCentral.Crucible.LLVM.CrucibleLLVM as Crucible
179177

178+
import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
179+
180180
-- parameterized-utils
181181
import qualified Data.Parameterized.TraversableFC as Ctx
182182

@@ -654,7 +654,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
654654
io $ verifyPrestate opts cc methodSpec globals1
655655

656656
when (detectVacuity opts)
657-
$ checkAssumptionsForContradictions cc methodSpec tactic assumes
657+
$ Vacuity.checkAssumptionsForContradictions sym methodSpec tactic assumes
658658

659659
-- save initial path conditions
660660
frameIdent <- io $ Crucible.pushAssumptionFrame bak
@@ -755,7 +755,7 @@ refineMethodSpec cc methodSpec lemmas tactic =
755755
io $ verifyPrestate opts cc methodSpec globals1
756756

757757
when (detectVacuity opts)
758-
$ checkAssumptionsForContradictions cc methodSpec tactic assumes
758+
$ Vacuity.checkAssumptionsForContradictions sym methodSpec tactic assumes
759759

760760
-- save initial path conditions
761761
frameIdent <- io $ Crucible.pushAssumptionFrame bak
@@ -981,86 +981,6 @@ verifyPrestate opts cc mspec globals =
981981

982982
return (args, cs, env, globals2)
983983

984-
-- | Checks for contradictions within the given list of assumptions, by asking
985-
-- the solver about whether their conjunction entails falsehood.
986-
assumptionsContainContradiction ::
987-
(Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
988-
LLVMCrucibleContext arch ->
989-
MS.CrucibleMethodSpecIR (LLVM arch) ->
990-
ProofScript () ->
991-
[Crucible.LabeledPred Term AssumptionReason] ->
992-
TopLevel Bool
993-
assumptionsContainContradiction cc methodSpec tactic assumptions =
994-
do
995-
let sym = cc^.ccSym
996-
st <- io $ Common.sawCoreState sym
997-
let sc = saw_ctx st
998-
let ploc = methodSpec^.MS.csLoc
999-
(goal',pgl) <- io $
1000-
do
1001-
-- conjunction of all assumptions
1002-
assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
1003-
-- implies falsehood
1004-
goal <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
1005-
goal' <- boolToProp sc [] goal
1006-
return $ (goal',
1007-
ProofGoal
1008-
{ goalNum = 0
1009-
, goalType = "vacuousness check"
1010-
, goalName = show (methodSpec^.MS.csMethod)
1011-
, goalLoc = show (W4.plSourceLoc ploc) ++ " in " ++ show (W4.plFunction ploc)
1012-
, goalDesc = "vacuousness check"
1013-
, goalSequent = propToSequent goal'
1014-
, goalTags = mempty
1015-
})
1016-
res <- runProofScript tactic goal' pgl Nothing
1017-
"vacuousness check" False False
1018-
case res of
1019-
ValidProof _ _ -> return True
1020-
InvalidProof _ _ _ -> return False
1021-
UnfinishedProof _ ->
1022-
-- TODO? is this the right behavior?
1023-
do printOutLnTop Warn "Could not determine if preconditions are vacuous"
1024-
return True
1025-
1026-
-- | Given a list of assumptions, computes and displays a smallest subset of
1027-
-- them that are contradictory among each themselves. This is **not**
1028-
-- implemented efficiently.
1029-
computeMinimalContradictingCore ::
1030-
(Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
1031-
LLVMCrucibleContext arch ->
1032-
MS.CrucibleMethodSpecIR (LLVM arch) ->
1033-
ProofScript () ->
1034-
[Crucible.LabeledPred Term AssumptionReason] ->
1035-
TopLevel ()
1036-
computeMinimalContradictingCore cc methodSpec tactic assumes =
1037-
do
1038-
printOutLnTop Warn "Contradiction detected! Computing minimal core of contradictory assumptions:"
1039-
-- test subsets of assumptions of increasing sizes until we find a
1040-
-- contradictory one
1041-
let cores = sortBy (compare `on` length) (subsequences assumes)
1042-
findM (assumptionsContainContradiction cc methodSpec tactic) cores >>= \case
1043-
Nothing -> printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction."
1044-
Just core ->
1045-
forM_ core $ \assume ->
1046-
case assume^.Crucible.labeledPredMsg of
1047-
(loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason)
1048-
printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous."
1049-
1050-
-- | Checks whether the given list of assumptions contains a contradiction, and
1051-
-- if so, computes and displays a minimal set of contradictory assumptions.
1052-
checkAssumptionsForContradictions ::
1053-
(Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
1054-
LLVMCrucibleContext arch ->
1055-
MS.CrucibleMethodSpecIR (LLVM arch) ->
1056-
ProofScript () ->
1057-
[Crucible.LabeledPred Term AssumptionReason] ->
1058-
TopLevel ()
1059-
checkAssumptionsForContradictions cc methodSpec tactic assumes =
1060-
whenM
1061-
(assumptionsContainContradiction cc methodSpec tactic assumes)
1062-
(computeMinimalContradictingCore cc methodSpec tactic assumes)
1063-
1064984
-- | Check two MemTypes for register compatiblity. This is a stricter
1065985
-- check than the memory compatiblity check that is done for points-to
1066986
-- assertions.

‎saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,7 @@ import qualified SAWCentral.Crucible.Common.MethodSpec as MS
132132
import SAWCentral.Crucible.Common.Override
133133
import qualified SAWCentral.Crucible.Common.Setup.Builtins as Setup
134134
import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
135+
import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
135136
import SAWCentral.Crucible.MIR.MethodSpecIR
136137
import SAWCentral.Crucible.MIR.Override
137138
import SAWCentral.Crucible.MIR.ResolveSetupValue
@@ -710,6 +711,14 @@ mir_verify rm nm lemmas checkSat setup tactic =
710711
-- save initial path conditions
711712
frameIdent <- io $ Crucible.pushAssumptionFrame bak
712713

714+
-- check for contradictory preconditions
715+
when (detectVacuity opts) $
716+
Vacuity.checkAssumptionsForContradictions
717+
sym
718+
methodSpec
719+
tactic
720+
assumes
721+
713722
-- run the symbolic execution
714723
printOutLnTop Info $
715724
unwords ["Simulating", show (methodSpec ^. MS.csMethod), "..."]

‎saw.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -641,6 +641,7 @@ library saw-central
641641
SAWCentral.Crucible.Common.Setup.Builtins
642642
SAWCentral.Crucible.Common.Setup.Type
643643
SAWCentral.Crucible.Common.Setup.Value
644+
SAWCentral.Crucible.Common.Vacuity
644645

645646
SAWCentral.Crucible.LLVM.Builtins
646647
SAWCentral.Crucible.LLVM.Boilerplate

0 commit comments

Comments
 (0)