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

Jump to bottom

Sync with Boogie 2.15.7 #160

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Sync with Boogie 2.15.7 #160

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
205d3d3
First Attempt
Aug 3, 2022
e9e2c9e
Fix loop extraction
Aug 3, 2022
6e0a36b
Bug fixes dealing with new Boogie APIs
akashlal Aug 6, 2022
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 .github/workflows/release.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ on:

env:
SOLUTION: source/Corral.sln
BOOGIESOLUTION: boogie/Source/Boogie.sln

jobs:
job0:
Expand All @@ -29,6 +30,8 @@ jobs:
cd $GITHUB_WORKSPACE
# Restore dotnet tools
dotnet tool restore
# Build custom Boogie
dotnet build ${BOOGIESOLUTION}
# Build Corral
dotnet build -p:Version=$VERSION -c Release ${SOLUTION}
# Create packages
Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ on: [push, pull_request, workflow_dispatch]

env:
SOLUTION: source/Corral.sln
BOOGIESOLUTION: boogie/Source/Boogie.sln
Z3URL: https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip

jobs:
Expand Down Expand Up @@ -32,6 +33,8 @@ jobs:
cd $GITHUB_WORKSPACE
# Restore dotnet tools
dotnet tool restore
# Build custom Boogie
dotnet build ${BOOGIESOLUTION}
# Build Corral
dotnet build -c ${{ matrix.configuration }} ${SOLUTION}
# Run regression tests
Expand Down
Binary file modified .gitignore
View file
Open in desktop
Binary file not shown.
4 changes: 4 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
[submodule "boogie"]
path = boogie
url = https://github.com/Dargones/boogie.git
branch = SyncWithCorral
1 change: 1 addition & 0 deletions boogie
Open in desktop
Submodule boogie added at 9c7cde
19 changes: 11 additions & 8 deletions source/CoreLib/AbstractHoudini.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,10 @@
using Bpl = Microsoft.Boogie;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using System.IO;
using System.Threading;
using Microsoft.Boogie.GraphUtil;
using Microsoft.Boogie.SMTLib;

namespace CoreLib {

Expand Down Expand Up @@ -48,8 +51,9 @@ public AbstractHoudini(Program program)
this.impl2Summary = new Dictionary<string, ISummaryElement>();
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.TimeLimit);
var checkerPool = new CheckerPool(CommandLineOptions.Clo);
this.vcgen = new VCGen(program, checkerPool);
this.prover = ProverInterface.CreateProver(CommandLineOptions.Clo, program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit);
this.reporter = new AbstractHoudiniErrorReporter();

var impls = new List<Implementation>(
Expand Down Expand Up @@ -180,8 +184,7 @@ private bool ProcessImpl(Implementation impl)

//Console.WriteLine("Checking: {0}", vc);

prover.BeginCheck(impl.Name, vc, reporter);
ProverInterface.Outcome proverOutcome = prover.CheckOutcome(reporter);
ProverInterface.Outcome proverOutcome= prover.Check(impl.Name, vc, reporter, 1, CancellationToken.None).Result;
if (reporter.model == null)
break;

Expand Down Expand Up @@ -312,13 +315,13 @@ private void attachEnsures(Implementation impl)
private void GenVC(Implementation impl)
{
ModelViewInfo mvInfo;
Dictionary<int, Absy> label2absy;
ControlFlowIdMap<Absy> label2absy = new ControlFlowIdMap<Absy>();

vcgen.ConvertCFG2DAG(impl);
vcgen.PassifyImpl(impl, out mvInfo);
vcgen.PassifyImpl(new ImplementationRun(impl, TextWriter.Null), out mvInfo);

var gen = prover.VCExprGen;
var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context);
var vcexpr = vcgen.GenerateVC(impl, null, label2absy, prover.Context);

// Create a macro so that the VC can sit with the theorem prover
Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));
Expand Down Expand Up @@ -803,7 +806,7 @@ class AbstractHoudiniErrorReporter : ProverInterface.ErrorHandler
{
public Model model;

public AbstractHoudiniErrorReporter()
public AbstractHoudiniErrorReporter(): base(CommandLineOptions.Clo)
{
model = null;
}
Expand Down
18 changes: 11 additions & 7 deletions source/CoreLib/BoogieVerify.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
//using BoogiePL;
using System.Diagnostics.Contracts;
using System.IO;
using System.Threading;
using VC;
using cba.Util;

Expand Down Expand Up @@ -116,7 +117,8 @@ public static ReturnStatus Verify(Program program,
CommandLineOptions.Clo.RecursionBound = BoogieVerify.irreducibleLoopUnroll;

// Do loop extraction
var extractionInfo = program.ExtractLoops();
var extractionInfo = LoopExtractor
.ExtractLoops(CommandLineOptions.Clo, program).loops;

// restore RB
CommandLineOptions.Clo.RecursionBound = rb;
Expand Down Expand Up @@ -191,7 +193,9 @@ public static ReturnStatus Verify(Program program,
{
var start = DateTime.Now;

outcome = vcgen.VerifyImplementation(impl, out errors);
var verificationResult = vcgen.VerifyImplementation(new ImplementationRun(impl, TextWriter.Null), CancellationToken.None).Result;
outcome = verificationResult.Item1;
errors = verificationResult.errors;

var end = DateTime.Now;

Expand Down Expand Up @@ -242,7 +246,7 @@ public static ReturnStatus Verify(Program program,
Log.WriteLine(Log.Debug, outcome.ToString());

Log.WriteLine(Log.Debug, (errors == null ? 0 : errors.Count) + " counterexamples.");
if (errors != null) ret = ReturnStatus.NOK;
if (errors != null && errors.Count > 0) ret = ReturnStatus.NOK;

// Print model
if (errors != null && errors.Count > 0 && errors[0].Model != null && CommandLineOptions.Clo.ModelViewFile != null)
Expand Down Expand Up @@ -272,7 +276,7 @@ public static ReturnStatus Verify(Program program,
// Map the trace across loop extraction
if (vcgen is VC.VCGen)
{
errors[i] = (vcgen as VC.VCGen).extractLoopTrace(errors[i], impl.Name, program, extractionInfo);
errors[i] = (vcgen as VC.VCGen).ExtractLoopTrace(errors[i], impl.Name, program, extractionInfo);
}

if (errors[i] is AssertCounterexample)
Expand Down Expand Up @@ -626,7 +630,7 @@ public static Counterexample ReconstructTrace(Counterexample trace, string currP
{
// find the corresponding call in origBlock
var calleeInfo = trace.calleeCounterexamples[currLocation];
var calleeName = trace.getCalledProcName(trace.Trace[currLocation.numBlock].Cmds[currLocation.numInstr]);
var calleeName = trace.GetCalledProcName(trace.Trace[currLocation.numBlock].Cmds[currLocation.numInstr]);
while (currOrigInstr < currOrigBlock.Cmds.Count)
{
var cmd = currOrigBlock.Cmds[currOrigInstr] as CallCmd;
Expand All @@ -649,7 +653,7 @@ public static Counterexample ReconstructTrace(Counterexample trace, string currP
break;
}

var ret = new AssertCounterexample(newTrace, null, null, trace.Model, trace.MvInfo, trace.Context);
var ret = new AssertCounterexample(CommandLineOptions.Clo, newTrace, null, null, trace.Model, trace.MvInfo, trace.Context, null);
ret.calleeCounterexamples = newTraceCallees;

return ret;
Expand Down Expand Up @@ -703,7 +707,7 @@ public static void ReconstructImperativeTrace(Counterexample trace, string currP
if (trace.calleeCounterexamples.ContainsKey(loc))
{
Cmd c = b.Cmds[numInstr];
var calleeName = trace.getCalledProcName(c);
var calleeName = trace.GetCalledProcName(c);
var calleeTrace = trace.calleeCounterexamples[loc].counterexample;
ReconstructImperativeTrace(calleeTrace, calleeName, origProg);
calleeTraces.Add(
Expand Down
11 changes: 7 additions & 4 deletions source/CoreLib/CBAPasses.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1120,16 +1120,19 @@ public override CBAProgram runCBAPass(CBAProgram p)

foreach (var impl in BoogieUtil.GetImplementations(p))
{
impl.PruneUnreachableBlocks();
impl.PruneUnreachableBlocks(CommandLineOptions.Clo);
}

// save RB
var rb = CommandLineOptions.Clo.RecursionBound;
if (BoogieVerify.irreducibleLoopUnroll >= 0)
CommandLineOptions.Clo.RecursionBound = BoogieVerify.irreducibleLoopUnroll;

var procsWithIrreducibleLoops = new HashSet<string>();
var passInfo = p.ExtractLoops(out procsWithIrreducibleLoops);

var loopExtractionResult = LoopExtractor.ExtractLoops(CommandLineOptions.Clo, p);
var passInfo = loopExtractionResult.loops;
var procsWithIrreducibleLoops =
loopExtractionResult.procsWithIrreducibleLoops
.Select(implementation => implementation.Name).ToHashSet();

// restore RB
CommandLineOptions.Clo.RecursionBound = rb;
Expand Down
12 changes: 6 additions & 6 deletions source/CoreLib/CompilerPass.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ public static string mergeRecCalls(Implementation impl)
.Iter(cc =>
{
var str = new System.IO.StringWriter();
var tt = new TokenTextWriter(str);
var tt = new TokenTextWriter(str, CommandLineOptions.Clo);
cc.Emit(tt, 0);
tt.Close();
callStr.Add(str.ToString());
Expand Down Expand Up @@ -538,9 +538,9 @@ public override CBAProgram runCBAPass(CBAProgram p)
// Type information is needed in some cases. For instance, the Command
// Mem[x] := untracked-expr is converted to havoc temp; Mem[x] := temp. Here
// we need the type of "untracked-expr" or of "Mem[x]"
if (p.Typecheck() != 0)
if (p.Typecheck(CommandLineOptions.Clo) != 0)
{
p.Emit(new TokenTextWriter("error.bpl"));
p.Emit(new TokenTextWriter("error.bpl", CommandLineOptions.Clo));
throw new InternalError("Type errors");
}
vslice.VisitProgram(p as Program);
Expand Down Expand Up @@ -712,9 +712,9 @@ private void doInlining(CBAProgram p)
foreach (Declaration d in TopLevelDeclarations)
{
Implementation impl = d as Implementation;
if (impl != null && !impl.SkipVerification)
if (impl != null && !impl.IsSkipVerification(CommandLineOptions.Clo))
{
Inliner.ProcessImplementation(p as Program, impl);
Inliner.ProcessImplementation(CommandLineOptions.Clo, p, impl);
}
}
foreach (Declaration d in TopLevelDeclarations)
Expand Down Expand Up @@ -766,7 +766,7 @@ public static void InlineToDepth(Program program)
}
foreach (Implementation impl in impls)
{
Inliner.ProcessImplementationForHoudini(program, impl);
Inliner.ProcessImplementationForHoudini(CommandLineOptions.Clo, program, impl);
}
foreach (Implementation impl in impls)
{
Expand Down
2 changes: 1 addition & 1 deletion source/CoreLib/ConcurrentTrace.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,7 @@ public static void printCTrace(PersistentCBAProgram program, ErrorTrace trace, s
private static void setupPrint(PersistentCBAProgram program, ErrorTrace trace, string file)
{
// Set output files
pathFile = file == null ? null : new TokenTextWriter(file + "_trace.txt");
pathFile = file == null ? null : new TokenTextWriter(file + "_trace.txt", CommandLineOptions.Clo);
if(pathFile != null) program.writeToFile(file + ".bpl");
Program prog = program.getProgram();

Expand Down
22 changes: 11 additions & 11 deletions source/CoreLib/ErrorTrace.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1327,7 +1327,7 @@ public static void PrintStackTrace(Program p, ErrorTrace trace, string filename)
stack = new List<PrintProgramPath.WorkItem>();
program = p;
nameImplMap = BoogieUtil.nameImplMapping(program);
pathFile = new TokenTextWriter(filename);
pathFile = new TokenTextWriter(filename, CommandLineOptions.Clo);
gcnt = 1;
abortMessage = null;

Expand Down Expand Up @@ -1506,8 +1506,8 @@ public static void Print(Program p, ErrorTrace trace, HashSet<string> recorded,
{
program = p;
nameImplMap = BoogieUtil.nameImplMapping(program);
pathFile = new TokenTextWriter(filename);
stackFile = new TokenTextWriter(stackFileName);
pathFile = new TokenTextWriter(filename, CommandLineOptions.Clo);
stackFile = new TokenTextWriter(stackFileName, CommandLineOptions.Clo);
gcnt = 1;
abortMessage = null;
abortMessageLocation = null;
Expand Down Expand Up @@ -1544,7 +1544,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet<string> recorded,

if (scalarWrites.Count > 0)
{
var scalarFile = new TokenTextWriter("scalars.txt");
var scalarFile = new TokenTextWriter("scalars.txt", CommandLineOptions.Clo);
scalarWrites.Iter(kvp =>
{
scalarFile.Write("{0}: ", kvp.Key);
Expand Down Expand Up @@ -1575,7 +1575,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet<string> recorded,
memWrites.Iter(kvp =>
kvp.Value.Iter(line => lineWrites.InitAndAdd(line, kvp.Key)));

var memFile = new TokenTextWriter("mem1.txt");
var memFile = new TokenTextWriter("mem1.txt", CommandLineOptions.Clo);

var lines = new HashSet<string>();
lineReads.Keys.Iter(line => lines.Add(line));
Expand All @@ -1592,7 +1592,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet<string> recorded,

memFile.Close();

memFile = new TokenTextWriter("mem2.txt");
memFile = new TokenTextWriter("mem2.txt", CommandLineOptions.Clo);

var addresses = new HashSet<int>();
memReads.Keys.Iter(a => addresses.Add(a));
Expand All @@ -1619,7 +1619,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet<string> recorded,
memWritesCS.Iter(kvp =>
kvp.Value.Iter(cs => stateWrites.InitAndAdd(cs, kvp.Key)));

memFile = new TokenTextWriter("mem3.txt");
memFile = new TokenTextWriter("mem3.txt", CommandLineOptions.Clo);

var states = new HashSet<int>();
stateReads.Keys.Iter(s => states.Add(s));
Expand All @@ -1636,7 +1636,7 @@ public static void Print(Program p, ErrorTrace trace, HashSet<string> recorded,

memFile.Close();

memFile = new TokenTextWriter("mem4.txt");
memFile = new TokenTextWriter("mem4.txt", CommandLineOptions.Clo);

foreach (var add in addresses)
{
Expand Down Expand Up @@ -1924,7 +1924,7 @@ public static void print(PersistentProgram program, ErrorTrace trace, string fil
private static void setupPrint(PersistentProgram program, ErrorTrace trace, string file)
{
// Set output files
pathFile = new TokenTextWriter(file + "_trace.txt");
pathFile = new TokenTextWriter(file + "_trace.txt", CommandLineOptions.Clo);
program.writeToFile(file + ".bpl");
Program prog = program.getProgram();

Expand Down Expand Up @@ -2049,7 +2049,7 @@ public class InlineToTrace : Inliner
private static Stack<Dictionary<int, ErrorTrace>> traceStack = new Stack<Dictionary<int, ErrorTrace>>();

public InlineToTrace(Program program, InlineCallback cb)
:base(program, cb, -1)
:base(program, cb, -1, CommandLineOptions.Clo)
{ }

// Return callCmd -> callee trace
Expand Down Expand Up @@ -2112,7 +2112,7 @@ public static void Inline(Program program, ErrorTrace trace)
var inliner = new InlineToTrace(program, null);

traceStack.Push(FindCallsOnTrace(entryPoint, trace));
Inliner.ProcessImplementation(program, entryPoint, inliner);
Inliner.ProcessImplementation(CommandLineOptions.Clo, program, entryPoint);

foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
{
Expand Down
Loading