Skip to content

Commit

Permalink
Merge pull request #68 from boogie-org/PropInstMatchFix
Browse files Browse the repository at this point in the history 
Prop instrumentation match fix for Ref type
  • Loading branch information
@shuvendu-lahiri
shuvendu-lahiri authored Jul 18, 2018
2 parents 179251c + 0367812 commit b3b26bb
Show file tree
Hide file tree
Showing 5 changed files with 88 additions and 52 deletions.
105 changes: 55 additions & 50 deletions AddOns/AngelicVerifierNull/test/propinst-regressions/Answer
View file
Original file line number Diff line number Diff line change
@@ -1,50 +1,55 @@

-------------------- uaf0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0

-------------------- uaf1.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf1_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])

-------------------- df0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing df0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0

-------------------- uaf2.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf2_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])

-------------------- uaf3.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf3_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])

-------------------- irql0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing irql0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 2)

-------------------- irql1.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing irql1_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 1)

-------------------- irql2.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing irql2_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int, x_2: int :: unknownTrigger_0(x_1) && unknownTrigger_1(x_2) ==> x_1 <= x_2)

-------------------- null0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing null0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr !(ax == NULL)

-------------------- uaf0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0

-------------------- uaf1.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf1_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])

-------------------- df0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing df0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0

-------------------- uaf2.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf2_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])

-------------------- uaf3.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing uaf3_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])

-------------------- irql0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing irql0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 2)

-------------------- irql1.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing irql1_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 1)

-------------------- irql2.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing irql2_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int, x_2: int :: unknownTrigger_0(x_1) && unknownTrigger_1(x_2) ==> x_1 <= x_2)

-------------------- null0.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing null0_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr !(ax == NULL)

-------------------- rodrigo_refnull.bpl --------------------
[TAG: AV_OUTPUT] ----- Analyzing rodrigo_refnull_pinst_hinst.bpl ------
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc Foo with expr r != null
9 changes: 9 additions & 0 deletions AddOns/AngelicVerifierNull/test/propinst-regressions/rodrigo_refnull.bpl
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
type Ref;

const unique null : Ref;
var r: Ref;

procedure Foo() {
r := null;
assume {:nonnull} r != null;
}
1 change: 1 addition & 0 deletions AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ call:add irql0.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle
call:add irql1.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle.avp
call:add irql2.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle.avp
call:add null0.bpl ..\..\..\PropInst\PropInst\ExampleProperties\nullcheck-razzle.avp
call:add rodrigo_refnull.bpl ..\..\..\PropInst\PropInst\ExampleProperties\nullcheck-csharp.avp

REM for %%f in (eeSlice3.bpl) do (
set i=0
Expand Down
21 changes: 21 additions & 0 deletions AddOns/PropInst/PropInst/ExampleProperties/nullcheck-csharp.avp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
GlobalDeclarations
{
function {:inline} {:aliasingQuery} {:mkUniqueFn} aliasQ(p:Ref, q:Ref) returns (bool) { p == q }
}


TemplateVariables
{
var p : Ref;
}


//Check every dereference
CmdRule
{
assume {:nonnull} p != null;
}
-->
{
assert p != null;
}
4 changes: 2 additions & 2 deletions source/Util/Visitor.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1294,7 +1294,7 @@ public override Expr VisitNAryExpr(NAryExpr node)
var nodeFunc = ((FunctionCall)node.Fun).Func;
for (var i = 0; i < tcFunc.InParams.Count; i++)
{
if (!Equals(tcFunc.InParams[i].TypedIdent.Type, nodeFunc.InParams[i].TypedIdent.Type))
if (!Equals(tcFunc.InParams[i].TypedIdent.Type.ToString(), nodeFunc.InParams[i].TypedIdent.Type.ToString()))
{
Matches = false;
return base.VisitNAryExpr(node);
Expand Down Expand Up @@ -1355,7 +1355,7 @@ public override Expr VisitIdentifierExpr(IdentifierExpr node)

if (idexToConsume.Decl != null)
{
if (Equals(node.Decl.TypedIdent.Type, idexToConsume.Decl.TypedIdent.Type)
if (Equals(node.Decl.TypedIdent.Type.ToString(), idexToConsume.Decl.TypedIdent.Type.ToString())
&& AreAttributesASubset(idexToConsume.Decl.Attributes, node.Decl.Attributes))
{
Substitution.Add(idexToConsume.Decl, node);
Expand Down

0 comments on commit b3b26bb

Please sign in to comment.