Skip to content

Commit

Permalink
[Civl] Add snapshot with parallel scans (#984)
Browse files Browse the repository at this point in the history 
Version of snapshot.bpl with both first and second scans being done in
parallel.
  • Loading branch information
@shazqadeer
shazqadeer authored Nov 14, 2024
1 parent 331cdf6 commit e8b5158
Show file tree
Hide file tree
Showing 7 changed files with 214 additions and 51 deletions.
10 changes: 7 additions & 3 deletions Source/Core/Analysis/ModSetCollector.cs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;

namespace Microsoft.Boogie;

Expand Down Expand Up @@ -29,10 +30,13 @@ public void DoModSetAnalysis(Implementation impl)
{
this.VisitImplementation(impl);
var proc = impl.Proc;
proc.Modifies = new List<IdentifierExpr>();
foreach (Variable v in modSets[proc])
if (modSets.ContainsKey(proc))
{
proc.Modifies.Add(new IdentifierExpr(v.tok, v));
proc.Modifies = new List<IdentifierExpr>(modSets[proc].Select(v => new IdentifierExpr(v.tok, v)));
}
else
{
proc.Modifies = new List<IdentifierExpr>();
}
}

Expand Down
4 changes: 2 additions & 2 deletions Source/Core/BoogiePL.atg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -759,11 +759,11 @@ SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>

SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs.>
=
(. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
(. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List<Variable> locals; StmtList stmtList; .)
"refines"
{ Attribute<ref kv> }
(
MoverQualifier<ref moverType>
[ MoverQualifier<ref moverType> ]
"action" (. tok = t; .)
{ Attribute<ref akv> }
Ident<out m>
Expand Down
55 changes: 29 additions & 26 deletions Source/Core/Parser.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1219,13 +1219,15 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) {
}

void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs) {
IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList;
IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.Atomic; List<Variable> locals; StmtList stmtList;
Expect(41);
while (la.kind == 26) {
Attribute(ref kv);
}
if (StartOf(5)) {
MoverQualifier(ref moverType);
if (StartOf(16)) {
if (StartOf(5)) {
MoverQualifier(ref moverType);
}
Expect(39);
tok = t;
while (la.kind == 26) {
Expand Down Expand Up @@ -1274,7 +1276,7 @@ void SpecYieldRequires(List<Requires> pre, List<CallCmd> yieldRequires ) {
Expr e; Cmd cmd; Token tok; QKeyValue kv = null;
Expect(49);
tok = t;
if (StartOf(16)) {
if (StartOf(17)) {
while (la.kind == 26) {
Attribute(ref kv);
}
Expand Down Expand Up @@ -1338,7 +1340,7 @@ void SpecYieldEnsures(List<Ensures> post, List<CallCmd> yieldEnsures ) {
Expr e; Cmd cmd; Token tok; QKeyValue kv = null;
Expect(50);
tok = t;
if (StartOf(16)) {
if (StartOf(17)) {
while (la.kind == 26) {
Attribute(ref kv);
}
Expand Down Expand Up @@ -1423,8 +1425,8 @@ void StmtList(out StmtList/*!*/ stmtList) {
StructuredCmd ec = null; StructuredCmd/*!*/ ecn;
TransferCmd tc = null; TransferCmd/*!*/ tcn;

while (StartOf(17)) {
if (StartOf(18)) {
while (StartOf(18)) {
if (StartOf(19)) {
LabelOrCmd(out c, out label);
Contract.Assert(c == null || label == null);
if (c != null) {
Expand Down Expand Up @@ -1655,7 +1657,7 @@ void WhileCmd(out WhileCmd wcmd) {
while (la.kind == 26) {
Attribute(ref kv);
}
if (StartOf(19)) {
if (StartOf(20)) {
Expression(out e);
if (isFree) {
invariants.Add(new AssumeCmd(z, e, kv));
Expand Down Expand Up @@ -1695,7 +1697,7 @@ void Guard(out Expr e) {
if (la.kind == 60) {
Get();
e = null;
} else if (StartOf(19)) {
} else if (StartOf(20)) {
Expression(out ee);
e = ee;
} else SynErr(152);
Expand Down Expand Up @@ -1733,7 +1735,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
Expect(10);
c = new UnpackCmd(x, lhsExpr, e0, kv);

} else if (StartOf(20)) {
} else if (StartOf(21)) {
lhss = new List<AssignLhs/*!*/>();
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
while (la.kind == 19 || la.kind == 70) {
Expand Down Expand Up @@ -1804,7 +1806,7 @@ void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {

Expect(19);
x = t;
if (StartOf(19)) {
if (StartOf(20)) {
Expression(out e);
indexes.Add(e);
while (la.kind == 14) {
Expand Down Expand Up @@ -1839,7 +1841,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
Ident(out first);
if (la.kind == 11) {
Get();
if (StartOf(19)) {
if (StartOf(20)) {
Expression(out en);
es.Add(en);
while (la.kind == 14) {
Expand All @@ -1865,7 +1867,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
Expect(69);
Ident(out first);
Expect(11);
if (StartOf(19)) {
if (StartOf(20)) {
Expression(out en);
es.Add(en);
while (la.kind == 14) {
Expand Down Expand Up @@ -1893,7 +1895,7 @@ void Expressions(out List<Expr>/*!*/ es) {
void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
LogicalExpression(out e0);
if (StartOf(21)) {
if (StartOf(22)) {
if (la.kind == 76 || la.kind == 77) {
ImpliesOp();
x = t;
Expand Down Expand Up @@ -1927,7 +1929,7 @@ void EquivOp() {
void LogicalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(22)) {
if (StartOf(23)) {
if (la.kind == 80 || la.kind == 81) {
AndOp();
x = t;
Expand Down Expand Up @@ -1973,7 +1975,7 @@ void ExpliesOp() {
void RelationalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
BvTerm(out e0);
if (StartOf(23)) {
if (StartOf(24)) {
RelOp(out x, out op);
BvTerm(out e1);
e0 = Expr.Binary(x, op, e0, e1);
Expand Down Expand Up @@ -2072,7 +2074,7 @@ void Term(out Expr/*!*/ e0) {
void Factor(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
Power(out e0);
while (StartOf(24)) {
while (StartOf(25)) {
MulOp(out x, out op);
Power(out e1);
e0 = Expr.Binary(x, op, e0, e1);
Expand Down Expand Up @@ -2145,7 +2147,7 @@ void UnaryExpression(out Expr/*!*/ e) {
x = t;
UnaryExpression(out e);
e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(25)) {
} else if (StartOf(26)) {
CoercionExpression(out e);
} else SynErr(163);
}
Expand Down Expand Up @@ -2197,8 +2199,8 @@ void ArrayExpression(out Expr/*!*/ e) {
x = t; allArgs = new List<Expr> ();
allArgs.Add(e);
store = false; bvExtract = false;
if (StartOf(26)) {
if (StartOf(19)) {
if (StartOf(27)) {
if (StartOf(20)) {
Expression(out index0);
if (index0 is BvBounds)
bvExtract = true;
Expand Down Expand Up @@ -2363,7 +2365,7 @@ void AtomExpression(out Expr/*!*/ e) {
id = new IdentifierExpr(x, x.val); e = id;
if (la.kind == 11) {
Get();
if (StartOf(19)) {
if (StartOf(20)) {
Expressions(out es);
e = new NAryExpr(x, new FunctionCall(id), es);
} else if (la.kind == 12) {
Expand Down Expand Up @@ -2402,7 +2404,7 @@ void AtomExpression(out Expr/*!*/ e) {
}
case 11: {
Get();
if (StartOf(19)) {
if (StartOf(20)) {
Expression(out e);
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds are not allowed");
Expand Down Expand Up @@ -2617,7 +2619,7 @@ void SpecBlock(out Block/*!*/ b) {

Ident(out x);
Expect(13);
while (StartOf(18)) {
while (StartOf(19)) {
LabelOrCmd(out c, out label);
Contract.Assert(c == null || label == null);
if (c != null) {
Expand Down Expand Up @@ -2666,7 +2668,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
Get();
Ident(out id);
parameters = new List<object/*!*/>();
if (StartOf(19)) {
if (StartOf(20)) {
AttributeParameter(out param);
parameters.Add(param);
while (la.kind == 14) {
Expand Down Expand Up @@ -2694,7 +2696,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
}
}

} else if (StartOf(19)) {
} else if (StartOf(20)) {
Expression(out e);
es = new List<Expr> { e };
while (la.kind == 14) {
Expand All @@ -2720,7 +2722,7 @@ void AttributeParameter(out object/*!*/ o) {
if (la.kind == 4) {
Get();
o = t.val.Substring(1, t.val.Length-2);
} else if (StartOf(19)) {
} else if (StartOf(20)) {
Expression(out e);
o = e;
} else SynErr(177);
Expand Down Expand Up @@ -2776,6 +2778,7 @@ public void Parse() {
{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
{_x,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
{_x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x},
Expand Down
Loading

0 comments on commit e8b5158

Please sign in to comment.