Skip to content

Commit

Permalink
Merge pull request #128 from smackers/update-boogie
Browse files Browse the repository at this point in the history 
Update boogie
  • Loading branch information
@akashlal
akashlal authored Sep 15, 2020
2 parents 9b11c40 + 8663135 commit 958fbb6
Show file tree
Hide file tree
Showing 40 changed files with 102 additions and 107 deletions.
2 changes: 1 addition & 1 deletion boogie
Submodule boogie updated 464 files
2 changes: 1 addition & 1 deletion cba-NetCore.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@

<ItemGroup>
<ProjectReference Include="boogie\Source\AbsInt\AbsInt-NetCore.csproj" />
<ProjectReference Include="boogie\Source\Basetypes\Basetypes-NetCore.csproj" />
<ProjectReference Include="boogie\Source\BaseTypes\BaseTypes-NetCore.csproj" />
<ProjectReference Include="boogie\Source\CodeContractsExtender\CodeContractsExtender-NetCore.csproj" />
<ProjectReference Include="boogie\Source\Concurrency\Concurrency-NetCore.csproj" />
<ProjectReference Include="boogie\Source\Core\Core-NetCore.csproj" />
Expand Down
6 changes: 3 additions & 3 deletions cba.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,9 +108,9 @@
<Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>
<Name>AbsInt</Name>
</ProjectReference>
<ProjectReference Include="boogie\Source\Basetypes\Basetypes.csproj">
<ProjectReference Include="boogie\Source\BaseTypes\BaseTypes.csproj">
<Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
<Name>Basetypes</Name>
<Name>BaseTypes</Name>
</ProjectReference>
<ProjectReference Include="boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj">
<Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>
Expand Down Expand Up @@ -215,4 +215,4 @@
<PostBuildEvent>
</PostBuildEvent>
</PropertyGroup>
</Project>
</Project>
2 changes: 1 addition & 1 deletion cba.sln
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "boogie", "boogie", "{247E7F
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "boogie\Source\AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Basetypes", "boogie\Source\Basetypes\Basetypes.csproj", "{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}"
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "boogie\Source\BaseTypes\BaseTypes.csproj", "{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}"
EndProject
Expand Down
2 changes: 1 addition & 1 deletion source/BctCleanup/BctCleanup-NetCore.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

<ItemGroup>
<ProjectReference Include="..\..\boogie\Source\AbsInt\AbsInt-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\Basetypes\Basetypes-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\Core\Core-NetCore.csproj" />
Expand Down
4 changes: 2 additions & 2 deletions source/BctCleanup/BctCleanup.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,9 +65,9 @@
<Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>
<Name>AbsInt</Name>
</ProjectReference>
<ProjectReference Include="..\..\boogie\Source\Basetypes\Basetypes.csproj">
<ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj">
<Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
<Name>Basetypes</Name>
<Name>BaseTypes</Name>
</ProjectReference>
<ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj">
<Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>
Expand Down
2 changes: 1 addition & 1 deletion source/BctCleanup/Driver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ private static void addInitializersToMain(Program prog, string mainProcName)
List<AssignLhs> lhss = new List<AssignLhs>();
lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(trackVariable)));
List<Expr> rhss = new List<Expr>();
rhss.Add(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.ZERO));
rhss.Add(new LiteralExpr(Token.NoToken, Microsoft.BaseTypes.BigNum.ZERO));
newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
}

Expand Down
2 changes: 1 addition & 1 deletion source/BctCleanup/app.config
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<runtime>
<assemblyBinding xmlns="urn:schemas-microsoft-com:asm.v1">
<dependentAssembly>
<assemblyIdentity name="Basetypes" publicKeyToken="736440C9B414EA16" culture="neutral"/>
<assemblyIdentity name="BaseTypes" publicKeyToken="736440C9B414EA16" culture="neutral"/>
<bindingRedirect oldVersion="0.0.0.0-2.2.30705.1126" newVersion="2.2.30705.1126"/>
</dependentAssembly>
<dependentAssembly>
Expand Down
6 changes: 3 additions & 3 deletions source/ConstLoop.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -439,8 +439,8 @@ private HashSet<string> FindConstantLoops(IEnumerable<Implementation> candidates
var ua_old = CommandLineOptions.Clo.UseArrayTheory;
CommandLineOptions.Clo.UseArrayTheory = true;

var to = CommandLineOptions.Clo.ProverKillTime;
CommandLineOptions.Clo.ProverKillTime = 5;
var to = CommandLineOptions.Clo.TimeLimit;
CommandLineOptions.Clo.TimeLimit = 5;

// verify
BoogieVerify.Verify(outProg, true, out allErrors, out timeOuts);
Expand Down Expand Up @@ -475,7 +475,7 @@ private HashSet<string> FindConstantLoops(IEnumerable<Implementation> candidates
// Reset options
CommandLineOptions.Clo.UseArrayTheory = ua_old;

CommandLineOptions.Clo.ProverKillTime = to;
CommandLineOptions.Clo.TimeLimit = to;

return ret;
}
Expand Down
10 changes: 5 additions & 5 deletions source/CoreLib/AbstractHoudini.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ public AbstractHoudini(Program program)
this.name2Impl = BoogieUtil.nameImplMapping(program);

this.vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List<Checker>());
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit);
this.reporter = new AbstractHoudiniErrorReporter();

var impls = new List<Implementation>(
Expand Down Expand Up @@ -443,7 +443,7 @@ public VCExpr GetSummaryExpr(Dictionary<string, VCExpr> incarnations, VCExpressi
continue;

var vexpr = VCExpressionGenerator.False;
consts.Iter(c => vexpr = gen.OrSimp(vexpr, gen.Eq(incarnations[v.Name], gen.Integer(Microsoft.Basetypes.BigNum.FromInt(c)))));
consts.Iter(c => vexpr = gen.OrSimp(vexpr, gen.Eq(incarnations[v.Name], gen.Integer(Microsoft.BaseTypes.BigNum.FromInt(c)))));
ret = gen.AndSimp(ret, vexpr);
}

Expand Down Expand Up @@ -592,7 +592,7 @@ private object ToValue(Model.Element elem)
{
if (elem is Model.Integer)
{
return Microsoft.Basetypes.BigNum.FromInt((elem as Model.Integer).AsInt());
return Microsoft.BaseTypes.BigNum.FromInt((elem as Model.Integer).AsInt());
}
if (elem is Model.Boolean)
{
Expand All @@ -617,9 +617,9 @@ private VCExpr ToVcExpr(Expr expr, Dictionary<string, VCExpr> incarnations, VCEx
return VCExpressionGenerator.False;
}
}
else if (val is Microsoft.Basetypes.BigNum)
else if (val is Microsoft.BaseTypes.BigNum)
{
return gen.Integer((Microsoft.Basetypes.BigNum)val);
return gen.Integer((Microsoft.BaseTypes.BigNum)val);
}

throw new NotImplementedException("Cannot handle literals of this type");
Expand Down
6 changes: 3 additions & 3 deletions source/CoreLib/BoogiePP.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ public static Expr assumeGt(Variable v1, int c)
{
var args = new List<Expr>();
args.Add(Expr.Ident(v1));
args.Add(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(c), 32));
args.Add(new LiteralExpr(Token.NoToken, Microsoft.BaseTypes.BigNum.FromInt(c), 32));

return new NAryExpr(Token.NoToken,
new FunctionCall(getBvGt()), args);
Expand All @@ -160,7 +160,7 @@ public static Expr assumeGt(Variable v1, int c)
public static LiteralExpr getLiteral(int c)
{
if (useIntArithmetic) return Expr.Literal(c);
return new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(c), 32);
return new LiteralExpr(Token.NoToken, Microsoft.BaseTypes.BigNum.FromInt(c), 32);
}

public static Expr increment(Variable v1)
Expand All @@ -173,7 +173,7 @@ public static Expr increment(Variable v1)
{
var args = new List<Expr>();
args.Add(Expr.Ident(v1));
args.Add(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1), 32));
args.Add(new LiteralExpr(Token.NoToken, Microsoft.BaseTypes.BigNum.FromInt(1), 32));

return new NAryExpr(Token.NoToken,
new FunctionCall(getBvAdd()), args);
Expand Down
4 changes: 2 additions & 2 deletions source/CoreLib/BoogieVerify.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,10 +42,10 @@ public enum ReturnStatus { OK, NOK, ReachedBound };

public static void setTimeOut(int TO)
{
CommandLineOptions.Clo.ProverKillTime = -1;
CommandLineOptions.Clo.TimeLimit = 0;
if (TO > 0)
{
CommandLineOptions.Clo.ProverKillTime = TO;
CommandLineOptions.Clo.TimeLimit = TO;
}
}

Expand Down
2 changes: 1 addition & 1 deletion source/CoreLib/CBAPasses.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -693,7 +693,7 @@ public void VisitImplementation(Implementation impl)

var uniqueId = useGlobalCounter ? counter : cnt[cc.callee];
var attr = new List<object>();
attr.Add(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(uniqueId)));
attr.Add(new LiteralExpr(Token.NoToken, Microsoft.BaseTypes.BigNum.FromInt(uniqueId)));

cc.Attributes = BoogieUtil.removeAttr("si_old_unique_call", cc.Attributes);
var oldAttr = BoogieUtil.getAttr("si_unique_call", cc.Attributes);
Expand Down
8 changes: 4 additions & 4 deletions source/CoreLib/ConcurrentTrace.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -282,11 +282,11 @@ public static bool getSourceInfo(Cmd cmd, out string file, out int line, out int
{
file = attr[0] as string;
var tt = attr[1] as LiteralExpr;
if (tt != null && (tt.Val is Microsoft.Basetypes.BigNum))
line = ((Microsoft.Basetypes.BigNum)(tt.Val)).ToInt;
if (tt != null && (tt.Val is Microsoft.BaseTypes.BigNum))
line = ((Microsoft.BaseTypes.BigNum)(tt.Val)).ToInt;
tt = attr[2] as LiteralExpr;
if (tt != null && (tt.Val is Microsoft.Basetypes.BigNum))
column = ((Microsoft.Basetypes.BigNum)(tt.Val)).ToInt;
if (tt != null && (tt.Val is Microsoft.BaseTypes.BigNum))
column = ((Microsoft.BaseTypes.BigNum)(tt.Val)).ToInt;

}
else
Expand Down
2 changes: 1 addition & 1 deletion source/CoreLib/CoreLib-NetCore.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

<ItemGroup>
<ProjectReference Include="..\..\boogie\Source\AbsInt\AbsInt-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\Basetypes\Basetypes-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency-NetCore.csproj" />
<ProjectReference Include="..\..\boogie\Source\Core\Core-NetCore.csproj" />
Expand Down
4 changes: 2 additions & 2 deletions source/CoreLib/CoreLib.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,9 +113,9 @@
<Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>
<Name>AbsInt</Name>
</ProjectReference>
<ProjectReference Include="..\..\boogie\Source\Basetypes\Basetypes.csproj">
<ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj">
<Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
<Name>Basetypes</Name>
<Name>BaseTypes</Name>
</ProjectReference>
<ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj">
<Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>
Expand Down
6 changes: 3 additions & 3 deletions source/CoreLib/Coverage.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,13 +55,13 @@ public override CBAProgram runCBAPass(CBAProgram p)
procsNotCovered.Remove(p.mainProcName);

// Iterate and gather procedures that can be reached
int oldProverLimit = CommandLineOptions.Clo.ProverCCLimit;
int oldErrorLimit = CommandLineOptions.Clo.ErrorLimit;

var done = false;
do
{
// Set the number of traces returned by boogie in one shot
CommandLineOptions.Clo.ProverCCLimit = procsNotCovered.Count();
CommandLineOptions.Clo.ErrorLimit = procsNotCovered.Count();

var covered = iterateComputation(input as PersistentCBAProgram, procsNotCovered);
if (covered.Count == 0)
Expand All @@ -78,7 +78,7 @@ public override CBAProgram runCBAPass(CBAProgram p)
}
} while (!done);

CommandLineOptions.Clo.ProverCCLimit = oldProverLimit;
CommandLineOptions.Clo.ErrorLimit = oldErrorLimit;

return null;
}
Expand Down
2 changes: 1 addition & 1 deletion source/CoreLib/ErrorProjection.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ public HashSet<string> iterateComputation(PersistentCBAProgram program, HashSet<
// instrument() sets labelProcMap
var newProg = instrument(program, candidates);

CommandLineOptions.Clo.ProverCCLimit = 5;
CommandLineOptions.Clo.ErrorLimit = 5;
var verifier = getVerifier();
verifier.run(newProg);

Expand Down
22 changes: 11 additions & 11 deletions source/CoreLib/ErrorTrace.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1062,9 +1062,9 @@ public void addVal(string var, object val)
{
if (var == "k" || var == LanguageSemantics.tidName)
{
if (val is Microsoft.Basetypes.BigNum)
if (val is Microsoft.BaseTypes.BigNum)
{
val = BoogieUtil.BigNumToIntForce((Microsoft.Basetypes.BigNum)val);
val = BoogieUtil.BigNumToIntForce((Microsoft.BaseTypes.BigNum)val);
}
}

Expand All @@ -1089,7 +1089,7 @@ public int getIntVal(string var)
var val = getVal(var);
if (val is int) return (int)val;
if (val is Model.Integer) return ((Model.Integer)val).AsInt();
if (val is Microsoft.Basetypes.BigNum) return BoogieUtil.BigNumToIntForce((Microsoft.Basetypes.BigNum)val);
if (val is Microsoft.BaseTypes.BigNum) return BoogieUtil.BigNumToIntForce((Microsoft.BaseTypes.BigNum)val);
Debug.Assert(false);
return 0;
}
Expand All @@ -1103,14 +1103,14 @@ public bool getBoolVal(string var)
return false;
}

public Microsoft.Basetypes.BigNum getBigNumVal(string var)
public Microsoft.BaseTypes.BigNum getBigNumVal(string var)
{
var val = getVal(var);
if (val is int) return Microsoft.Basetypes.BigNum.FromInt((int)val);
if (val is Model.Integer) return Microsoft.Basetypes.BigNum.FromString(((Model.Integer)val).Numeral);
if (val is Microsoft.Basetypes.BigNum) return (Microsoft.Basetypes.BigNum)val;
if (val is int) return Microsoft.BaseTypes.BigNum.FromInt((int)val);
if (val is Model.Integer) return Microsoft.BaseTypes.BigNum.FromString(((Model.Integer)val).Numeral);
if (val is Microsoft.BaseTypes.BigNum) return (Microsoft.BaseTypes.BigNum)val;
Debug.Assert(false);
return Microsoft.Basetypes.BigNum.FromInt(0);
return Microsoft.BaseTypes.BigNum.FromInt(0);
}


Expand All @@ -1124,7 +1124,7 @@ public bool hasIntVar(string var)
if (!hasVar(var)) return false;
var v = varToVal[var];
return ((v is int) || (v is Microsoft.Boogie.Model.Integer) ||
(v is Microsoft.Basetypes.BigNum));
(v is Microsoft.BaseTypes.BigNum));
}

public bool hasBoolVar(string var)
Expand Down Expand Up @@ -1767,8 +1767,8 @@ private static void printInfo(Cmd cmd, InstrInfo info, string procName)
{
file = attr[0] as string;
var tt = attr[1] as LiteralExpr;
if (tt != null && (tt.Val is Microsoft.Basetypes.BigNum))
line = ((Microsoft.Basetypes.BigNum)(tt.Val)).ToInt;
if (tt != null && (tt.Val is Microsoft.BaseTypes.BigNum))
line = ((Microsoft.BaseTypes.BigNum)(tt.Val)).ToInt;
}
else
{
Expand Down
2 changes: 1 addition & 1 deletion source/CoreLib/Instrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1499,7 +1499,7 @@ private CallCmd ContextSwitchCmd(Implementation impl, string blockName, int inst
var ret = ContextSwitchCmd();
// {:cs_location int}
var param = new List<object>();
param.Add(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(getNewCSLocation())));
param.Add(new LiteralExpr(Token.NoToken, Microsoft.BaseTypes.BigNum.FromInt(getNewCSLocation())));
var attr = new QKeyValue(Token.NoToken, "cs_location", param, null);

ret.Attributes = attr;
Expand Down
8 changes: 4 additions & 4 deletions source/CoreLib/StratifiedInlining.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1191,9 +1191,9 @@ public Outcome Fwd(HashSet<StratifiedCallSite> openCallSites, StratifiedInlining
while (true)
{
// Check timeout
if (CommandLineOptions.Clo.ProverKillTime != -1)
if (CommandLineOptions.Clo.TimeLimit != 0)
{
if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.TimeLimit)
{
return Outcome.TimedOut;
}
Expand Down Expand Up @@ -1484,7 +1484,7 @@ void MustFail(StratifiedVC svc)
{
if (cba.Util.BoogieVerify.assertsPassedIsInt)
{
Microsoft.Basetypes.BigNum zero = Microsoft.Basetypes.BigNum.FromInt(0);
Microsoft.BaseTypes.BigNum zero = Microsoft.BaseTypes.BigNum.FromInt(0);
prover.Assert(prover.VCExprGen.Eq(svc.interfaceExprVars[index], prover.VCExprGen.Integer(zero)), b);
}
else
Expand All @@ -1507,7 +1507,7 @@ void MustNotFail(StratifiedCallSite scs, StratifiedVC svc)
VCExpr assertsPass = null;
if (cba.Util.BoogieVerify.assertsPassedIsInt)
{
Microsoft.Basetypes.BigNum zero = Microsoft.Basetypes.BigNum.FromInt(0);
Microsoft.BaseTypes.BigNum zero = Microsoft.BaseTypes.BigNum.FromInt(0);
assertsPass = prover.VCExprGen.Eq(scs.interfaceExprs[index], prover.VCExprGen.Integer(zero));
}
else
Expand Down
Loading

0 comments on commit 958fbb6

Please sign in to comment.