Merge

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));

         }

       }