Skip to content

Commit

Permalink
Remove labels and unused VC generation code (#201)
Browse files Browse the repository at this point in the history 
* first checkin

* removed labels entirely

* removed references to Doomed
disabled doomed tests

* updated golden outputs

* disabled these tests

* updated golden outputs

* Do not parse prover options just for printing help

* calculate path only if a model exists

* check if there are prover warnings before processing model

* Revert "updated golden outputs"

This reverts commit b9e3aba.

* Revert "updated golden outputs"

This reverts commit 35c39dd.

* fixed a few golden outputs (all except the ones that use MUlTI_TRACES)

* eliminated MULTI_TRACES which was done using labels and updated golden outputs

* removed /vc: option

* remove doomed code and tests

* removed doomed related command line options

Co-authored-by: Bernhard Kragl <[email protected]>
  • Loading branch information
@shazqadeer @bkragl
shazqadeer and bkragl authored Feb 19, 2020
1 parent a2a2597 commit 55baa23
Show file tree
Hide file tree
Showing 65 changed files with 225 additions and 5,026 deletions.
2 changes: 0 additions & 2 deletions Source/Boogie-NetCore.sln
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini-NetCore", "Houdini\
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Predication-NetCore", "Predication\Predication-NetCore.csproj", "{7A4B3721-D902-4265-94DB-CA8B0BB295B7}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed-NetCore", "Doomed\Doomed-NetCore.csproj", "{CE190976-D727-4038-8D8A-8C5579E48CCF}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine-NetCore", "ExecutionEngine\ExecutionEngine-NetCore.csproj", "{51768B2E-FFF9-49F0-96D7-022250A4BEB4}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency-NetCore", "Concurrency\Concurrency-NetCore.csproj", "{4AC86856-E985-4DBC-B089-20D5B9317A99}"
Expand Down
2 changes: 0 additions & 2 deletions Source/Boogie.sln
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Predication", "Predication\Predication.csproj", "{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed", "Doomed\Doomed.csproj", "{884386A3-58E9-40BB-A273-B24976775553}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "ExecutionEngine\ExecutionEngine.csproj", "{EAA5EB79-D475-4601-A59B-825C191CD25F}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8A05D14E-F2BF-4890-BBE0-D76B18A50797}"
Expand Down
1 change: 0 additions & 1 deletion Source/BoogieDriver/BoogieDriver-NetCore.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
<ProjectReference Include="..\Basetypes\Basetypes-NetCore.csproj" />
<ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender-NetCore.csproj" />
<ProjectReference Include="..\Core\Core-NetCore.csproj" />
<ProjectReference Include="..\Doomed\Doomed-NetCore.csproj" />
<ProjectReference Include="..\ExecutionEngine\ExecutionEngine-NetCore.csproj" />
<ProjectReference Include="..\Graph\Graph-NetCore.csproj" />
<ProjectReference Include="..\Houdini\Houdini-NetCore.csproj" />
Expand Down
4 changes: 0 additions & 4 deletions Source/BoogieDriver/BoogieDriver.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -214,10 +214,6 @@
<Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\Doomed\Doomed.csproj">
<Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>
<Name>Doomed</Name>
</ProjectReference>
<ProjectReference Include="..\ExecutionEngine\ExecutionEngine.csproj">
<Project>{EAA5EB79-D475-4601-A59B-825C191CD25F}</Project>
<Name>ExecutionEngine</Name>
Expand Down
121 changes: 18 additions & 103 deletions Source/Core/CommandLineOptions.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,7 @@ public virtual void AttributeUsage() {
/// </summary>
public virtual void ApplyDefaultOptions() {
}

/// <summary>
/// Parses the command-line arguments "args" into the global flag variables. Returns true
/// if there were no errors.
Expand Down Expand Up @@ -413,14 +413,12 @@ void ObjectInvariant2() {
public string PrintFile = null;
public int PrintUnstructured = 0;
public bool UseBaseNameForFileName = false;
public int DoomStrategy = -1;
public bool DoomRestartTP = false;
public bool PrintDesugarings = false;
public bool PrintLambdaLifting = false;
public bool FreeVarLambdaLifting = false;
public string ProverLogFilePath = null;
public bool ProverLogFileAppend = false;

public bool PrintInstrumented = false;
public bool InstrumentWithAsserts = false;
public string ProverPreamble = null;
Expand Down Expand Up @@ -564,7 +562,6 @@ public enum OwnershipModelOption {
public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
public bool UseArrayTheory = false;
public bool WeakArrayTheory = false;
public bool UseLabels = true;
public bool RunDiagnosticsOnTimeout = false;
public bool TraceDiagnosticsOnTimeout = false;
public int TimeLimitPerAssertionInPercent = 10;
Expand Down Expand Up @@ -599,20 +596,6 @@ public int StepsBeforeWidening
public int TrustLayersUpto = -1;
public int TrustLayersDownto = int.MaxValue;

public enum VCVariety {
Structured,
Block,
Local,
BlockNested,
BlockReach,
BlockNestedReach,
Dag,
DagIterative,
Doomed,
Unspecified
}
public VCVariety vcVariety = VCVariety.Unspecified; // will not be Unspecified after command line has been parsed

public bool RemoveEmptyBlocks = true;
public bool CoalesceBlocks = true;
public bool PruneInfeasibleEdges = true;
Expand Down Expand Up @@ -737,7 +720,7 @@ public enum Inlining {
public int StratifiedInliningVerbose = 0; // verbosity level
public int RecursionBound = 500;
public bool NonUniformUnfolding = false;
public int StackDepthBound = 0;
public int StackDepthBound = 0;
public string inferLeastForUnsat = null;

// Inference mode for fixed point engine
Expand All @@ -749,11 +732,11 @@ public enum FixedPointInferenceMode {
Call
};
public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;

public string PrintFixedPoint = null;

public string PrintConjectures = null;

public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)

public enum TypeEncoding {
Expand Down Expand Up @@ -789,7 +772,7 @@ public IEnumerable<string/*!*/> ProcsToCheck {
}

private List<string/*!*/> procsToCheck = null; // null means "no restriction"

[ContractInvariantMethod]
void ObjectInvariant5() {
Contract.Invariant(cce.NonNullElements(this.procsToCheck, true));
Expand Down Expand Up @@ -890,7 +873,7 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
int val = 1;
if (ps.GetNumericArgument(ref val, 2)) {
PrettyPrint = val == 1;
}
}
return true;

case "CivlDesugaredFile":
Expand Down Expand Up @@ -919,13 +902,13 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
}
return true;

case "proverPreamble":
case "proverPreamble":
if (ps.ConfirmArgumentCount(1))
{
ProverPreamble = args[ps.i];
}
return true;

case "logPrefix":
if (ps.ConfirmArgumentCount(1)) {
string s = cce.NonNull(args[ps.i]);
Expand Down Expand Up @@ -1152,47 +1135,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
}
return true;
}
case "vc":
if (ps.ConfirmArgumentCount(1)) {
switch (args[ps.i]) {
case "s":
case "structured":
vcVariety = VCVariety.Structured;
break;
case "b":
case "block":
vcVariety = VCVariety.Block;
break;
case "l":
case "local":
vcVariety = VCVariety.Local;
break;
case "n":
case "nested":
vcVariety = VCVariety.BlockNested;
break;
case "m":
vcVariety = VCVariety.BlockNestedReach;
break;
case "r":
vcVariety = VCVariety.BlockReach;
break;
case "d":
case "dag":
vcVariety = VCVariety.Dag;
break;
case "i":
vcVariety = VCVariety.DagIterative;
break;
case "doomed":
vcVariety = VCVariety.Doomed;
break;
default:
ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
break;
}
}
return true;

case "proverDll":
if (ps.ConfirmArgumentCount(1)) {
Expand All @@ -1207,28 +1149,18 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
ProverOptions = ProverOptions.Concat1(cce.NonNull(args[ps.i]));
}
return true;

case "proverHelp":
if (ps.ConfirmArgumentCount(0)) {
ProverHelpRequested = true;
}
return true;

case "DoomStrategy":
ps.GetNumericArgument(ref DoomStrategy);
return true;

case "DoomRestartTP":
if (ps.ConfirmArgumentCount(0)) {
DoomRestartTP = true;
}
return true;

case "extractLoops":
if (ps.ConfirmArgumentCount(0)) {
ExtractLoops = true;
}
return true;
return true;

case "deterministicExtractLoops":
if (ps.ConfirmArgumentCount(0)) {
Expand Down Expand Up @@ -1502,7 +1434,7 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
case "traceCaching":
ps.GetNumericArgument(ref TraceCaching, 4);
return true;

case "platform":
if (ps.ConfirmArgumentCount(1)) {
StringCollection platformOptions = this.ParseNamedArgumentList(args[ps.i]);
Expand Down Expand Up @@ -1563,9 +1495,8 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command
ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||
ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) ||
ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) ||
ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||
ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) ||
ps.CheckBooleanFlag("traceDiagnosticsOnTimeout", ref TraceDiagnosticsOnTimeout) ||
ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) ||
Expand Down Expand Up @@ -1597,7 +1528,6 @@ protected override bool ParseOption(string name, CommandLineOptionEngine.Command

public override void ApplyDefaultOptions() {
Contract.Ensures(TheProverFactory != null);
Contract.Ensures(vcVariety != VCVariety.Unspecified);

base.ApplyDefaultOptions();

Expand All @@ -1617,17 +1547,8 @@ public override void ApplyDefaultOptions() {
TheProverFactory = ProverFactory.Load(ProverDllName);
}

var proverOpts = TheProverFactory.BlankProverOptions();
proverOpts.Parse(ProverOptions);
if (ProverHelpRequested) {
Console.WriteLine(proverOpts.Help);
}
if (!TheProverFactory.SupportsLabels(proverOpts)) {
UseLabels = false;
}

if (vcVariety == VCVariety.Unspecified) {
vcVariety = TheProverFactory.DefaultVCVariety;
Console.WriteLine(TheProverFactory.BlankProverOptions().Help);
}

if (UseArrayTheory) {
Expand Down Expand Up @@ -1853,7 +1774,7 @@ identifies variables
expressions into templates with holes. By default, holes
are maximally large subexpressions that do not contain
bound variables. This option performs a form of lambda
lifting in which holes are the lambda's free variables.
lifting in which holes are the lambda's free variables.
/overlookTypeErrors : skip any implementation with resolution or type
checking errors
Expand Down Expand Up @@ -1961,7 +1882,7 @@ verify several program snapshots (named <filename>.v0.bpl
3 - use the more advanced caching and report errors according
to the new source locations for errors and their
related locations (but not /errorTrace and CaptureState
locations)
locations)
/traceCaching:<n>
0 (default) - none
1 - for testing
Expand All @@ -1975,12 +1896,6 @@ verify each input program separately
/coalesceBlocks:<c>
0 = do not coalesce blocks
1 = coalesce blocks (default)
/vc:<variety> n = nested block,
m = nested block reach,
b = flat block, r = flat block reach,
s = structured, l = local,
d = dag (default)
doomed = doomed
/traceverify print debug output during verification condition generation
/subsumption:<c>
apply subsumption to asserted conditions:
Expand Down Expand Up @@ -2025,7 +1940,7 @@ how to encode types when sending VC to theorem prover
p = predicates (default)
a = arguments
m = monomorphic
/monomorphize
/monomorphize
Do not abstract map types in the encoding (this is an
experimental feature that will not do the right thing if
the program uses polymorphism)
Expand Down Expand Up @@ -2065,7 +1980,7 @@ assertion in the keep going mode. Defaults to 30s.
/vcsPathCostMult:<f1>
/vcsAssumeMult:<f2>
The cost of a block is
(<assert-cost> + <f2>*<assume-cost>) *
(<assert-cost> + <f2>*<assume-cost>) *
(1.0 + <f1>*<entering-paths>)
<f1> defaults to 1.0, <f2> defaults to 0.01.
The cost of a single assertion or assumption is
Expand Down
11 changes: 0 additions & 11 deletions Source/Core/VCExp.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,17 +254,6 @@ public virtual bool SupportsDags {
}
}

public virtual CommandLineOptions.VCVariety DefaultVCVariety {
get {
Contract.Ensures(Contract.Result<CommandLineOptions.VCVariety>() != CommandLineOptions.VCVariety.Unspecified);
return CommandLineOptions.VCVariety.DagIterative;
}
}

public virtual bool SupportsLabels(ProverOptions options) {
return true;
}

public virtual void Close() {
}

Expand Down
Loading

0 comments on commit 55baa23

Please sign in to comment.