summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl3
-rw-r--r--Source/Dafny/Translator.cs20
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs5
-rw-r--r--Source/Model/Model.cs7
-rw-r--r--Source/ModelViewer/DafnyProvider.cs358
-rw-r--r--Source/ModelViewer/Main.cs1
-rw-r--r--Source/ModelViewer/ModelViewer.csproj1
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs40
8 files changed, 414 insertions, 21 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 476a6bd9..5675d2a1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -4,6 +4,9 @@
// Edited sequence axioms 20 October 2009 by Alex Summers.
// Copyright (c) 2008-2010, Microsoft.
+const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as
+axiom $$Language$Dafny; // coming from a Dafny program.
+
// ---------------------------------------------------------------
// -- References -------------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 55769d0f..44e05a41 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -948,6 +948,19 @@ namespace Microsoft.Dafny {
// set up the information used to verify the method's modifies clause
DefineFrame(m.tok, m.Mod, builder, localVariables);
}
+
+ Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
+ Contract.Requires(tok != null);
+ Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);
+ string description = string.Format("{0}({1},{2}){3}{4}", tok.filename, tok.line, tok.col, additionalInfo == null ? "" : ": ", additionalInfo ?? "");
+ QKeyValue kv = new QKeyValue(tok, "captureState", new List<object>() { description }, null);
+ return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv);
+ }
+ Bpl.Cmd CaptureState(IToken tok) {
+ Contract.Requires(tok != null);
+ Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);
+ return CaptureState(tok, null);
+ }
void CEVPrelude(Method m, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams, Bpl.StmtListBuilder builder)
{
@@ -959,7 +972,7 @@ namespace Microsoft.Dafny {
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(1))));
foreach (Bpl.Variable p in inParams) {
- Contract.Assert( p != null);
+ Contract.Assert(p != null);
builder.Add(new Bpl.CallCmd(p.tok, "CevVarIntro",
new Bpl.ExprSeq(
CevLocation(p.tok),
@@ -2576,6 +2589,7 @@ void ObjectInvariant()
new Bpl.IdentifierExprSeq()));
}
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStep", new Bpl.ExprSeq(CevLocation(stmt.Tok)), new Bpl.IdentifierExprSeq()));
+ builder.Add(CaptureState(stmt.Tok));
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
@@ -2800,6 +2814,7 @@ void ObjectInvariant()
loopBodyBuilder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",
new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),
new Bpl.IdentifierExprSeq()));
+ loopBodyBuilder.Add(CaptureState(stmt.Tok, "loop entered"));
// termination checking
if (Contract.Exists(theDecreases,e=> e is WildcardExpr)) {
// omit termination checking for this loop
@@ -2826,6 +2841,7 @@ void ObjectInvariant()
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",
new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_exited", predef.CevEventType)),
new Bpl.IdentifierExprSeq()));
+ builder.Add(CaptureState(stmt.Tok, "loop exit"));
} else if (stmt is ForeachStmt) {
AddComment(builder, stmt, "foreach statement");
@@ -2952,6 +2968,7 @@ void ObjectInvariant()
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",
new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
new Bpl.IdentifierExprSeq()));
+ builder.Add(CaptureState(stmt.Tok));
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
@@ -3460,6 +3477,7 @@ void ObjectInvariant()
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
}
+ builder.Add(CaptureState(tok));
}
Bpl.AssumeCmd AssumeGoodHeap(IToken tok, ExpressionTranslator etran) {
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 48c85d27..bd87186b 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -717,8 +717,11 @@ void ObjectInvariant()
}
}
}
- errorCount++;
+ if (CommandLineOptions.Clo.ModelViewFile != null) {
+ error.PrintModel();
}
+ errorCount++;
+ }
}
Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
break;
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 3e5ff0c3..3d1df65e 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -123,6 +123,13 @@ namespace Microsoft.Boogie
}
}
+ public IEnumerable<FuncTuple> AppsWithArgs(int argIdx0, Element elt0, int argIdx1, Element elt1) {
+ foreach (var r in elt0.References) {
+ if (r.Func == this && r.Args[argIdx0] == elt0 && r.Args[argIdx1] == elt1)
+ yield return r;
+ }
+ }
+
public IEnumerable<FuncTuple> AppsWithResult(Element elt)
{
foreach (var r in elt.References) {
diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
new file mode 100644
index 00000000..8ac0d033
--- /dev/null
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -0,0 +1,358 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Boogie.ModelViewer.Dafny
+{
+ public class Provider : ILanguageProvider
+ {
+ public static Provider Instance = new Provider();
+ private Provider() { }
+
+ public bool IsMyModel(Model m)
+ {
+ return m.TryGetFunc("$$Language$Dafny") != null;
+ }
+
+ public IEnumerable<IState> GetStates(Model m)
+ {
+ System.Diagnostics.Debugger.Launch(); // KRML DEBUG
+ var dm = new DafnyModel(m);
+ foreach (var s in m.States) {
+ var sn = new StateNode(dm.states.Count, dm, s);
+ dm.states.Add(sn);
+ }
+ foreach (var s in dm.states) s.ComputeNames();
+ Namer.ComputeCanonicalNames(dm.states.Select(s => s.namer));
+ Namer.ComputeCanonicalNames(dm.states.Select(s => s.namer));
+ // Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));
+ return dm.states;
+ }
+ }
+
+ //KRML: todo: make this Dafny specific
+ enum DataKind
+ {
+ Flat,
+ PhysPtr,
+ SpecPtr,
+ Map
+ }
+
+ class DafnyModel
+ {
+ public readonly Model model;
+ public readonly Model.Func f_heap_select, f_class_int, f_class_bool, f_class_set, f_class_seq, f_dtype;
+ Dictionary<Model.Element, string> typeName = new Dictionary<Model.Element, string>();
+ public List<StateNode> states = new List<StateNode>();
+
+ public DafnyModel(Model m)
+ {
+ model = m;
+ f_heap_select = m.MkFunc("MapType1Select", 3); // todo: this is a hardcoded hack, we need a disciplined way of getting the name of this built-in select function
+
+ f_class_int = m.MkFunc("class.int", 0);
+ f_class_bool = m.MkFunc("class.bool", 0);
+ f_class_set = m.MkFunc("class.set", 0);
+ f_class_seq = m.MkFunc("class.seq", 0);
+ f_dtype = m.MkFunc("dtype", 1);
+ }
+
+ public string GetUserVariableName(string name)
+ {
+ if (name == "$Heap" || name == "$_Frame" || name == "#cev_pc")
+ return null;
+ var hash = name.IndexOf('#');
+ if (0 < hash)
+ return name.Substring(0, hash);
+ return name;
+ }
+
+ public Model.Element LocalType(Model.Element e)
+ {
+ if (e is Model.Integer)
+ return f_class_int.GetConstant();
+ if (e is Model.Boolean)
+ return f_class_bool.GetConstant();
+ var className = f_dtype.AppWithArg(0, e);
+ if (className != null)
+ return className.Result;
+ // don't know
+ return f_class_int.GetConstant();
+ }
+
+ public Model.Element Image(Model.Element elt, Model.Func f)
+ {
+ var r = f.AppWithResult(elt);
+ if (r != null)
+ return r.Args[0];
+ return null;
+ }
+
+ public string TypeName(Model.Element elt)
+ {
+ string res;
+ if (!typeName.TryGetValue(elt, out res)) {
+ if (elt == f_class_bool.GetConstant()) {
+ res = "bool";
+ } else if (elt == f_class_int.GetConstant()) {
+ res = "int";
+ } else if (elt == f_class_set.GetConstant()) {
+ res = "set"; // todo: instantiation?
+ } else if (elt == f_class_seq.GetConstant()) {
+ res = "seq"; // todo: instantiation?
+ } else {
+ res = "object"; // todo: specific class type; also todo: datatypes
+ }
+ typeName[elt] = res;
+ }
+ return res;
+ }
+
+ public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)
+ {
+ List<ElementNode> result = new List<ElementNode>();
+
+ var heap = state.state.TryGet("$Heap");
+ if (heap != null) {
+ foreach (var tpl in f_heap_select.AppsWithArgs(0, heap, 1, elt)) {
+ var field = tpl.Args[2];
+ var fieldName = field.ToString();
+ foreach (var n in field.Names) {
+ fieldName = n.Func.Name;
+ int dot = fieldName.LastIndexOf('.');
+ if (0 <= dot) {
+ fieldName = fieldName.Substring(dot + 1);
+ }
+ break;
+ }
+ var val = tpl.Result;
+ var ftp = LocalType(val);
+ var edgname = new EdgeName(state.namer, "%0." + fieldName, fieldName, elt);
+ result.Add(new FieldNode(state, edgname, val, ftp));
+ }
+ }
+
+ return result;
+ }
+ }
+
+ class StateNode : IState
+ {
+ internal readonly Model.CapturedState state;
+ readonly string name;
+ internal readonly DafnyModel dm;
+ internal readonly List<VariableNode> vars = new List<VariableNode>();
+ internal readonly Namer namer = new Namer();
+ internal readonly int index;
+
+ public StateNode(int i, DafnyModel parent, Model.CapturedState s)
+ {
+ dm = parent;
+ state = s;
+ index = i;
+
+ name = s.Name;
+ var idx = name.LastIndexOfAny(new char[] { '\\', '/' });
+ if (0 <= idx)
+ name = name.Substring(idx + 1);
+ var limit = 16;
+ if (name.Length > limit) {
+ idx = name.IndexOf('(');
+ if (idx > 0) {
+ var prefLen = limit - (name.Length - idx);
+ if (prefLen > 2) {
+ name = name.Substring(0,prefLen) + ".." + name.Substring(idx);
+ }
+ }
+ }
+
+ SetupVars();
+ }
+
+ void SetupVars()
+ {
+ var names = Util.Empty<string>();
+
+ if (dm.states.Count > 0) {
+ var prev = dm.states.Last();
+ names = prev.vars.Map(v => v.realName);
+ }
+
+ names = names.Concat(state.Variables).Distinct();
+
+ var curVars = state.Variables.ToDictionary(x => x);
+ foreach (var v in names) {
+ if (dm.GetUserVariableName(v) != null) {
+ var val = state.TryGet(v);
+ var tp = dm.LocalType(val);
+ // val = dm.WrapForUse(val, tp);
+ var vn = new VariableNode(this, v, val, tp);
+ vn.updatedHere = dm.states.Count > 0 && curVars.ContainsKey(v);
+ vars.Add(vn);
+ }
+ }
+
+ foreach (var e in dm.model.Elements) {
+ if (e is Model.Number || e is Model.Boolean)
+ namer.AddName(e, new EdgeName(e.ToString()));
+ }
+ }
+
+ internal void ComputeNames()
+ {
+ namer.ComputeNames(vars);
+ }
+
+ public string Name
+ {
+ get { return name; }
+ }
+
+ public IEnumerable<IDisplayNode> Nodes
+ {
+ get {
+ return vars;
+ }
+ }
+
+ }
+
+ class ElementNode : DisplayNode
+ {
+ protected StateNode stateNode;
+ protected Model.Element elt, tp;
+ protected DafnyModel vm { get { return stateNode.dm; } }
+ protected List<ElementNode> children;
+
+ public ElementNode(StateNode st, IEdgeName name, Model.Element elt, Model.Element tp)
+ : base(name)
+ {
+ this.stateNode = st;
+ this.tp = tp;
+ this.elt = elt;
+ }
+
+ public ElementNode(StateNode st, string name, Model.Element elt, Model.Element tp)
+ : this(st, new EdgeName(name), elt, tp) { }
+
+ public override Model.Element Element
+ {
+ get
+ {
+ return elt;
+ }
+ }
+
+ protected virtual void DoInitChildren()
+ {
+ children.AddRange(vm.GetExpansion(stateNode, elt, tp));
+ }
+
+ protected void InitChildren()
+ {
+ if (children == null) {
+ children = new List<ElementNode>();
+ DoInitChildren();
+ }
+ }
+
+ public override string CanonicalValue
+ {
+ get
+ {
+ return stateNode.namer.CanonicalName(Element);
+ }
+ }
+
+ public override IEnumerable<string> Aliases
+ {
+ get
+ {
+ if (Element is Model.Boolean) {
+ yield break;
+ } else {
+ foreach (var edge in stateNode.namer.Aliases(Element))
+ if (!edge.Equals(Name))
+ yield return edge.FullName();
+ }
+ }
+ }
+
+ public override string ToolTip
+ {
+ get
+ {
+ var sb = new StringBuilder();
+ sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));
+ int limit = 30;
+ foreach (var n in Aliases){
+ sb.AppendFormat(" = {0}\n", n);
+ if (limit-- < 0) {
+ sb.Append("...");
+ break;
+ }
+ }
+ return sb.ToString();
+ }
+ }
+
+ public override bool Expandable
+ {
+ get
+ {
+ InitChildren();
+ return children.Count > 0;
+ }
+ }
+
+ public override IEnumerable<IDisplayNode> Expand()
+ {
+ InitChildren();
+ return children;
+ }
+ }
+
+ class FieldNode : ElementNode
+ {
+ public FieldNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)
+ : base(par, realName, elt, tp)
+ {
+ /*
+ var idx = realName.LastIndexOf('.');
+ if (idx > 0)
+ name = realName.Substring(idx + 1);
+ */
+ }
+ }
+
+ class MapletNode : ElementNode
+ {
+ public MapletNode(StateNode par, IEdgeName realName, Model.Element elt, Model.Element tp)
+ : base(par, realName, elt, tp)
+ {
+ }
+ }
+
+ class VariableNode : ElementNode
+ {
+ public bool updatedHere;
+ public string realName;
+
+ public VariableNode(StateNode par, string realName, Model.Element elt, Model.Element tp)
+ : base(par, realName, elt, tp)
+ {
+ this.realName = realName;
+ name = new EdgeName(vm.GetUserVariableName(realName));
+ }
+
+ public override NodeState State
+ {
+ get
+ {
+ return base.State | (updatedHere ? NodeState.Changed : NodeState.Normal);
+ }
+ }
+ }
+}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 609bf571..dbb91390 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -24,6 +24,7 @@ namespace Microsoft.Boogie.ModelViewer
IEnumerable<ILanguageProvider> Providers()
{
yield return Vcc.Provider.Instance;
+ yield return Dafny.Provider.Instance;
yield return Base.Provider.Instance;
}
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index 413abd67..3027900a 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -68,6 +68,7 @@
</ItemGroup>
<ItemGroup>
<Compile Include="BaseProvider.cs" />
+ <Compile Include="DafnyProvider.cs" />
<Compile Include="DataModel.cs" />
<Compile Include="Main.cs">
<SubType>Form</SubType>
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 927868b5..031f0f18 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -210,10 +210,7 @@ namespace Microsoft.Boogie {
Contract.Assert(mvstates.Arity == 1);
foreach (Variable v in MvInfo.AllVariables) {
- var fn = m.TryGetFunc(v.Name);
- if (fn != null && fn.Arity == 0) {
- m.InitialState.AddBinding(v.Name, fn.GetConstant());
- }
+ m.InitialState.AddBinding(v.Name, GetModelValue(m, v));
}
var states = new List<int>();
@@ -239,21 +236,7 @@ namespace Microsoft.Boogie {
if (e is IdentifierExpr) {
IdentifierExpr ide = (IdentifierExpr)e;
-
- // first, get the unique name
- string uniqueName;
- VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(ide.Decl);
- if (vvar == null) {
- uniqueName = ide.Decl.Name;
- } else {
- uniqueName = Context.Lookup(vvar);
- }
-
- var f = m.TryGetFunc(uniqueName);
- if (f == null) {
- f = m.MkFunc(uniqueName, 0);
- }
- elt = f.GetConstant();
+ elt = GetModelValue(m, ide.Decl);
} else if (e is LiteralExpr) {
LiteralExpr lit = (LiteralExpr)e;
elt = m.MkElement(lit.Val.ToString());
@@ -272,6 +255,25 @@ namespace Microsoft.Boogie {
return m;
}
+ private Model.Element GetModelValue(Model m, Variable v) {
+ Model.Element elt;
+ // first, get the unique name
+ string uniqueName;
+ VCExprVar vvar = Context.BoogieExprTranslator.TryLookupVariable(v);
+ if (vvar == null) {
+ uniqueName = v.Name;
+ } else {
+ uniqueName = Context.Lookup(vvar);
+ }
+
+ var f = m.TryGetFunc(uniqueName);
+ if (f == null) {
+ f = m.MkFunc(uniqueName, 0);
+ }
+ elt = f.GetConstant();
+ return elt;
+ }
+
public abstract int GetLocation();
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 07:15:40 +0000