summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/Absy.cs67
-rw-r--r--Source/Core/AbsyCmd.cs18
-rw-r--r--Source/Core/AbsyQuant.cs27
-rw-r--r--Source/Core/CommandLineOptions.cs28
-rw-r--r--Source/Core/ResolutionContext.cs12
5 files changed, 134 insertions, 18 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 36c99b7b..8a8558bf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -696,6 +696,8 @@ namespace Microsoft.Boogie {
}
}
+ public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+
public IEnumerable<Block> Blocks()
{
return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
@@ -733,6 +735,45 @@ namespace Microsoft.Boogie {
}
}
+
+ /// <summary>
+ /// Finds blocks that break out of a loop in NaturalLoops(header, backEdgeNode)
+ /// </summary>
+ /// <param name="header"></param>
+ /// <param name="backEdgeNode"></param>
+ /// <returns></returns>
+ private HashSet<Block> GetBreakBlocksOfLoop(Block header, Block backEdgeNode, Graph<Block/*!*/>/*!*/ g)
+ {
+ Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+ var immSuccBlks = new HashSet<Block>();
+ var loopBlocks = g.NaturalLoops(header, backEdgeNode);
+ foreach (Block/*!*/ block in loopBlocks)
+ {
+ Contract.Assert(block != null);
+ var auxCmd = block.TransferCmd as GotoCmd;
+ if (auxCmd == null) continue;
+ foreach (var bl in auxCmd.labelTargets)
+ {
+ if (loopBlocks.Contains(bl)) continue;
+ immSuccBlks.Add(bl);
+ }
+ }
+ return immSuccBlks;
+ }
+
+ private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g)
+ {
+ Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+ var allBlocksInNaturalLoops = new HashSet<Block>();
+ foreach (Block/*!*/ source in g.BackEdgeNodes(header))
+ {
+ Contract.Assert(source != null);
+ g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b));
+ }
+ return allBlocksInNaturalLoops;
+ }
+
+
void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
List<Implementation/*!*/>/*!*/ loopImpls,
Dictionary<string, Dictionary<string, Block>> fullMap) {
@@ -788,7 +829,13 @@ namespace Microsoft.Boogie {
foreach (Block/*!*/ b in g.BackEdgeNodes(header))
{
Contract.Assert(b != null);
- foreach (Block/*!*/ block in g.NaturalLoops(header, b))
+ HashSet<Block> immSuccBlks = new HashSet<Block>();
+ if (detLoopExtract)
+ {
+ //Need to get the blocks that exit the loop, as we need to add them to targets and footprint
+ immSuccBlks = GetBreakBlocksOfLoop(header, b, g);
+ }
+ foreach (Block/*!*/ block in g.NaturalLoops(header, b).Union(immSuccBlks))
{
Contract.Assert(block != null);
foreach (Cmd/*!*/ cmd in block.Cmds)
@@ -943,18 +990,16 @@ namespace Microsoft.Boogie {
GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
+ //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
+ var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source);
foreach(var bl in auxGotoCmd.labelTargets) {
- bool found = false;
- foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains?
- if (bl == n) { //clarify: is this the right comparison?
- found = true;
- break;
- }
- }
- if (!found) {
+ if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
+ !loopNodes.Contains(bl)) {
Block auxNewBlock = new Block();
auxNewBlock.Label = ((Block)bl).Label;
- auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);
+ //these blocks may have read/write locals that are not present in naturalLoops
+ //we need to capture these variables
+ auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);
//add restoration code for such blocks
if (loopHeaderToAssignCmd.ContainsKey(header))
{
@@ -2196,6 +2241,7 @@ namespace Microsoft.Boogie {
}
public class Incarnation : LocalVariable {
public int incarnationNumber;
+ public readonly Variable OriginalVariable;
public Incarnation(Variable/*!*/ var, int i) :
base(
var.tok,
@@ -2203,6 +2249,7 @@ namespace Microsoft.Boogie {
) {
Contract.Requires(var != null);
incarnationNumber = i;
+ OriginalVariable = var;
}
}
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 404945a9..2e33e1dd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie {
} finally {
rc.TypeBinderState = previousTypeBinderState;
}
+
+ var id = QKeyValue.FindStringAttribute(Attributes, "id");
+ if (id != null)
+ {
+ rc.AddStatementId(tok, id);
+ }
}
public override void AddAssignedVariables(List<Variable> vars) {
@@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie {
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
Expr.Resolve(rc);
+
+ var id = QKeyValue.FindStringAttribute(Attributes, "id");
+ if (id != null)
+ {
+ rc.AddStatementId(tok, id);
+ }
}
public override void AddAssignedVariables(List<Variable> vars) {
//Contract.Requires(vars != null);
@@ -3206,8 +3218,14 @@ namespace Microsoft.Boogie {
this.Expr.Emit(stream);
stream.WriteLine(";");
}
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ ResolveAttributes(Attributes, rc);
+ base.Resolve(rc);
+ }
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
+ TypecheckAttributes(Attributes, tc);
Expr.Typecheck(tc);
Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition
if (!Expr.Type.Unify(Type.Bool)) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9f94490b..3a27eddf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -338,6 +338,17 @@ namespace Microsoft.Boogie {
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
+
+ if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
+ {
+ rc.Error(this, "attributes :minimize and :maximize accept only one argument");
+ }
+
+ if (Key == "verified_under" && Params.Count != 1)
+ {
+ rc.Error(this, "attribute :verified_under accepts only one argument");
+ }
+
foreach (object p in Params) {
if (p is Expr) {
((Expr)p).Resolve(rc);
@@ -348,8 +359,20 @@ namespace Microsoft.Boogie {
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
foreach (object p in Params) {
- if (p is Expr) {
- ((Expr)p).Typecheck(tc);
+ var expr = p as Expr;
+ if (expr != null) {
+ expr.Typecheck(tc);
+ }
+ if ((Key == "minimize" || Key == "maximize")
+ && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
+ {
+ tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
+ break;
+ }
+ if (Key == "verified_under" && (expr == null || !expr.Type.IsBool))
+ {
+ tc.Error(this, "attribute :verified_under accepts only one argument of type bool");
+ break;
}
}
}
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 2be1cdf7..e9aa3ceb 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -11,6 +11,7 @@ using System.IO;
using System.Linq;
using System.Diagnostics;
using System.Diagnostics.Contracts;
+using System.Text.RegularExpressions;
namespace Microsoft.Boogie {
public class CommandLineOptionEngine
@@ -478,6 +479,8 @@ namespace Microsoft.Boogie {
public string AbstractHoudini = null;
public bool UseUnsatCoreForContractInfer = false;
public bool PrintAssignment = false;
+ // TODO(wuestholz): Add documentation for this flag.
+ public bool PrintNecessaryAssumes = false;
public int InlineDepth = -1;
public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
public bool UseUncheckedContracts = false;
@@ -588,7 +591,7 @@ namespace Microsoft.Boogie {
}
}
- public string OwickiGriesDesugaredOutputFile = null;
+ public string CivlDesugaredFile = null;
public bool TrustAtomicityTypes = false;
public bool TrustNonInterference = false;
public int TrustLayersUpto = -1;
@@ -915,9 +918,9 @@ namespace Microsoft.Boogie {
}
return true;
- case "OwickiGries":
+ case "CivlDesugaredFile":
if (ps.ConfirmArgumentCount(1)) {
- OwickiGriesDesugaredOutputFile = args[ps.i];
+ CivlDesugaredFile = args[ps.i];
}
return true;
@@ -1502,7 +1505,7 @@ namespace Microsoft.Boogie {
return true;
case "verifySnapshots":
- ps.GetNumericArgument(ref VerifySnapshots, 3);
+ ps.GetNumericArgument(ref VerifySnapshots, 4);
return true;
case "traceCaching":
@@ -1618,6 +1621,7 @@ namespace Microsoft.Boogie {
ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+ ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) ||
ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
@@ -1700,7 +1704,7 @@ namespace Microsoft.Boogie {
// no preference
return true;
}
- return ProcsToCheck.Contains(methodFullname);
+ return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$"));
}
public virtual StringCollection ParseNamedArgumentList(string argList) {
@@ -1857,7 +1861,15 @@ namespace Microsoft.Boogie {
Multiple .bpl files supplied on the command line are concatenated into one
Boogie program.
- /proc:<p> : limits which procedures to check
+ /proc:<p> : Only check procedures matched by pattern <p>. This option
+ may be specified multiple times to match multiple patterns.
+ The pattern <p> matches the whole procedure name (i.e.
+ pattern ""foo"" will only match a procedure called foo and
+ not fooBar). The pattern <p> may contain * wildcards which
+ match any character zero or more times. For example the
+ pattern ""ab*d"" would match abd, abcd and abccd but not
+ Aabd nor abdD. The pattern ""*ab*d*"" would match abd,
+ abcd, abccd, Abd and abdD.
/noResolve : parse only
/noTypecheck : parse and resolve only
@@ -1961,6 +1973,10 @@ namespace Microsoft.Boogie {
0 - do not use any verification result caching (default)
1 - use the basic verification result caching
2 - use the more advanced verification result caching
+ 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)
/verifySeparately
verify each input program separately
/removeEmptyBlocks:<c>
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 474a91dd..279e00bf 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -339,6 +339,18 @@ namespace Microsoft.Boogie {
varContext = varContext.ParentContext;
}
+ public readonly ISet<string> StatementIds = new HashSet<string>();
+
+ public void AddStatementId(IToken tok, string name)
+ {
+ if (StatementIds.Contains(name))
+ {
+ Error(tok, "more than one statement with same id: " + name);
+ return;
+ }
+ StatementIds.Add(name);
+ }
+
public void AddVariable(Variable var, bool global) {
Contract.Requires(var != null);
var previous = FindVariable(cce.NonNull(var.Name), !global);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 06:30:57 +0000