summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/Absy.cs28
-rw-r--r--Source/Core/AbsyCmd.cs18
-rw-r--r--Source/Core/AbsyQuant.cs27
-rw-r--r--Source/Core/CommandLineOptions.cs16
-rw-r--r--Source/Core/ResolutionContext.cs12
5 files changed, 92 insertions, 9 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2e68002..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);
@@ -750,15 +752,28 @@ namespace Microsoft.Boogie {
Contract.Assert(block != null);
var auxCmd = block.TransferCmd as GotoCmd;
if (auxCmd == null) continue;
- foreach(var bl in auxCmd.labelTargets)
+ foreach (var bl in auxCmd.labelTargets)
{
if (loopBlocks.Contains(bl)) continue;
- immSuccBlks.Add(bl);
+ 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) {
@@ -975,10 +990,11 @@ namespace Microsoft.Boogie {
GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
- var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g);
- var loopNodes = g.NaturalLoops(header, source);
+ //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) {
- if (!loopNodes.Contains(bl)) {
+ 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;
//these blocks may have read/write locals that are not present in naturalLoops
@@ -2225,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,
@@ -2232,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 f4cba1dc..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;
@@ -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
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-06-10 01:45:19 +0000