diff options
author | Rustan Leino <leino@microsoft.com> | 2011-12-05 23:08:25 -0800 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-12-05 23:08:25 -0800 |
commit | 1dcb9b3aa68245791e667f7354ada0dac1fbeddb (patch) | |
tree | 1f148b11bdaeb3aed4030b63d39d4b673c378d0e /Source | |
parent | 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd (diff) | |
parent | b5eca423560fa18e89d7a03c3b8a2baa5dce3249 (diff) |
Merge
Diffstat (limited to 'Source')
-rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 19 | ||||
-rw-r--r-- | Source/Core/Absy.cs | 1 | ||||
-rw-r--r-- | Source/Houdini/Houdini.cs | 62 | ||||
-rw-r--r-- | Source/ModelViewer/VccProvider.cs | 30 | ||||
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 24 | ||||
-rw-r--r-- | Source/VCGeneration/VC.cs | 4 |
6 files changed, 111 insertions, 29 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index aa132c5d..cffe3b5a 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -67,7 +67,22 @@ namespace Microsoft.Boogie { Helpers.ExtraTraceInformation("Becoming sentient");
+ List<string> fileList = new List<string>();
foreach (string file in CommandLineOptions.Clo.Files) {
+ string extension = Path.GetExtension(file);
+ if (extension != null) {
+ extension = extension.ToLower();
+ }
+ if (extension == ".txt") {
+ StreamReader stream = new StreamReader(file);
+ string s = stream.ReadToEnd();
+ fileList.AddRange(s.Split(new char[3] {' ', '\n', '\r'}, StringSplitOptions.RemoveEmptyEntries));
+ }
+ else {
+ fileList.Add(file);
+ }
+ }
+ foreach (string file in fileList) {
Contract.Assert(file != null);
string extension = Path.GetExtension(file);
if (extension != null) {
@@ -79,7 +94,7 @@ namespace Microsoft.Boogie { goto END;
}
}
- ProcessFiles(CommandLineOptions.Clo.Files);
+ ProcessFiles(fileList);
END:
if (CommandLineOptions.Clo.XmlSink != null) {
@@ -374,6 +389,8 @@ namespace Microsoft.Boogie { // Coalesce blocks
if (CommandLineOptions.Clo.CoalesceBlocks) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 402905a3..5f7328d1 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2017,6 +2017,7 @@ namespace Microsoft.Boogie { stream.WriteLine(this, level, "// " + Comment);
}
stream.Write(this, level, "{0}requires ", Free ? "free " : "");
+ Cmd.EmitAttributes(stream, Attributes);
this.Condition.Emit(stream);
stream.WriteLine(";");
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index ed3d1afc..f6dd07bf 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -255,25 +255,46 @@ namespace Microsoft.Boogie.Houdini { private Checker checker;
private Graph<Implementation> callGraph;
private bool continueAtError;
+ private HashSet<Implementation> vcgenFailures;
public Houdini(Program program, bool continueAtError) {
this.program = program;
- this.callGraph = BuildCallGraph();
this.continueAtError = continueAtError;
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Collecting existential constants...");
this.houdiniConstants = CollectExistentialConstants();
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Building call graph...");
+ this.callGraph = BuildCallGraph();
+
Inline();
+
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+ vcgenFailures = new HashSet<Implementation>();
Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Beginning VC generation for Houdini...");
foreach (Implementation impl in callGraph.Nodes) {
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ try {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Generating VC for {0}", impl.Name);
+ // make a different simplify log file for each function
+ String simplifyLog = null;
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+ simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ }
+ HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ houdiniSessions.Add(impl, session);
+ }
+ catch (VCGenException) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("VC generation failed");
+ vcgenFailures.Add(impl);
}
- HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- houdiniSessions.Add(impl, session);
}
this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
}
@@ -281,17 +302,40 @@ namespace Microsoft.Boogie.Houdini { private void Inline() {
if (CommandLineOptions.Clo.InlineDepth < 0)
return;
+
foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
}
foreach (Implementation impl in callGraph.Nodes) {
+ CommandLineOptions.Inlining savedOption = CommandLineOptions.Clo.ProcedureInlining;
+ CommandLineOptions.Clo.ProcedureInlining = CommandLineOptions.Inlining.Spec;
Inliner.ProcessImplementationForHoudini(program, impl);
+ CommandLineOptions.Clo.ProcedureInlining = savedOption;
}
foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
}
+
+ Graph<Implementation> oldCallGraph = callGraph;
+ callGraph = new Graph<Implementation>();
+ foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) {
+ callGraph.AddEdge(edge.Item1, edge.Item2);
+ }
+ int count = CommandLineOptions.Clo.InlineDepth;
+ while (count > 0) {
+ foreach (Implementation impl in oldCallGraph.Nodes) {
+ List<Implementation> newNodes = new List<Implementation>();
+ foreach (Implementation succ in callGraph.Successors(impl)) {
+ newNodes.AddRange(oldCallGraph.Successors(succ));
+ }
+ foreach (Implementation newNode in newNodes) {
+ callGraph.AddEdge(impl, newNode);
+ }
+ }
+ count--;
+ }
}
private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
@@ -349,6 +393,7 @@ namespace Microsoft.Boogie.Houdini { sccs.Compute();
foreach (SCC<Implementation> scc in sccs) {
foreach (Implementation impl in scc) {
+ if (vcgenFailures.Contains(impl)) continue;
queue.Enqueue(impl);
}
}
@@ -806,6 +851,9 @@ namespace Microsoft.Boogie.Houdini { public HoudiniOutcome PerformHoudiniInference() {
HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
this.NotifyStart(program, houdiniConstants.Keys.Count);
+ foreach (Implementation impl in vcgenFailures) {
+ current.addToBlackList(impl.Name);
+ }
while (current.WorkQueue.Count > 0) {
bool exceptional = false;
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index 6fd068a8..4a6d579b 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -39,7 +39,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state,
f_int_to_version, f_int_to_ptrset, f_set_in0, f_is_ghost_field, f_is_phys_field, f_idx, f_field_plus,
f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array, f_active_option, f_int_to_field,
- f_blob_type, f_array_emb, f_addr, f_address_root, f_base, f_field_arr_size, f_field_arr_root, f_field_arr_index;
+ f_blob_type, f_array_emb, f_addr, f_address_root, f_base, f_field_arr_size, f_field_arr_root, f_field_arr_index,
+ f_dot, f_prim_emb;
public readonly Model.Element tp_object, tp_mathint, tp_bool, tp_state, tp_ptrset, tp_heaptp;
public readonly Model.Element elt_me, elt_null;
Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
@@ -80,6 +81,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc f_int_to_ptr = m.MkFunc("$int_to_ptr", 1);
f_ptr_to_int = m.MkFunc("$ptr_to_int", 1);
f_ptr = m.MkFunc("$ptr", 2);
+ f_dot = m.MkFunc("$dot", 2);
f_map_t = m.MkFunc("$map_t", 2);
f_is_null = m.MkFunc("$is_null", 1);
f_good_state = m.MkFunc("$good_state", 1);
@@ -99,6 +101,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc f_array_emb = m.MkFunc("$array_emb", 2);
f_addr = m.MkFunc("$addr", 1);
f_base = m.MkFunc("$base", 1);
+ f_prim_emb = m.MkFunc("$prim_emb", 1);
f_address_root = m.MkFunc("$address_root", 2);
f_field_arr_index = m.MkFunc("$field_arr_index", 1);
f_field_arr_size = m.MkFunc("$field_arr_size", 1);
@@ -941,13 +944,14 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var addresses = new HashSet<Model.Element>();
if (heap != null && elt != null) {
+ var basePtr = f_base.TryEval(elt);
foreach (var fld in f_select_field.AppsWithArg(0, heap)) {
var val = f_select_value.TryEval(fld.Result, elt);
if (val != null) {
var field = fld.Args[1];
if (!IsConstantField(field) && viewOpts.ViewLevel <= 2)
- continue;
- var addr = f_ptr.TryEval(field, elt);
+ continue;
+ var addr = f_dot.TryEval(elt, field);
if (addr != null) addresses.Add(addr);
var node = ComputeUnionActiveOption(state, elt, val, field);
if (node != null)
@@ -965,18 +969,18 @@ namespace Microsoft.Boogie.ModelViewer.Vcc if (eltBase != null && eltField != null) {
foreach (var app in f_field_plus.AppsWithArg(0, eltField)) {
var fieldName = app.Result;
- var addr = f_ptr.TryEval(fieldName, eltBase);
+ var addr = f_dot.TryEval(eltBase, fieldName);
if (addr == null) continue;
Model.Element val = null, atp = tp;
addresses.Add(addr);
- foreach (var papp in f_ptr.AppsWithResult(addr)) {
- var tmp = f_select_value.OptEval(f_select_field.OptEval(heap, papp.Args[0]), papp.Args[1]);
+ foreach (var papp in f_dot.AppsWithResult(addr)) {
+ var tmp = f_select_value.OptEval(f_select_field.OptEval(heap, papp.Args[1]), papp.Args[0]);
if (tmp != null) {
val = tmp;
- var tt = f_field_type.TryEval(papp.Args[0]);
+ var tt = f_field_type.TryEval(papp.Args[1]);
if (tt != null) atp = tt;
}
}
@@ -991,16 +995,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc }
if (elt != null) {
- foreach (var ptr in f_ptr.AppsWithArg(1, elt)) {
+ foreach (var ptr in f_dot.AppsWithArg(0, elt)) {
if (addresses.Contains(ptr.Result)) continue;
- var fld = ptr.Args[0];
+ var fld = ptr.Args[1];
var idx = f_field_arr_index.TryEval(fld);
if (idx != null) {
var xtp = f_field_type.TryEval(fld);
result.Add(new MapletNode(state, new EdgeName(this, "&[%0] of %1", idx, f_field_arr_size.TryEval(fld)), ptr.Result, GuessPtrTo(xtp)) { Category = NodeCategory.Maplet });
}
- if (!IsConstantField(ptr.Args[0])) continue;
- BuildFieldNode(result, state, ptr.Result, ptr.Args[0], null, ptr.Result);
+ if (!IsConstantField(ptr.Args[1])) continue;
+ BuildFieldNode(result, state, ptr.Result, ptr.Args[1], null, ptr.Result);
}
}
@@ -1008,7 +1012,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc AddSpecialField(state, elt, result, "\\owner", f_owners);
AddSpecialField(state, elt, result, "\\root", f_roots);
AddSpecialField(state, elt, result, "\\timestamp", f_timestamps);
- AddPointerFunction(state, elt, result, "\\embedding", f_base, tp_object);
+ AddPointerFunction(state, elt, result, "\\embedding", f_prim_emb, tp_object);
AddPointerFunction(state, elt, result, "\\addr", f_addr, tp_mathint);
if (viewOpts.ViewLevel >= 1 && elt != null) {
@@ -1137,7 +1141,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc private FieldNode ComputeUnionActiveOption(StateNode state, Model.Element elt, Model.Element val, Model.Element field)
{
if (f_active_option.AppsWithResult(field).FirstOrDefault() != null) {
- var activeOpt = f_ptr.OptEval(f_int_to_field.OptEval(val), elt);
+ var activeOpt = f_dot.OptEval(elt, f_int_to_field.OptEval(val));
if (activeOpt != null) {
var nm = ConstantFieldName(field);
var fieldNode = new FieldNode(state, new EdgeName(nm), activeOpt, GuessType(activeOpt)) { Category = NodeCategory.MethodologyProperty };
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index cb28cd7d..6752a2b7 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1201,14 +1201,7 @@ namespace VC { Contract.Assert(sortedNodes != null);
#endregion
- // Create substitution for old expressions
- Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
- foreach (IdentifierExpr ie in modifies) {
- Contract.Assert(ie != null);
- if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))
- oldFrameMap.Add(ie.Decl, ie);
- }
- Substitution oldFrameSubst = Substituter.SubstitutionFromHashtable(oldFrameMap);
+ Substitution oldFrameSubst = ComputeOldExpressionSubstitution(modifies);
// Now we can process the nodes in an order so that we're guaranteed to have
// processed all of a node's predecessors before we process the node.
@@ -1257,6 +1250,21 @@ namespace VC { }
/// <summary>
+ /// Compute the substitution for old expressions.
+ /// </summary>
+ protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)
+ {
+ Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
+ foreach (IdentifierExpr ie in modifies)
+ {
+ Contract.Assert(ie != null);
+ if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))
+ oldFrameMap.Add(ie.Decl, ie);
+ }
+ return Substituter.SubstitutionFromHashtable(oldFrameMap);
+ }
+
+ /// <summary>
/// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc
/// Meanwhile, record any information needed to later reconstruct a model view.
/// </summary>
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 486f940f..36b9edc2 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2388,6 +2388,10 @@ namespace VC { Block entryBlock = cce.NonNull( impl.Blocks[0]);
cmds.AddRange(entryBlock.Cmds);
entryBlock.Cmds = cmds;
+ // Make sure that all added commands are passive commands.
+ Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());
+ TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,
+ ComputeOldExpressionSubstitution(impl.Proc.Modifies));
}
}
|