summaryrefslogtreecommitdiff
path: root/Source/ModelViewer/VccProvider.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ModelViewer/VccProvider.cs')
-rw-r--r--Source/ModelViewer/VccProvider.cs3052
1 files changed, 1526 insertions, 1526 deletions
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index ae062c93..345dfda5 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -1,1526 +1,1526 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-namespace Microsoft.Boogie.ModelViewer.Vcc
-{
- public class Provider : ILanguageProvider
- {
- public static Provider Instance = new Provider();
- private Provider() { }
-
- public bool IsMyModel(Model m)
- {
- return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;
- }
-
- public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
- {
- var vm = new VccModel(m, opts);
- return vm;
- }
- }
-
- enum DataKind
- {
- Flat,
- PhysPtr,
- SpecPtr,
- Object,
- Ptrset,
- Map
- }
-
- class VccModel : LanguageModel
- {
- public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,
- f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t, f_select_ptr,
- 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_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_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>();
- Dictionary<Model.Element, string> literalName = new Dictionary<Model.Element, string>();
- Dictionary<Model.Element, Model.Element> guessedType = new Dictionary<Model.Element,Model.Element>();
- public List<StateNode> states = new List<StateNode>();
- public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();
-
- Dictionary<Model.Element, string> datatypeLongName = new Dictionary<Model.Element, string>();
-
- Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();
-
- public const string selfMarker = "\\self";
- public const int maxDatatypeNameLength = 5;
-
- public VccModel(Model m, ViewOptions opts)
- : base(m, opts)
- {
- f_ptr_to = m.MkFunc("$ptr_to", 1);
- f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);
- f_phys_ptr_cast = m.MkFunc("$phys_ptr_cast", 2);
- f_spec_ptr_cast = m.MkFunc("$spec_ptr_cast", 2);
- f_mathint = m.MkFunc("^^mathint", 0);
- f_local_value_is = m.MkFunc("$local_value_is", 5);
- f_heap = m.MkFunc("$heap", 1);
- f_select_field = m.MkFunc("Select_[$field][$ptr]$int", 2);
- f_select_value = m.MkFunc("Select_[$ptr]$int", 2);
- f_select_ptr = m.MkFunc("Select_[$ptr]$ptr", 2);
- f_select_int = m.MkFunc("Select_[$ptr]$int", 2);
- f_select_bool = m.MkFunc("Select_[$ptr]$bool", 2);
- f_owners = m.MkFunc("$f_owner", 1);
- f_closed = m.MkFunc("$f_closed", 1);
- f_roots = m.MkFunc("$roots", 1);
- f_timestamps = m.MkFunc("$f_timestamp", 1);
- f_active_option = m.MkFunc("$f_active_option", 1);
- f_field = m.MkFunc("$field", 1);
- f_field_type = m.MkFunc("$field_type", 1);
- 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);
- f_int_to_version = m.MkFunc("$int_to_version", 1);
- f_int_to_ptrset = m.MkFunc("$int_to_ptrset", 1);
- f_int_to_field = m.MkFunc("$int_to_field", 1);
- f_set_in0 = m.MkFunc("$set_in0", 2);
- f_is_ghost_field = m.MkFunc("$is_ghost_field", 1);
- f_is_phys_field = m.MkFunc("$is_phys_field", 1);
- f_idx = m.MkFunc("$idx", 2);
- f_is_sequential_field = m.MkFunc("$is_sequential_field", 1);
- f_is_volatile_field = m.MkFunc("$is_volatile_field", 1);
- f_type_project_0 = m.MkFunc("$type_project_0", 1);
- f_array = m.MkFunc("$array", 2);
- f_blob_type = m.MkFunc("$blob_type", 1);
- 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);
- f_field_arr_root = m.MkFunc("$field_arr_root", 1);
-
- tp_bool = m.GetFunc("^^bool").GetConstant();
- tp_mathint = m.GetFunc("^^mathint").GetConstant();
- tp_object = m.GetFunc("^^object").GetConstant();
- tp_state = m.GetFunc("^$#state_t").GetConstant();
- tp_ptrset = m.GetFunc("^$#ptrset").GetConstant();
-
- tp_heaptp = m.MkFunc("$heap_type", 0).GetConstant();
-
- elt_me = m.GetFunc("$me").GetConstant();
- elt_null = m.GetFunc("$null").GetConstant();
-
- literalName[elt_me] = "\\me";
- literalName[elt_null] = "NULL";
- foreach (var tpl in f_phys_ptr_cast.Apps) {
- if (tpl.Args[0] == elt_null)
- literalName[tpl.Result] = "(" + TypeName(tpl.Args[1]) + "*)NULL";
- }
- foreach (var tpl in f_spec_ptr_cast.Apps) {
- if (tpl.Args[0] == elt_null)
- literalName[tpl.Result] = "(" + TypeName(tpl.Args[1]) + "^)NULL";
- }
- foreach (var fn in model.Functions) {
- if (fn.Arity == 0 && fn.Name.StartsWith("l#"))
- literalName[fn.GetConstant()] = ":" + fn.Name.Substring(2);
- }
-
- DecodeFileNames();
- ComputeLocalVariableNames();
-
- foreach (var s in m.States) {
- var sn = new StateNode(this, s);
- sn.SetupVars();
- states.Add(sn);
- }
-
- var allStates = states.ToArray();
- if (allStates.Length == 1 && allStates[0].vars.Count == 0) {
- throw new Exception("This VCC model doesn't contain any variables. Was it saved with the -bvd option?");
- }
- states.Clear();
- var i = 0;
- while (i < allStates.Length) {
- var lastGoodName = allStates[i].State.Name;
-
- var userVars = new HashSet<string>(allStates[i].State.Variables.Where(localVariableNames.ContainsKey));
- i++;
- while (i < allStates.Length) {
- foreach (var v in allStates[i].State.Variables) {
- if (v == "$s" || userVars.Contains(v)) goto stop;
- if (localVariableNames.ContainsKey(v))
- userVars.Add(v);
- }
-
- var curName = TryParseSourceLocation(allStates[i].State.Name);
- if (!IsBadName(curName))
- lastGoodName = allStates[i].State.Name;
- i++;
- }
-
- stop:
-
- var lastState = allStates[i - 1];
- lastState.capturedStateName = lastGoodName;
- lastState.index = states.Count;
- states.Add(lastState);
- lastState.SetupVars();
- }
-
- foreach (var s in states) {
- var elt = s.State.TryGet("$s");
- if (elt != null)
- literalName[elt] = "\\state'" + s.index;
- }
-
- GenerateSourceLocations(states);
- }
-
-
- bool IsBadName(SourceLocation l)
- {
- return l == null || l.Filename.StartsWith("<");
- }
-
- private void ComputeLocalVariableNames()
- {
- var vars = model.States.SelectMany(s => s.Variables).Where(v => v != null).Distinct();
- Func<string, string> simpleName = s => { string dummy; return GetUserVariableNameCore(s, out dummy); };
- var userVars = vars.Where(s => simpleName(s) != null);
- var conflictsName = Conflicts(userVars, simpleName).ToArray();
- Func<string, string> qName = s => { string kind, n = GetUserVariableNameCore(s, out kind); return n + " (" + kind + ")"; };
- var conflictsKind = Conflicts(conflictsName, qName).ToArray();
-
- var conflictsNameH = new HashSet<string>(conflictsName);
- var conflictsKindH = new HashSet<string>(conflictsKind);
-
- foreach (var v in userVars) {
- if (conflictsKindH.Contains(v)) continue;
- if (conflictsNameH.Contains(v))
- localVariableNames[v] = qName(v);
- else
- localVariableNames[v] = simpleName(v);
- }
-
- var idx = 0;
- foreach (var v in conflictsKind) {
- localVariableNames[v] = string.Format("{0} #{1}", qName(v), idx++);
- }
- }
-
- static IEnumerable<A> Conflicts<A, B>(IEnumerable<A> input, Func<A, B> f)
- {
- var revMap = new Dictionary<B, A>();
- var reported = new HashSet<A>();
-
- foreach (var k in input) {
- if (reported.Contains(k)) continue;
- var v = f(k);
- A tmp;
- if (revMap.TryGetValue(v, out tmp) && !tmp.Equals(k)) {
- if (!reported.Contains(tmp)) {
- yield return tmp;
- reported.Add(tmp);
- }
- yield return k;
- reported.Add(k);
- } else {
- revMap[v] = k;
- }
- }
- }
-
- #region Function name scoring
- static string[][] prefixes = new string[][] {
- new string[] { "F#", "$eq.$map", "Q#", },
- new string[] { "F#lambda", },
- new string[] { "$int_to_", "lambda@", "distinct-aux-f", "Select_","Store_", "$select.", "$store.", },
- };
-
- static string[][] totals = new string[][] {
- new string[] {
- "$current_timestamp",
- "$full_stop", "$function_entry", "$ptr_to_i4",
- "$ptr_to_i8", "$ptr_to_u4", "$ptr_to_u8",
- "$span", "$sizeof", "$in_domain",
- "$inv2",
- "$is_claimable",
- "$set_cardinality", "$set_difference", "$set_union",
- "$thread_local", "$unchecked", "$writes_at",
- "$array_range", "$arrays_disjoint",
- "$byte_ptr_subtraction",
- },
-
- new string[] {
- "$addr", "$dot", "$emb0", "$fetch_from_domain", "$in_range_phys_ptr",
- "$in_range_spec_ptr", "$is_sequential_field", "$is_volatile_field",
- "$is_ghost_field", "$is_phys_field", "$is_math_type", "$invok_state",
- "$is_primitive",
- "$spec_ptr_cast",
- "$phys_ptr_cast",
- "$is_null",
- "$in_domain_lab",
- "$inv_lab",
- "$set_in0",
- },
-
- new string[] {
- "$_pow2", "$as_composite_field", "$as_field_with_type", "$as_in_range_t",
- "$as_primitive_field", "$base", "$call_transition", "tickleBool", "Ctor",
- "$mv_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
- "$field_parent_type", "$field_type", "$file_name_is", "$good_state",
- "$good_state_ext", "$function_arg_type", "$has_field_at0", "$map_domain",
- "$map_range", "$map_t", "$ptr_to", "$ptr_to_i1", "$ptr_to_i2",
- "$ptr_to_u1", "$ptr_to_u2", "$is_unwrapped", "$is_unwrapped_dynamic",
- "$heap", "$closed", "$owner", "$owns", "$modifies", "$post_unwrap",
- "$pow2", "$pre_unwrap", "$ptr", "$is", "$in_range_t", "$roots",
- "$timestamp", "$type_branch", "$type_code_is", "$type_project_0",
- "$typemap", "$set_in_pos", "$updated_owns", "$ver_domain", "$vs_state",
- "$set_singleton",
- "$f_owner", "$f_closed", "$f_timestamps",
- "$local_value_is",
- "$field_arr_ctor",
- "$idx",
- },
- };
-
- string[] state_props = new string[] { };
-
- Dictionary<string, int> functionScores = new Dictionary<string, int>();
-
- int FunctionScore(string name)
- {
- if (functionScores.Count == 0) {
- for (int i = 0; i < totals.Length; ++i)
- foreach (var s in totals[i])
- functionScores[s] = i;
- }
-
- int res;
- if (functionScores.TryGetValue(name, out res))
- return res;
-
- res = -1;
- if (name[0] == '$' && name.EndsWith("_to_int"))
- res = 1;
- else if (name.EndsWith("#frame"))
- res = 2;
- else if (name.Contains("#limited#"))
- res = 2;
- else {
- for (int i = 0; i < prefixes.Length; ++i)
- foreach (var p in prefixes[i])
- if (name.StartsWith(p)) {
- res = i;
- //goto stop;
- }
- //stop: ;
- }
-
- if (res == -1)
- res = 1; // default
-
- functionScores[name] = res;
- return res;
- }
- #endregion
-
- private void DecodeFileNames()
- {
- var fis = model.GetFunc("$file_name_is");
- foreach (var f in model.Functions) {
- if (f.Arity == 0 && f.Name.StartsWith("#file^")) {
- var sb = new StringBuilder();
- var idx = 6;
- var name = f.Name;
- while (idx < name.Length) {
- if (name[idx] == '?') {
- var c = (char)Int32.Parse(name.Substring(idx + 1, 2), System.Globalization.NumberStyles.HexNumber);
- sb.Append(c);
- idx += 3;
- } else {
- sb.Append(name[idx++]);
- }
- }
- name = sb.ToString();
-
- foreach (var app in fis.AppsWithArg(1, f.GetConstant()))
- fileNameMapping[app.Args[0].AsInt()] = name;
- }
- }
- }
-
- private Model.Element DecodeDT(string dt)
- {
- if (dt.StartsWith("dt")) {
- var tpName = dt.Replace("dt", "#distTp");
- var f = model.TryGetFunc(tpName);
- if (f != null) {
- return f.GetConstant();
- //var res = f_type_project_0.TryEval(ptr);
- //if (res != null)
- // tp = res;
- }
- }
- return null;
- }
-
- private string DecodeToken(string name, ref Model.Element tp)
- {
- var idx = name.LastIndexOf("$");
- if (idx < 0) return null;
- var words = name.Substring(idx + 1).Split('.', '^', '!', '#', '@');
- if (words.Length > 3)
- tp = DecodeDT(words[3]);
- return string.Format("{0}({1},{2})", fileNameMapping[int.Parse(words[0])], words[1], words[2]);
- }
-
- public string GetUserVariableName(string name)
- {
- string res;
- localVariableNames.TryGetValue(name, out res);
- return res;
- }
-
-
- string GetUserVariableNameCore(string name, out string kind)
- {
- if (name.StartsWith("L#")) {
- kind = "local";
- return name.Substring(2);
- }
-
- if (name.StartsWith("P#")) {
- kind = "in-param";
- return name.Substring(2);
- }
-
- if (name.StartsWith("OP#")) {
- kind = "out-param";
- return name.Substring(3);
- }
-
- if (name.StartsWith("SL#")) {
- kind = "spec local";
- return name.Substring(3);
- }
-
- if (name.StartsWith("SP#")) {
- kind = "spec in-param";
- return name.Substring(3);
- }
-
- if (name.StartsWith("local.")) {
- kind = "param copied to local";
- return name.Substring(6);
- }
-
- if (name.StartsWith("addr.")) {
- kind = "stack-allocated struct";
- return name.Substring(5);
- }
-
- if (name == "$result") {
- kind = "function return value";
- return "\\result";
- }
-
- if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1) {
- kind = "call result";
- return name;
- }
-
- if (name == "$s" && viewOpts.ViewLevel >= 1) {
- kind = "current state";
- return "\\now";
- }
-
- kind = null;
- return null;
- }
-
-
- private string LiteralName(Model.Element elt)
- {
- string r;
-
- if (literalName.TryGetValue(elt, out r))
- return r;
-
- r = TryTypeName(elt);
- if (r != null) {
- literalName[elt] = r;
- return r;
- }
-
- var i = elt as Model.Integer;
- if (i != null)
- return AsPow2(i);
-
- var bv = elt as Model.BitVector;
- if (bv != null)
- return bv.Numeral + "bv" + bv.Size.ToString();
-
- return null;
- }
-
- public Model.Element LocalType(string localName)
- {
- string dummy;
- var v = GetUserVariableNameCore(localName, out dummy);
- if (v == null) v = localName;
- var c = model.TryGetFunc("#loc." + v);
- if (c != null) {
- var localIs = f_local_value_is.AppWithArg(2, c.GetConstant());
- if (localIs != null)
- return localIs.Args[4];
- }
- foreach (var s in model.States.Reverse()) {
- var val = s.TryGet(localName);
- var tp = GuessType(val);
- if (tp != tp_mathint)
- return tp;
- }
- return tp_mathint;
- }
-
- public Model.Element Image(Model.Element elt, Model.Func f)
- {
- var r = f.AppWithResult(elt);
- if (r != null)
- return r.Args[0];
- return null;
- }
-
- string TypeNameCore(Model.Element elt)
- {
- var deref = Image(elt, f_ptr_to);
- if (deref != null)
- return TypeName(deref) + "*";
- deref = Image(elt, f_spec_ptr_to);
- if (deref != null)
- return TypeName(deref) + "^";
- deref = Image(elt, f_blob_type);
- if (deref != null)
- return "_(blob " + CanonicalName(deref) + ")";
- var mapt = f_map_t.AppWithResult(elt);
- if (mapt != null)
- return string.Format("{1}[{0}]", TypeName(mapt.Args[0]), TypeName(mapt.Args[1]));
-
- var arr = f_array.AppWithResult(elt);
- if (arr != null) {
- return string.Format("{0}[{1}]", TypeName(arr.Args[0]), arr.Args[1].ToString());
- }
-
- foreach (var app in elt.Names)
- if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^")) {
- var n = app.Func.Name.Substring(1);
- switch (n) {
- case "^i1": return "int8_t";
- case "^u1": return "uint8_t";
- case "^i2": return "int16_t";
- case "^u2": return "uint16_t";
- case "^i4": return "int32_t";
- case "^u4": return "uint32_t";
- case "^i8": return "int64_t";
- case "^u8": return "uint64_t";
- case "^bool": return "bool";
- default:
- var pref = "_vcc_math_type_";
- if (n.StartsWith(pref)) n = n.Substring(pref.Length);
- return n;
- }
- }
-
- return null;
- }
-
- public string TypeName(Model.Element elt)
- {
- var r = TryTypeName(elt);
- if (r == null)
- return elt.ToString();
- else return r;
- }
-
- public string TryTypeName(Model.Element elt)
- {
- string res;
- if (!typeName.TryGetValue(elt, out res)) {
- typeName[elt] = elt.ToString(); // avoid infinite recursion
- res = TypeNameCore(elt);
- typeName[elt] = res;
- }
- return res;
- }
-
- public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root", "$f_active_option" };
-
- public string ConstantFieldName(Model.Element elt)
- {
- string res;
- IsConstantField(elt, out res);
- return res;
- }
-
- public bool IsConstantField(Model.Element elt)
- {
- string dummy;
- return IsConstantField(elt, out dummy);
- }
-
- public bool IsConstantField(Model.Element elt, out string theName)
- {
- var bestScore = int.MinValue;
- string bestName = null;
-
- foreach (var t in elt.Names) {
- var score = int.MinValue;
- string name = null;
- if (t.Args.Length == 0) {
- name = t.Func.Name;
- score = 0;
- var dotIdx = name.IndexOf('.');
- if (dotIdx > 0) {
- score += 10;
- name = name.Substring(dotIdx + 1);
- }
- if (name.Contains('#')) score -= 1;
- } else if (t.Func.Name.StartsWith("$f_") && synthethic_fields.Contains(t.Func.Name)) {
- name = string.Format("{0}<{1}>", t.Func.Name.Substring(3).Replace("root", "alloc_root"), TypeName(t.Args[0]));
- score = 6;
- } else if (t.Func == f_array_emb) {
- name = string.Format("[0] (of {0}[{1}])", TypeName(t.Args[0]), t.Args[1].ToString());
- score = 5;
- }
- if (score > bestScore) {
- bestScore = score;
- bestName = name;
- }
- }
-
- theName = bestName;
- return bestScore >= 5;
- }
-
- bool IsSomeState(Model.Element elt)
- {
- var tp = GuessType(elt);
- return tp == tp_state || tp == tp_heaptp;
- }
-
- bool IsThisState(Model.Element st, Model.Element elt)
- {
- return elt == st || elt == f_heap.TryEval(st);
- }
-
- Model.Element GuessType(Model.Element element)
- {
- Model.Element res;
- if (!guessedType.TryGetValue(element, out res)) {
- res = GuessTypeCore(element);
- guessedType[element] = res;
- }
- return res;
- }
-
- Model.Element GuessTypeCore(Model.Element element)
- {
- if (element is Model.Boolean)
- return tp_bool;
-
- var fld = f_field.TryEval(element);
- if (fld != null) {
- var tp = f_field_type.TryEval(fld);
- if (tp != null) {
- var ptp = f_ptr_to.TryEval(tp);
- if (ptp != null)
- return ptp;
- ptp = f_spec_ptr_to.TryEval(tp);
- if (ptp != null)
- return ptp;
- }
- return tp_object;
- }
-
- foreach (var tpl in element.References) {
- if (element == tpl.Result) {
- if (tpl.Func == f_ptr)
- return tp_object;
- if (tpl.Func == f_heap)
- return tp_heaptp;
- }
-
- if (tpl.Args.Length >= 1 && tpl.Args[0] == element) {
- if (tpl.Func == f_heap || tpl.Func == f_closed || tpl.Func == f_good_state)
- return tp_state;
- }
-
- if (tpl.Func == f_select_bool)
- if (tpl.Args[0] == element)
- return tp_ptrset;
- else if (tpl.Args[1] == element)
- return tp_object;
-
- var fname = tpl.Func.Name;
-
- if (tpl.Args.Length == 2 && tpl.Args[0] == element && fname.StartsWith("$select.$map_t")) {
- var mt = model.TryGetFunc("MT#" + fname);
- if (mt != null && mt.Arity == 0)
- return mt.GetConstant();
- var t1 = GuessType(tpl.Args[1]);
- var t2 = GuessType(tpl.Result);
- var t = f_map_t.TryEval(t1, t2);
- if (t != null)
- return t;
- }
-
- var tpName = DataTypeName(element, tpl);
- if (tpName != null) {
- var tp = model.TryGetFunc("^$#" + tpName);
- if (tp != null)
- return tp.GetConstant();
- }
- }
-
- return tp_mathint;
- }
-
- string DataTypeName(Model.Element elt, Model.FuncTuple tpl)
- {
- var fname = tpl.Func.Name;
- if (tpl.Args.Length == 1 && tpl.Args[0] == elt && fname.StartsWith("RF#")) {
- var fldName = tpl.Func.Name.Substring(3);
- var idx = fldName.LastIndexOf('.');
- if (idx > 0) {
- return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");
- }
- }
-
- if (tpl.Args.Length == 1 && tpl.Args[0] == elt && (fname.StartsWith("DSZ#") || fname.StartsWith("RSZ#") || fname.StartsWith("DGH#"))) {
- return fname.Substring(4).Replace("_vcc_math_type_", "");
- }
- return null;
- }
-
- public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)
- {
- tpl = null;
-
- if (tp == tp_object)
- return DataKind.Object;
- else if (tp == tp_ptrset)
- return DataKind.Ptrset;
-
- tpl = f_ptr_to.AppWithResult(tp);
- if (tpl != null) return DataKind.PhysPtr;
- tpl = f_spec_ptr_to.AppWithResult(tp);
- if (tpl != null) return DataKind.SpecPtr;
- tpl = f_map_t.AppWithResult(tp);
- if (tpl != null) return DataKind.Map;
-
- return DataKind.Flat;
- }
-
- public DataKind GetKind(Model.Element tp)
- {
- Model.FuncTuple dummy;
- return GetKind(tp, out dummy);
- }
-
-
- public Model.Element WrapForUse(Model.Element elt, Model.Element tp)
- {
- Model.FuncTuple tpl;
- var kind = GetKind(tp, out tpl);
-
- if (kind == DataKind.Flat) {
- if (elt.Kind == Model.ElementKind.Integer) {
- var tpname = TypeName(tp);
- if(tpname.StartsWith("$")) tpname = tpname.Substring(1);
- if (tpname.StartsWith("#")) {
- foreach (var tupl in elt.References) {
- if (tupl.Args.Length == 1 && tupl.Args[0] == elt && tupl.Func.Name.StartsWith("$int_to_") && tupl.Func.Name.EndsWith(tpname)) {
- return tupl.Result;
- }
- }
- }
- }
- return elt;
- }
-
- if (kind == DataKind.Map) {
- if (elt.Kind == Model.ElementKind.Integer) {
- Model.Element theMap = null;
- foreach (var conv in model.Functions)
- // really, we should reconstruct the name of this function, but this is painful
- if (conv.Arity == 1 && conv.Name.StartsWith("$int_to_map_t")) {
- var app = conv.AppWithArg(0, elt);
- if (app != null) {
- theMap = app.Result;
- break;
- }
- }
- if (theMap == null) return elt;
- return theMap;
- }
- return elt;
- } else if (kind == DataKind.Ptrset) {
- var tmp = f_int_to_ptrset.TryEval(elt);
- if (tmp != null)
- return tmp;
- return elt;
- }
-
- if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr || kind == DataKind.Object) {
- if (elt.Kind == Model.ElementKind.Integer) {
- var tmp = f_int_to_ptr.TryEval(elt);
- if (tmp != null)
- elt = tmp;
- }
- }
-
- if (kind == DataKind.Object)
- return elt;
-
- if (kind == DataKind.PhysPtr)
- return Util.OrElse(f_phys_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
-
- if (kind == DataKind.SpecPtr)
- return Util.OrElse(f_spec_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
-
- Util.Assert(false);
- return elt;
- }
-
- void AddSpecialField(StateNode state, Model.Element elt, List<ElementNode> res, string name, Model.Func select_map)
- {
- if (elt == null) return;
-
- var map = state.State.TryGet("$s");
- if (map != null)
- map = select_map.TryEval(map);
- if (map != null) {
- var model = elt.Model;
- Model.Element val = f_select_bool.TryEval(map, elt);
- Model.Element tp = tp_bool;
- if (val == null) {
- val = f_select_ptr.TryEval(map, elt);
- tp = tp_object;
- }
- if (val == null) {
- val = f_select_int.TryEval(map, elt);
- tp = tp_mathint;
- }
- if (val != null) {
- res.Add(new FieldNode(state, new EdgeName(name), val, tp) { Category = NodeCategory.MethodologyProperty });
- }
- }
- }
-
- void AddPointerFunction(StateNode state, Model.Element elt, List<ElementNode> res, string name, Model.Func fn, Model.Element tp)
- {
- if (elt == null) return;
-
- var val = fn.TryEval(elt);
- if (val != null) {
- res.Add(new FieldNode(state, new EdgeName(name), val, tp) { Category = NodeCategory.MethodologyProperty });
- }
- }
-
- void AddPtrType(StateNode state, Model.Element elt, List<ElementNode> res)
- {
- var f = f_field.TryEval(elt);
- if (f == null) return;
-
- var tp = f_field_type.TryEval(f);
-
- var seq = "";
-
- var is_seq = f_is_sequential_field.TryEval(f) as Model.Boolean;
- var is_vol = f_is_volatile_field.TryEval(f) as Model.Boolean;
-
- if (is_seq != null && is_vol != null && is_seq.Value == is_vol.Value) {
- seq = " (volatile/sequential mismatch)";
- } else if ((is_seq != null && is_seq.Value) || (is_vol != null && !is_vol.Value)) {
- seq = " (sequential)";
- } else if ((is_seq != null && !is_seq.Value) || (is_vol != null && is_vol.Value)) {
- seq = " (volatile)";
- }
-
- if (tp != null || seq != "") {
- res.Add(new FieldNode(state, new EdgeName("\\typeof" + seq), tp, tp_mathint) { Category = NodeCategory.MethodologyProperty });
- }
- }
-
- string SkolemName(Model.Func f, ref Model.Element tp)
- {
- if (f.Name.IndexOf('!') > 0) {
- var tok = DecodeToken(f.Name, ref tp);
- if (tok != null) {
- var baseName = f.Name.Substring(0, f.Name.LastIndexOf('$'));
- if (baseName.StartsWith("Q#"))
- baseName = baseName.Substring(2);
- return string.Format("{0}@{1}", baseName, ShortenToken(tok, 10, false));
- }
- }
- return null;
- }
-
- string GlobalName(Model.Func f, ref Model.Element tp)
- {
- if (f.Name.StartsWith("G#")) {
- var idx = f.Name.LastIndexOf("#dt");
- if (idx < 0) return null;
- var name = f.Name.Substring(2, idx - 2);
- tp = DecodeDT(f.Name.Substring(idx + 1));
- return string.Format("::{0}", name);
- }
- return null;
- }
-
-
- public IEnumerable<ElementNode> CommonNodes(StateNode state)
- {
- var skolems = new List<ElementNode>();
-
- Model.Element tp = null;
-
- foreach (var f in model.Functions) {
- if (f.Arity != 0) continue;
- var s = SkolemName(f, ref tp);
- if (s == null)
- s = GlobalName(f, ref tp);
- if (s != null) {
- if (tp == null)
- tp = GuessType(f.GetConstant());
- var val = WrapForUse(f.GetConstant(), tp);
- skolems.Add(new VariableNode(state, s, val, tp));
- }
- }
-
- return skolems;
- }
-
- private Model.Element GuessPtrTo(Model.Element tp)
- {
- var p = f_ptr_to.TryEval(tp);
- if (p != null) return p;
- p = f_spec_ptr_to.TryEval(tp);
- if (p != null) return p;
- var nm = model.MkFunc("*ptrto_" + TypeName(tp), 0).GetConstant();
- f_ptr_to.AddApp(nm, tp);
- return f_ptr_to.TryEval(tp);
- }
-
- private Model.Element PtrTo(Model.Element tp, Model.Func f_ptr_to)
- {
- var p = f_ptr_to.TryEval(tp);
- if (p != null) return p;
- var nm = model.MkFunc("*" + f_ptr_to.Name + "_" + TypeName(tp), 0).GetConstant();
- f_ptr_to.AddApp(nm, tp);
- return f_ptr_to.TryEval(tp);
- }
-
- private bool IsArrayField(Model.Element ptr)
- {
- return ptr != null && f_idx.TryEval(ptr, model.TryMkElement("0")) != null;
- }
-
- public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)
- {
- List<ElementNode> result = new List<ElementNode>();
- Model.FuncTuple tpl;
-
- if (elt == null) return result;
-
- var kind = GetKind(tp, out tpl);
- if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr || kind == DataKind.Object) {
- var heap = state.State.TryGet("$s");
- if (heap != null)
- heap = f_heap.TryEval(heap);
- var addresses = new HashSet<Model.Element>();
-
- if (heap != 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_dot.TryEval(elt, field);
- if (addr != null) addresses.Add(addr);
- var node = ComputeUnionActiveOption(state, elt, val, field);
- if (node != null)
- result.Add(node);
- else
- BuildFieldNode(result, state, addr, field, val, addr);
- }
- }
- //result.Sort(CompareFields);
- }
-
- {
- foreach (var app in f_idx.AppsWithArg(0, elt)) {
- var addr = app.Result;
- Model.Element val = null, atp = tp;
-
- addresses.Add(addr);
-
- 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[1]);
- if (tt != null) atp = tt;
- }
- }
-
- if (val != null)
- val = WrapForUse(val, atp);
- result.Add(new MapletNode(state, new EdgeName(this, "[%0]", app.Args[1]), val, atp) { Category = NodeCategory.Maplet });
- if (addr != null)
- result.Add(new MapletNode(state, new EdgeName(this, "&[%0]", app.Args[1]), addr, GuessPtrTo(atp)) { Category = NodeCategory.Maplet });
- }
- }
-
- foreach (var ptr in f_dot.AppsWithArg(0, elt)) {
- if (addresses.Contains(ptr.Result)) continue;
- 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[1])) continue;
- BuildFieldNode(result, state, ptr.Result, ptr.Args[1], null, ptr.Result);
- }
-
- AddSpecialField(state, elt, result, "\\closed", f_closed);
- 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_prim_emb, tp_object);
- AddPointerFunction(state, elt, result, "\\addr", f_addr, tp_mathint);
-
- if (viewOpts.ViewLevel >= 1) {
- AddPtrType(state, elt, result);
- AddCasts(state, elt, result);
- var sets = new SetsNode(state, elt);
- if (!sets.IsEmpty)
- result.Add(sets);
- }
-
- } else if (kind == DataKind.Map) {
- var elTp = tpl.Args[1];
- foreach (var sel in model.Functions)
- if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {
- foreach (var app in sel.AppsWithArg(0, elt)) {
- var val = WrapForUse(app.Result, elTp);
- var edgname = new EdgeName(this, "[%0]", app.Args[1]);
- result.Add(new MapletNode(state, edgname, val, elTp) { Category = NodeCategory.Maplet });
- }
- }
- } else if (kind == DataKind.Ptrset) {
- foreach (var sel in f_select_bool.AppsWithArg(0, elt)) {
- var edgname = new EdgeName(this, "[%0]", sel.Args[1]);
- result.Add(new MapletNode(state, edgname, sel.Result, tp_bool) { Category = NodeCategory.Maplet });
- }
- } else if (kind == DataKind.Flat) {
- foreach (var tupl in elt.References) {
- if (tupl.Args.Length == 1 && tupl.Args[0] == elt) {
- var fname = tupl.Func.Name;
- var idx = fname.LastIndexOf('.');
- if (fname.StartsWith("RF#") && idx > 0) {
- fname = fname.Substring(idx + 1);
- } else if (fname.StartsWith("DP#p")) {
- fname = fname.Substring(4);
- idx = fname.IndexOf('#');
- if (idx > 0)
- fname = fname.Substring(idx + 1) + "#" + fname.Substring(0, idx);
- } else {
- fname = null;
- }
-
- if (fname != null)
- result.Add(new FieldNode(state, new EdgeName(fname), tupl.Result, GuessType(tupl.Result)) { Category = NodeCategory.SpecField });
- }
- }
- }
-
- if (!(elt is Model.Boolean)) {
- var curState = state.State.TryGet("$s");
-
- foreach (var tupl in elt.References) {
- {
- var seenSelf = false;
- var seenState = false;
- var seenThisState = false;
- var args = tupl.Args;
- for (int i = 0; i < args.Length; ++i) {
- if (args[i] == elt) seenSelf = true;
- if (IsThisState(curState, args[i])) seenThisState = true;
- else if (IsSomeState(args[i])) seenState = true;
- }
- if (!seenSelf) continue; // not looking for aliases (maybe we should?)
- if (seenState && !seenThisState) continue;
- }
-
- var argsFmt = new StringBuilder();
- var name = tupl.Func.Name;
-
- var score = FunctionScore(name);
- if (score >= viewOpts.ViewLevel)
- continue;
-
- var retTp = GuessType(tupl.Result);
- var retVal = tupl.Result;
-
- var cat = NodeCategory.MethodologyProperty;
- if (name.StartsWith("F#")) {
- name = name.Substring(2);
- cat = NodeCategory.UserFunction;
- }
-
- if (name.StartsWith("DF#")) {
- name = name.Substring(3);
- cat = NodeCategory.UserFunction;
- }
-
- if (name.StartsWith("$eq.$"))
- name = "EQ";
-
- {
- Model.Element sktp = null;
- var sk = SkolemName(tupl.Func, ref sktp);
- if (sk != null) {
- name = sk;
- if (sktp != null)
- retVal = WrapForUse(tupl.Result, sktp);
- cat = NodeCategory.Maplet;
- }
- }
-
- {
- argsFmt.Append(name).Append("(");
- var args = new List<Model.Element>();
- foreach (var a in tupl.Args) {
- if (IsThisState(curState, a))
- argsFmt.Append("\\now, ");
- else if (a == elt)
- argsFmt.Append(selfMarker + ", ");
- else {
- argsFmt.AppendFormat("%{0}, ", args.Count);
- args.Add(a);
- }
- }
- argsFmt.Length -= 2;
- argsFmt.Append(")");
- var edgeName = new EdgeName(this, argsFmt.ToString(), args.ToArray());
- result.Add(new MapletNode(state, edgeName, retVal, retTp) { ViewLevel = score, Category = cat });
- }
-
- }
- }
-
- return result;
- }
-
- 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_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 };
- return fieldNode;
- }
- }
- return null;
- }
-
- private void AddCasts(StateNode state, Model.Element elt, List<ElementNode> result)
- {
- foreach (var app in f_phys_ptr_cast.AppsWithArg(0, elt)) {
- if (app.Result != elt)
- result.Add(new MapletNode(state, new EdgeName(this, "(" + TypeName(app.Args[1]) + "*)..."), app.Result, PtrTo(app.Args[1], f_ptr_to)));
- }
- foreach (var app in f_spec_ptr_cast.AppsWithArg(0, elt)) {
- if (app.Result != elt)
- result.Add(new MapletNode(state, new EdgeName(this, "(" + TypeName(app.Args[1]) + "^)..."), app.Result, PtrTo(app.Args[1], f_spec_ptr_to)));
- }
- var addr = f_addr.TryEval(elt);
- if (addr != null) {
- foreach (var app in f_blob_type.Apps) {
- var blob = f_address_root.TryEval(addr, app.Result);
- if (blob != null) {
- result.Add(new MapletNode(state, new EdgeName(this, TypeName(app.Result) + "..."), blob, app.Result));
- }
- }
- }
- }
-
- private void BuildFieldNode(List<ElementNode> result, StateNode state, Model.Element ptr, Model.Element field, Model.Element val, Model.Element addr)
- {
- var ftp = f_field_type.TryEval(field);
- if (val != null)
- val = WrapForUse(val, ftp);
-
- if (IsArrayField(ptr)) {
- val = addr;
- addr = null;
- ftp = GuessPtrTo(ftp);
- }
-
- var nm = ConstantFieldName(field);
- var edgname = nm == null ? field.ToString() : nm;
-
- var cat = NodeCategory.PhysField;
- if (f_is_ghost_field.IsTrue(field))
- cat = NodeCategory.SpecField;
- if (nm != null && nm.Contains("<"))
- cat = NodeCategory.MethodologyProperty;
-
- var fieldNode = new FieldNode(state, new EdgeName(edgname), val, ftp) { Category = cat};
- result.Add(fieldNode);
-
- if (addr != null) {
- result.Add(new FieldNode(state, new EdgeName("&" + edgname), addr, GuessPtrTo(ftp)) { Category = cat });
- }
- }
-
- public override IEnumerable<IState> States
- {
- get
- {
- return states;
- }
- }
-
- private int DataTypeToString(StringBuilder sb, int level, Model.Element elt)
- {
- Model.FuncTuple ctor = null;
- int len = 1;
- string dataTypeType = null;
- foreach (var app in elt.References) {
- var n = app.Func.Name;
- if (app.Result == elt && n.StartsWith("DF#")) {
- ctor = app;
- }
- var tmp = DataTypeName(elt, app);
- if (tmp != null) dataTypeType = tmp;
- }
-
- if (dataTypeType != null) {
- if (ctor != null)
- sb.Append(ctor.Func.Name.Substring(3));
- else
- sb.Append(DataTypeShortName(elt, dataTypeType));
- if (ctor != null && ctor.Args.Length > 0) {
- if (level <= 0) sb.Append("(...)");
- else {
- sb.Append("(");
- for (int i = 0; i < ctor.Args.Length; ++i) {
- if (i != 0) sb.Append(", ");
- len += DataTypeToString(sb, level - 1, ctor.Args[i]);
- }
- sb.Append(")");
- }
- }
- } else {
- sb.Append(CanonicalName(elt));
- }
- return len;
- }
-
- private string DataTypeShortName(Model.Element elt, string tp)
- {
- var baseName = tp;
-
- var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt);
- if (hd != null) {
- foreach (var nm in hd.References) {
- if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
- baseName = nm.Func.Name.Substring(3);
- }
- }
-
- return baseName;
- }
-
- private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)
- {
- var vm = this;
-
- if (name.Contains("[") || name.Contains("'"))
- name = "";
-
- if (name != "")
- return name;
-
- var isNull = false;
- foreach (var tpl in elt.References) {
- var fn = tpl.Func;
- if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)
- return "map";
- if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)
- return "map";
-
- if (fn.Arity >= 1 && tpl.Args[0] == elt) {
- if (fn == f_select_bool)
- return "ptrset";
- }
-
- if (tpl.Result == elt)
- if (fn == f_int_to_version)
- return "version";
-
- if (fn == f_is_null && tpl.Result == model.True)
- isNull = true;
-
- var dtpName = DataTypeName(elt, tpl);
- if (dtpName != null) {
- var sb = new StringBuilder();
- string prev = null;
- datatypeLongName[elt] = "*SELF*"; // in case we recurse (but this shouldn't happen)
- for (int lev = 0; lev < 10; lev++) {
- sb.Length = 0;
- var len = DataTypeToString(sb, lev, elt);
- if (prev == null || len <= maxDatatypeNameLength)
- prev = sb.ToString();
- }
-
- datatypeLongName[elt] = prev;
- suff = NameSeqSuffix.WhenNonZero;
- return prev;
- }
- }
-
- var fld = vm.f_field.TryEval(elt);
- if (fld != null) {
- var tp = vm.f_field_type.TryEval(fld);
- if (tp != null) {
- var n = vm.TryTypeName(tp);
- if (n != null) {
- if (isNull)
- return "(" + n + "*)NULL";
- return n;
- }
- }
- }
-
- return "";
- }
-
- protected override string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)
- {
- var lit = this.LiteralName(elt);
- if (lit != null) {
- suff = NameSeqSuffix.None;
- return lit;
- }
- if (datatypeLongName.TryGetValue(elt, out lit)) {
- suff = NameSeqSuffix.WhenNonZero;
- return lit;
- }
-
- var name = base.CanonicalBaseName(elt, out suff);
- name = CanonicalBaseNameCore(name, elt, true, ref suff);
-
- return name;
- }
-
- public override string PathName(IEnumerable<IDisplayNode> path)
- {
- var sb = new StringBuilder();
- foreach (var d in path) {
- var name = d.Name;
- if (name == "") continue; // can that happen?
- if (name.Contains("(") && name.Contains(selfMarker)) {
- var repl = name.Replace(selfMarker, sb.ToString());
- sb.Length = 0;
- sb.Append(repl);
- } else {
- if (sb.Length > 0 && name[0] != '[')
- sb.Append("->");
- sb.Append(d.Name);
- }
- }
-
- return sb.ToString();
- }
- }
-
- class StateNode : NamedState
- {
- internal VccModel vm;
- internal List<VariableNode> vars;
- internal List<ElementNode> commons;
- internal int index;
- internal string capturedStateName;
-
- public StateNode(VccModel parent, Model.CapturedState s)
- : base(s, parent)
- {
- this.capturedStateName = s.Name;
- this.vm = parent;
- }
-
- internal void SetupVars()
- {
- if (vars != null) return;
- vars = new List<VariableNode>();
-
- var names = Util.Empty<string>();
-
- if (vm.states.Count > 0) {
- var prev = vm.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) {
- var localName = vm.GetUserVariableName(v);
- if (localName != null) {
- var tp = vm.LocalType(v);
- var val = state.TryGet(v);
- val = vm.WrapForUse(val, tp);
- var vn = new VariableNode(this, v, val, tp) { ShortName = localName };
- vn.updatedHere = vm.states.Count > 0 && curVars.ContainsKey(v);
- if (curVars.ContainsKey(v))
- vm.RegisterLocalValue(vn.Name, val);
- vars.Add(vn);
- }
- }
-
- vm.Flush(vars);
-
- commons = new List<ElementNode>();
- commons.AddRange(vm.CommonNodes(this));
- }
-
- public override IEnumerable<IDisplayNode> Nodes
- {
- get {
- return vars.Concat(commons);
- }
- }
-
- public override string CapturedStateName
- {
- get
- {
- return this.capturedStateName;
- }
- }
- }
-
- class ElementNode : DisplayNode
- {
- protected StateNode stateNode;
- protected Model.Element tp;
- protected VccModel vm { get { return stateNode.vm; } }
-
- public ElementNode(StateNode st, EdgeName name, Model.Element elt, Model.Element tp)
- : base(st.vm, name, elt)
- {
- this.stateNode = st;
- this.tp = tp;
- }
-
- protected override void ComputeChildren()
- {
- children.AddRange(vm.GetExpansion(stateNode, element, tp));
- }
-
- public override string ToolTip
- {
- get
- {
- var sb = new StringBuilder();
- if (tp != null)
- sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));
- var i = element as Model.Integer;
- if (i != null) {
- var n = System.Numerics.BigInteger.Parse(i.Numeral);
- sb.AppendFormat("Value: {0} (0x{1:x})\n", n, n);
- } else if (element != null) {
- sb.AppendFormat("Value: {0}\n", element);
- }
- return sb.ToString();
- }
- }
- }
-
- class SetsNode : ElementNode
- {
- List<Model.Element> refs = new List<Model.Element>();
-
- public SetsNode(StateNode par, Model.Element elt)
- : base(par, new EdgeName("\\in ..."), null, null)
- {
- children = new List<IDisplayNode>();
- foreach (var app in vm.f_select_bool.AppsWithArg(1, elt)) {
- children.Add(
- new MapletNode(par, new EdgeName(vm, VccModel.selfMarker + " \\in %0", app.Args[0]), app.Result, vm.tp_bool) { Category = NodeCategory.MethodologyProperty });
- refs.Add(app.Args[0]);
- }
- Category = NodeCategory.MethodologyProperty;
- }
-
- public override IEnumerable<Model.Element> References
- {
- get
- {
- return refs;
- }
- }
-
- public bool IsEmpty { get { return children.Count == 0; } }
- }
-
-
- class FieldNode : ElementNode
- {
- public FieldNode(StateNode par, EdgeName realName, Model.Element elt, Model.Element tp)
- : base(par, realName, elt, tp)
- {
- }
- }
-
- class MapletNode : ElementNode
- {
- public MapletNode(StateNode par, EdgeName 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, new EdgeName(realName), elt, tp)
- {
- this.realName = realName;
- }
-
- public override string ShortName
- {
- set { this.name = new EdgeName(value); }
- get { return this.name.ToString(); }
- }
- }
-}
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Boogie.ModelViewer.Vcc
+{
+ public class Provider : ILanguageProvider
+ {
+ public static Provider Instance = new Provider();
+ private Provider() { }
+
+ public bool IsMyModel(Model m)
+ {
+ return m.TryGetFunc("$is_ghost_field") != null && m.TryGetFunc("$fk_vol_version") != null;
+ }
+
+ public ILanguageSpecificModel GetLanguageSpecificModel(Model m, ViewOptions opts)
+ {
+ var vm = new VccModel(m, opts);
+ return vm;
+ }
+ }
+
+ enum DataKind
+ {
+ Flat,
+ PhysPtr,
+ SpecPtr,
+ Object,
+ Ptrset,
+ Map
+ }
+
+ class VccModel : LanguageModel
+ {
+ public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,
+ f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t, f_select_ptr,
+ 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_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_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>();
+ Dictionary<Model.Element, string> literalName = new Dictionary<Model.Element, string>();
+ Dictionary<Model.Element, Model.Element> guessedType = new Dictionary<Model.Element,Model.Element>();
+ public List<StateNode> states = new List<StateNode>();
+ public Dictionary<string, string> localVariableNames = new Dictionary<string, string>();
+
+ Dictionary<Model.Element, string> datatypeLongName = new Dictionary<Model.Element, string>();
+
+ Dictionary<int, string> fileNameMapping = new Dictionary<int, string>();
+
+ public const string selfMarker = "\\self";
+ public const int maxDatatypeNameLength = 5;
+
+ public VccModel(Model m, ViewOptions opts)
+ : base(m, opts)
+ {
+ f_ptr_to = m.MkFunc("$ptr_to", 1);
+ f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);
+ f_phys_ptr_cast = m.MkFunc("$phys_ptr_cast", 2);
+ f_spec_ptr_cast = m.MkFunc("$spec_ptr_cast", 2);
+ f_mathint = m.MkFunc("^^mathint", 0);
+ f_local_value_is = m.MkFunc("$local_value_is", 5);
+ f_heap = m.MkFunc("$heap", 1);
+ f_select_field = m.MkFunc("Select_[$field][$ptr]$int", 2);
+ f_select_value = m.MkFunc("Select_[$ptr]$int", 2);
+ f_select_ptr = m.MkFunc("Select_[$ptr]$ptr", 2);
+ f_select_int = m.MkFunc("Select_[$ptr]$int", 2);
+ f_select_bool = m.MkFunc("Select_[$ptr]$bool", 2);
+ f_owners = m.MkFunc("$f_owner", 1);
+ f_closed = m.MkFunc("$f_closed", 1);
+ f_roots = m.MkFunc("$roots", 1);
+ f_timestamps = m.MkFunc("$f_timestamp", 1);
+ f_active_option = m.MkFunc("$f_active_option", 1);
+ f_field = m.MkFunc("$field", 1);
+ f_field_type = m.MkFunc("$field_type", 1);
+ 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);
+ f_int_to_version = m.MkFunc("$int_to_version", 1);
+ f_int_to_ptrset = m.MkFunc("$int_to_ptrset", 1);
+ f_int_to_field = m.MkFunc("$int_to_field", 1);
+ f_set_in0 = m.MkFunc("$set_in0", 2);
+ f_is_ghost_field = m.MkFunc("$is_ghost_field", 1);
+ f_is_phys_field = m.MkFunc("$is_phys_field", 1);
+ f_idx = m.MkFunc("$idx", 2);
+ f_is_sequential_field = m.MkFunc("$is_sequential_field", 1);
+ f_is_volatile_field = m.MkFunc("$is_volatile_field", 1);
+ f_type_project_0 = m.MkFunc("$type_project_0", 1);
+ f_array = m.MkFunc("$array", 2);
+ f_blob_type = m.MkFunc("$blob_type", 1);
+ 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);
+ f_field_arr_root = m.MkFunc("$field_arr_root", 1);
+
+ tp_bool = m.GetFunc("^^bool").GetConstant();
+ tp_mathint = m.GetFunc("^^mathint").GetConstant();
+ tp_object = m.GetFunc("^^object").GetConstant();
+ tp_state = m.GetFunc("^$#state_t").GetConstant();
+ tp_ptrset = m.GetFunc("^$#ptrset").GetConstant();
+
+ tp_heaptp = m.MkFunc("$heap_type", 0).GetConstant();
+
+ elt_me = m.GetFunc("$me").GetConstant();
+ elt_null = m.GetFunc("$null").GetConstant();
+
+ literalName[elt_me] = "\\me";
+ literalName[elt_null] = "NULL";
+ foreach (var tpl in f_phys_ptr_cast.Apps) {
+ if (tpl.Args[0] == elt_null)
+ literalName[tpl.Result] = "(" + TypeName(tpl.Args[1]) + "*)NULL";
+ }
+ foreach (var tpl in f_spec_ptr_cast.Apps) {
+ if (tpl.Args[0] == elt_null)
+ literalName[tpl.Result] = "(" + TypeName(tpl.Args[1]) + "^)NULL";
+ }
+ foreach (var fn in model.Functions) {
+ if (fn.Arity == 0 && fn.Name.StartsWith("l#"))
+ literalName[fn.GetConstant()] = ":" + fn.Name.Substring(2);
+ }
+
+ DecodeFileNames();
+ ComputeLocalVariableNames();
+
+ foreach (var s in m.States) {
+ var sn = new StateNode(this, s);
+ sn.SetupVars();
+ states.Add(sn);
+ }
+
+ var allStates = states.ToArray();
+ if (allStates.Length == 1 && allStates[0].vars.Count == 0) {
+ throw new Exception("This VCC model doesn't contain any variables. Was it saved with the -bvd option?");
+ }
+ states.Clear();
+ var i = 0;
+ while (i < allStates.Length) {
+ var lastGoodName = allStates[i].State.Name;
+
+ var userVars = new HashSet<string>(allStates[i].State.Variables.Where(localVariableNames.ContainsKey));
+ i++;
+ while (i < allStates.Length) {
+ foreach (var v in allStates[i].State.Variables) {
+ if (v == "$s" || userVars.Contains(v)) goto stop;
+ if (localVariableNames.ContainsKey(v))
+ userVars.Add(v);
+ }
+
+ var curName = TryParseSourceLocation(allStates[i].State.Name);
+ if (!IsBadName(curName))
+ lastGoodName = allStates[i].State.Name;
+ i++;
+ }
+
+ stop:
+
+ var lastState = allStates[i - 1];
+ lastState.capturedStateName = lastGoodName;
+ lastState.index = states.Count;
+ states.Add(lastState);
+ lastState.SetupVars();
+ }
+
+ foreach (var s in states) {
+ var elt = s.State.TryGet("$s");
+ if (elt != null)
+ literalName[elt] = "\\state'" + s.index;
+ }
+
+ GenerateSourceLocations(states);
+ }
+
+
+ bool IsBadName(SourceLocation l)
+ {
+ return l == null || l.Filename.StartsWith("<");
+ }
+
+ private void ComputeLocalVariableNames()
+ {
+ var vars = model.States.SelectMany(s => s.Variables).Where(v => v != null).Distinct();
+ Func<string, string> simpleName = s => { string dummy; return GetUserVariableNameCore(s, out dummy); };
+ var userVars = vars.Where(s => simpleName(s) != null);
+ var conflictsName = Conflicts(userVars, simpleName).ToArray();
+ Func<string, string> qName = s => { string kind, n = GetUserVariableNameCore(s, out kind); return n + " (" + kind + ")"; };
+ var conflictsKind = Conflicts(conflictsName, qName).ToArray();
+
+ var conflictsNameH = new HashSet<string>(conflictsName);
+ var conflictsKindH = new HashSet<string>(conflictsKind);
+
+ foreach (var v in userVars) {
+ if (conflictsKindH.Contains(v)) continue;
+ if (conflictsNameH.Contains(v))
+ localVariableNames[v] = qName(v);
+ else
+ localVariableNames[v] = simpleName(v);
+ }
+
+ var idx = 0;
+ foreach (var v in conflictsKind) {
+ localVariableNames[v] = string.Format("{0} #{1}", qName(v), idx++);
+ }
+ }
+
+ static IEnumerable<A> Conflicts<A, B>(IEnumerable<A> input, Func<A, B> f)
+ {
+ var revMap = new Dictionary<B, A>();
+ var reported = new HashSet<A>();
+
+ foreach (var k in input) {
+ if (reported.Contains(k)) continue;
+ var v = f(k);
+ A tmp;
+ if (revMap.TryGetValue(v, out tmp) && !tmp.Equals(k)) {
+ if (!reported.Contains(tmp)) {
+ yield return tmp;
+ reported.Add(tmp);
+ }
+ yield return k;
+ reported.Add(k);
+ } else {
+ revMap[v] = k;
+ }
+ }
+ }
+
+ #region Function name scoring
+ static string[][] prefixes = new string[][] {
+ new string[] { "F#", "$eq.$map", "Q#", },
+ new string[] { "F#lambda", },
+ new string[] { "$int_to_", "lambda@", "distinct-aux-f", "Select_","Store_", "$select.", "$store.", },
+ };
+
+ static string[][] totals = new string[][] {
+ new string[] {
+ "$current_timestamp",
+ "$full_stop", "$function_entry", "$ptr_to_i4",
+ "$ptr_to_i8", "$ptr_to_u4", "$ptr_to_u8",
+ "$span", "$sizeof", "$in_domain",
+ "$inv2",
+ "$is_claimable",
+ "$set_cardinality", "$set_difference", "$set_union",
+ "$thread_local", "$unchecked", "$writes_at",
+ "$array_range", "$arrays_disjoint",
+ "$byte_ptr_subtraction",
+ },
+
+ new string[] {
+ "$addr", "$dot", "$emb0", "$fetch_from_domain", "$in_range_phys_ptr",
+ "$in_range_spec_ptr", "$is_sequential_field", "$is_volatile_field",
+ "$is_ghost_field", "$is_phys_field", "$is_math_type", "$invok_state",
+ "$is_primitive",
+ "$spec_ptr_cast",
+ "$phys_ptr_cast",
+ "$is_null",
+ "$in_domain_lab",
+ "$inv_lab",
+ "$set_in0",
+ },
+
+ new string[] {
+ "$_pow2", "$as_composite_field", "$as_field_with_type", "$as_in_range_t",
+ "$as_primitive_field", "$base", "$call_transition", "tickleBool", "Ctor",
+ "$mv_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
+ "$field_parent_type", "$field_type", "$file_name_is", "$good_state",
+ "$good_state_ext", "$function_arg_type", "$has_field_at0", "$map_domain",
+ "$map_range", "$map_t", "$ptr_to", "$ptr_to_i1", "$ptr_to_i2",
+ "$ptr_to_u1", "$ptr_to_u2", "$is_unwrapped", "$is_unwrapped_dynamic",
+ "$heap", "$closed", "$owner", "$owns", "$modifies", "$post_unwrap",
+ "$pow2", "$pre_unwrap", "$ptr", "$is", "$in_range_t", "$roots",
+ "$timestamp", "$type_branch", "$type_code_is", "$type_project_0",
+ "$typemap", "$set_in_pos", "$updated_owns", "$ver_domain", "$vs_state",
+ "$set_singleton",
+ "$f_owner", "$f_closed", "$f_timestamps",
+ "$local_value_is",
+ "$field_arr_ctor",
+ "$idx",
+ },
+ };
+
+ string[] state_props = new string[] { };
+
+ Dictionary<string, int> functionScores = new Dictionary<string, int>();
+
+ int FunctionScore(string name)
+ {
+ if (functionScores.Count == 0) {
+ for (int i = 0; i < totals.Length; ++i)
+ foreach (var s in totals[i])
+ functionScores[s] = i;
+ }
+
+ int res;
+ if (functionScores.TryGetValue(name, out res))
+ return res;
+
+ res = -1;
+ if (name[0] == '$' && name.EndsWith("_to_int"))
+ res = 1;
+ else if (name.EndsWith("#frame"))
+ res = 2;
+ else if (name.Contains("#limited#"))
+ res = 2;
+ else {
+ for (int i = 0; i < prefixes.Length; ++i)
+ foreach (var p in prefixes[i])
+ if (name.StartsWith(p)) {
+ res = i;
+ //goto stop;
+ }
+ //stop: ;
+ }
+
+ if (res == -1)
+ res = 1; // default
+
+ functionScores[name] = res;
+ return res;
+ }
+ #endregion
+
+ private void DecodeFileNames()
+ {
+ var fis = model.GetFunc("$file_name_is");
+ foreach (var f in model.Functions) {
+ if (f.Arity == 0 && f.Name.StartsWith("#file^")) {
+ var sb = new StringBuilder();
+ var idx = 6;
+ var name = f.Name;
+ while (idx < name.Length) {
+ if (name[idx] == '?') {
+ var c = (char)Int32.Parse(name.Substring(idx + 1, 2), System.Globalization.NumberStyles.HexNumber);
+ sb.Append(c);
+ idx += 3;
+ } else {
+ sb.Append(name[idx++]);
+ }
+ }
+ name = sb.ToString();
+
+ foreach (var app in fis.AppsWithArg(1, f.GetConstant()))
+ fileNameMapping[app.Args[0].AsInt()] = name;
+ }
+ }
+ }
+
+ private Model.Element DecodeDT(string dt)
+ {
+ if (dt.StartsWith("dt")) {
+ var tpName = dt.Replace("dt", "#distTp");
+ var f = model.TryGetFunc(tpName);
+ if (f != null) {
+ return f.GetConstant();
+ //var res = f_type_project_0.TryEval(ptr);
+ //if (res != null)
+ // tp = res;
+ }
+ }
+ return null;
+ }
+
+ private string DecodeToken(string name, ref Model.Element tp)
+ {
+ var idx = name.LastIndexOf("$");
+ if (idx < 0) return null;
+ var words = name.Substring(idx + 1).Split('.', '^', '!', '#', '@');
+ if (words.Length > 3)
+ tp = DecodeDT(words[3]);
+ return string.Format("{0}({1},{2})", fileNameMapping[int.Parse(words[0])], words[1], words[2]);
+ }
+
+ public string GetUserVariableName(string name)
+ {
+ string res;
+ localVariableNames.TryGetValue(name, out res);
+ return res;
+ }
+
+
+ string GetUserVariableNameCore(string name, out string kind)
+ {
+ if (name.StartsWith("L#")) {
+ kind = "local";
+ return name.Substring(2);
+ }
+
+ if (name.StartsWith("P#")) {
+ kind = "in-param";
+ return name.Substring(2);
+ }
+
+ if (name.StartsWith("OP#")) {
+ kind = "out-param";
+ return name.Substring(3);
+ }
+
+ if (name.StartsWith("SL#")) {
+ kind = "spec local";
+ return name.Substring(3);
+ }
+
+ if (name.StartsWith("SP#")) {
+ kind = "spec in-param";
+ return name.Substring(3);
+ }
+
+ if (name.StartsWith("local.")) {
+ kind = "param copied to local";
+ return name.Substring(6);
+ }
+
+ if (name.StartsWith("addr.")) {
+ kind = "stack-allocated struct";
+ return name.Substring(5);
+ }
+
+ if (name == "$result") {
+ kind = "function return value";
+ return "\\result";
+ }
+
+ if (name.StartsWith("res__") && viewOpts.ViewLevel >= 1) {
+ kind = "call result";
+ return name;
+ }
+
+ if (name == "$s" && viewOpts.ViewLevel >= 1) {
+ kind = "current state";
+ return "\\now";
+ }
+
+ kind = null;
+ return null;
+ }
+
+
+ private string LiteralName(Model.Element elt)
+ {
+ string r;
+
+ if (literalName.TryGetValue(elt, out r))
+ return r;
+
+ r = TryTypeName(elt);
+ if (r != null) {
+ literalName[elt] = r;
+ return r;
+ }
+
+ var i = elt as Model.Integer;
+ if (i != null)
+ return AsPow2(i);
+
+ var bv = elt as Model.BitVector;
+ if (bv != null)
+ return bv.Numeral + "bv" + bv.Size.ToString();
+
+ return null;
+ }
+
+ public Model.Element LocalType(string localName)
+ {
+ string dummy;
+ var v = GetUserVariableNameCore(localName, out dummy);
+ if (v == null) v = localName;
+ var c = model.TryGetFunc("#loc." + v);
+ if (c != null) {
+ var localIs = f_local_value_is.AppWithArg(2, c.GetConstant());
+ if (localIs != null)
+ return localIs.Args[4];
+ }
+ foreach (var s in model.States.Reverse()) {
+ var val = s.TryGet(localName);
+ var tp = GuessType(val);
+ if (tp != tp_mathint)
+ return tp;
+ }
+ return tp_mathint;
+ }
+
+ public Model.Element Image(Model.Element elt, Model.Func f)
+ {
+ var r = f.AppWithResult(elt);
+ if (r != null)
+ return r.Args[0];
+ return null;
+ }
+
+ string TypeNameCore(Model.Element elt)
+ {
+ var deref = Image(elt, f_ptr_to);
+ if (deref != null)
+ return TypeName(deref) + "*";
+ deref = Image(elt, f_spec_ptr_to);
+ if (deref != null)
+ return TypeName(deref) + "^";
+ deref = Image(elt, f_blob_type);
+ if (deref != null)
+ return "_(blob " + CanonicalName(deref) + ")";
+ var mapt = f_map_t.AppWithResult(elt);
+ if (mapt != null)
+ return string.Format("{1}[{0}]", TypeName(mapt.Args[0]), TypeName(mapt.Args[1]));
+
+ var arr = f_array.AppWithResult(elt);
+ if (arr != null) {
+ return string.Format("{0}[{1}]", TypeName(arr.Args[0]), arr.Args[1].ToString());
+ }
+
+ foreach (var app in elt.Names)
+ if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^")) {
+ var n = app.Func.Name.Substring(1);
+ switch (n) {
+ case "^i1": return "int8_t";
+ case "^u1": return "uint8_t";
+ case "^i2": return "int16_t";
+ case "^u2": return "uint16_t";
+ case "^i4": return "int32_t";
+ case "^u4": return "uint32_t";
+ case "^i8": return "int64_t";
+ case "^u8": return "uint64_t";
+ case "^bool": return "bool";
+ default:
+ var pref = "_vcc_math_type_";
+ if (n.StartsWith(pref)) n = n.Substring(pref.Length);
+ return n;
+ }
+ }
+
+ return null;
+ }
+
+ public string TypeName(Model.Element elt)
+ {
+ var r = TryTypeName(elt);
+ if (r == null)
+ return elt.ToString();
+ else return r;
+ }
+
+ public string TryTypeName(Model.Element elt)
+ {
+ string res;
+ if (!typeName.TryGetValue(elt, out res)) {
+ typeName[elt] = elt.ToString(); // avoid infinite recursion
+ res = TypeNameCore(elt);
+ typeName[elt] = res;
+ }
+ return res;
+ }
+
+ public static readonly string[] synthethic_fields = new string[] { "$f_owns", "$f_ref_cnt", "$f_vol_version", "$f_root", "$f_group_root", "$f_active_option" };
+
+ public string ConstantFieldName(Model.Element elt)
+ {
+ string res;
+ IsConstantField(elt, out res);
+ return res;
+ }
+
+ public bool IsConstantField(Model.Element elt)
+ {
+ string dummy;
+ return IsConstantField(elt, out dummy);
+ }
+
+ public bool IsConstantField(Model.Element elt, out string theName)
+ {
+ var bestScore = int.MinValue;
+ string bestName = null;
+
+ foreach (var t in elt.Names) {
+ var score = int.MinValue;
+ string name = null;
+ if (t.Args.Length == 0) {
+ name = t.Func.Name;
+ score = 0;
+ var dotIdx = name.IndexOf('.');
+ if (dotIdx > 0) {
+ score += 10;
+ name = name.Substring(dotIdx + 1);
+ }
+ if (name.Contains('#')) score -= 1;
+ } else if (t.Func.Name.StartsWith("$f_") && synthethic_fields.Contains(t.Func.Name)) {
+ name = string.Format("{0}<{1}>", t.Func.Name.Substring(3).Replace("root", "alloc_root"), TypeName(t.Args[0]));
+ score = 6;
+ } else if (t.Func == f_array_emb) {
+ name = string.Format("[0] (of {0}[{1}])", TypeName(t.Args[0]), t.Args[1].ToString());
+ score = 5;
+ }
+ if (score > bestScore) {
+ bestScore = score;
+ bestName = name;
+ }
+ }
+
+ theName = bestName;
+ return bestScore >= 5;
+ }
+
+ bool IsSomeState(Model.Element elt)
+ {
+ var tp = GuessType(elt);
+ return tp == tp_state || tp == tp_heaptp;
+ }
+
+ bool IsThisState(Model.Element st, Model.Element elt)
+ {
+ return elt == st || elt == f_heap.TryEval(st);
+ }
+
+ Model.Element GuessType(Model.Element element)
+ {
+ Model.Element res;
+ if (!guessedType.TryGetValue(element, out res)) {
+ res = GuessTypeCore(element);
+ guessedType[element] = res;
+ }
+ return res;
+ }
+
+ Model.Element GuessTypeCore(Model.Element element)
+ {
+ if (element is Model.Boolean)
+ return tp_bool;
+
+ var fld = f_field.TryEval(element);
+ if (fld != null) {
+ var tp = f_field_type.TryEval(fld);
+ if (tp != null) {
+ var ptp = f_ptr_to.TryEval(tp);
+ if (ptp != null)
+ return ptp;
+ ptp = f_spec_ptr_to.TryEval(tp);
+ if (ptp != null)
+ return ptp;
+ }
+ return tp_object;
+ }
+
+ foreach (var tpl in element.References) {
+ if (element == tpl.Result) {
+ if (tpl.Func == f_ptr)
+ return tp_object;
+ if (tpl.Func == f_heap)
+ return tp_heaptp;
+ }
+
+ if (tpl.Args.Length >= 1 && tpl.Args[0] == element) {
+ if (tpl.Func == f_heap || tpl.Func == f_closed || tpl.Func == f_good_state)
+ return tp_state;
+ }
+
+ if (tpl.Func == f_select_bool)
+ if (tpl.Args[0] == element)
+ return tp_ptrset;
+ else if (tpl.Args[1] == element)
+ return tp_object;
+
+ var fname = tpl.Func.Name;
+
+ if (tpl.Args.Length == 2 && tpl.Args[0] == element && fname.StartsWith("$select.$map_t")) {
+ var mt = model.TryGetFunc("MT#" + fname);
+ if (mt != null && mt.Arity == 0)
+ return mt.GetConstant();
+ var t1 = GuessType(tpl.Args[1]);
+ var t2 = GuessType(tpl.Result);
+ var t = f_map_t.TryEval(t1, t2);
+ if (t != null)
+ return t;
+ }
+
+ var tpName = DataTypeName(element, tpl);
+ if (tpName != null) {
+ var tp = model.TryGetFunc("^$#" + tpName);
+ if (tp != null)
+ return tp.GetConstant();
+ }
+ }
+
+ return tp_mathint;
+ }
+
+ string DataTypeName(Model.Element elt, Model.FuncTuple tpl)
+ {
+ var fname = tpl.Func.Name;
+ if (tpl.Args.Length == 1 && tpl.Args[0] == elt && fname.StartsWith("RF#")) {
+ var fldName = tpl.Func.Name.Substring(3);
+ var idx = fldName.LastIndexOf('.');
+ if (idx > 0) {
+ return fldName.Substring(0, idx).Replace("_vcc_math_type_", "");
+ }
+ }
+
+ if (tpl.Args.Length == 1 && tpl.Args[0] == elt && (fname.StartsWith("DSZ#") || fname.StartsWith("RSZ#") || fname.StartsWith("DGH#"))) {
+ return fname.Substring(4).Replace("_vcc_math_type_", "");
+ }
+ return null;
+ }
+
+ public DataKind GetKind(Model.Element tp, out Model.FuncTuple tpl)
+ {
+ tpl = null;
+
+ if (tp == tp_object)
+ return DataKind.Object;
+ else if (tp == tp_ptrset)
+ return DataKind.Ptrset;
+
+ tpl = f_ptr_to.AppWithResult(tp);
+ if (tpl != null) return DataKind.PhysPtr;
+ tpl = f_spec_ptr_to.AppWithResult(tp);
+ if (tpl != null) return DataKind.SpecPtr;
+ tpl = f_map_t.AppWithResult(tp);
+ if (tpl != null) return DataKind.Map;
+
+ return DataKind.Flat;
+ }
+
+ public DataKind GetKind(Model.Element tp)
+ {
+ Model.FuncTuple dummy;
+ return GetKind(tp, out dummy);
+ }
+
+
+ public Model.Element WrapForUse(Model.Element elt, Model.Element tp)
+ {
+ Model.FuncTuple tpl;
+ var kind = GetKind(tp, out tpl);
+
+ if (kind == DataKind.Flat) {
+ if (elt.Kind == Model.ElementKind.Integer) {
+ var tpname = TypeName(tp);
+ if(tpname.StartsWith("$")) tpname = tpname.Substring(1);
+ if (tpname.StartsWith("#")) {
+ foreach (var tupl in elt.References) {
+ if (tupl.Args.Length == 1 && tupl.Args[0] == elt && tupl.Func.Name.StartsWith("$int_to_") && tupl.Func.Name.EndsWith(tpname)) {
+ return tupl.Result;
+ }
+ }
+ }
+ }
+ return elt;
+ }
+
+ if (kind == DataKind.Map) {
+ if (elt.Kind == Model.ElementKind.Integer) {
+ Model.Element theMap = null;
+ foreach (var conv in model.Functions)
+ // really, we should reconstruct the name of this function, but this is painful
+ if (conv.Arity == 1 && conv.Name.StartsWith("$int_to_map_t")) {
+ var app = conv.AppWithArg(0, elt);
+ if (app != null) {
+ theMap = app.Result;
+ break;
+ }
+ }
+ if (theMap == null) return elt;
+ return theMap;
+ }
+ return elt;
+ } else if (kind == DataKind.Ptrset) {
+ var tmp = f_int_to_ptrset.TryEval(elt);
+ if (tmp != null)
+ return tmp;
+ return elt;
+ }
+
+ if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr || kind == DataKind.Object) {
+ if (elt.Kind == Model.ElementKind.Integer) {
+ var tmp = f_int_to_ptr.TryEval(elt);
+ if (tmp != null)
+ elt = tmp;
+ }
+ }
+
+ if (kind == DataKind.Object)
+ return elt;
+
+ if (kind == DataKind.PhysPtr)
+ return Util.OrElse(f_phys_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
+
+ if (kind == DataKind.SpecPtr)
+ return Util.OrElse(f_spec_ptr_cast.TryEval(elt, tpl.Args[0]), elt);
+
+ Util.Assert(false);
+ return elt;
+ }
+
+ void AddSpecialField(StateNode state, Model.Element elt, List<ElementNode> res, string name, Model.Func select_map)
+ {
+ if (elt == null) return;
+
+ var map = state.State.TryGet("$s");
+ if (map != null)
+ map = select_map.TryEval(map);
+ if (map != null) {
+ var model = elt.Model;
+ Model.Element val = f_select_bool.TryEval(map, elt);
+ Model.Element tp = tp_bool;
+ if (val == null) {
+ val = f_select_ptr.TryEval(map, elt);
+ tp = tp_object;
+ }
+ if (val == null) {
+ val = f_select_int.TryEval(map, elt);
+ tp = tp_mathint;
+ }
+ if (val != null) {
+ res.Add(new FieldNode(state, new EdgeName(name), val, tp) { Category = NodeCategory.MethodologyProperty });
+ }
+ }
+ }
+
+ void AddPointerFunction(StateNode state, Model.Element elt, List<ElementNode> res, string name, Model.Func fn, Model.Element tp)
+ {
+ if (elt == null) return;
+
+ var val = fn.TryEval(elt);
+ if (val != null) {
+ res.Add(new FieldNode(state, new EdgeName(name), val, tp) { Category = NodeCategory.MethodologyProperty });
+ }
+ }
+
+ void AddPtrType(StateNode state, Model.Element elt, List<ElementNode> res)
+ {
+ var f = f_field.TryEval(elt);
+ if (f == null) return;
+
+ var tp = f_field_type.TryEval(f);
+
+ var seq = "";
+
+ var is_seq = f_is_sequential_field.TryEval(f) as Model.Boolean;
+ var is_vol = f_is_volatile_field.TryEval(f) as Model.Boolean;
+
+ if (is_seq != null && is_vol != null && is_seq.Value == is_vol.Value) {
+ seq = " (volatile/sequential mismatch)";
+ } else if ((is_seq != null && is_seq.Value) || (is_vol != null && !is_vol.Value)) {
+ seq = " (sequential)";
+ } else if ((is_seq != null && !is_seq.Value) || (is_vol != null && is_vol.Value)) {
+ seq = " (volatile)";
+ }
+
+ if (tp != null || seq != "") {
+ res.Add(new FieldNode(state, new EdgeName("\\typeof" + seq), tp, tp_mathint) { Category = NodeCategory.MethodologyProperty });
+ }
+ }
+
+ string SkolemName(Model.Func f, ref Model.Element tp)
+ {
+ if (f.Name.IndexOf('!') > 0) {
+ var tok = DecodeToken(f.Name, ref tp);
+ if (tok != null) {
+ var baseName = f.Name.Substring(0, f.Name.LastIndexOf('$'));
+ if (baseName.StartsWith("Q#"))
+ baseName = baseName.Substring(2);
+ return string.Format("{0}@{1}", baseName, ShortenToken(tok, 10, false));
+ }
+ }
+ return null;
+ }
+
+ string GlobalName(Model.Func f, ref Model.Element tp)
+ {
+ if (f.Name.StartsWith("G#")) {
+ var idx = f.Name.LastIndexOf("#dt");
+ if (idx < 0) return null;
+ var name = f.Name.Substring(2, idx - 2);
+ tp = DecodeDT(f.Name.Substring(idx + 1));
+ return string.Format("::{0}", name);
+ }
+ return null;
+ }
+
+
+ public IEnumerable<ElementNode> CommonNodes(StateNode state)
+ {
+ var skolems = new List<ElementNode>();
+
+ Model.Element tp = null;
+
+ foreach (var f in model.Functions) {
+ if (f.Arity != 0) continue;
+ var s = SkolemName(f, ref tp);
+ if (s == null)
+ s = GlobalName(f, ref tp);
+ if (s != null) {
+ if (tp == null)
+ tp = GuessType(f.GetConstant());
+ var val = WrapForUse(f.GetConstant(), tp);
+ skolems.Add(new VariableNode(state, s, val, tp));
+ }
+ }
+
+ return skolems;
+ }
+
+ private Model.Element GuessPtrTo(Model.Element tp)
+ {
+ var p = f_ptr_to.TryEval(tp);
+ if (p != null) return p;
+ p = f_spec_ptr_to.TryEval(tp);
+ if (p != null) return p;
+ var nm = model.MkFunc("*ptrto_" + TypeName(tp), 0).GetConstant();
+ f_ptr_to.AddApp(nm, tp);
+ return f_ptr_to.TryEval(tp);
+ }
+
+ private Model.Element PtrTo(Model.Element tp, Model.Func f_ptr_to)
+ {
+ var p = f_ptr_to.TryEval(tp);
+ if (p != null) return p;
+ var nm = model.MkFunc("*" + f_ptr_to.Name + "_" + TypeName(tp), 0).GetConstant();
+ f_ptr_to.AddApp(nm, tp);
+ return f_ptr_to.TryEval(tp);
+ }
+
+ private bool IsArrayField(Model.Element ptr)
+ {
+ return ptr != null && f_idx.TryEval(ptr, model.TryMkElement("0")) != null;
+ }
+
+ public IEnumerable<ElementNode> GetExpansion(StateNode state, Model.Element elt, Model.Element tp)
+ {
+ List<ElementNode> result = new List<ElementNode>();
+ Model.FuncTuple tpl;
+
+ if (elt == null) return result;
+
+ var kind = GetKind(tp, out tpl);
+ if (kind == DataKind.PhysPtr || kind == DataKind.SpecPtr || kind == DataKind.Object) {
+ var heap = state.State.TryGet("$s");
+ if (heap != null)
+ heap = f_heap.TryEval(heap);
+ var addresses = new HashSet<Model.Element>();
+
+ if (heap != 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_dot.TryEval(elt, field);
+ if (addr != null) addresses.Add(addr);
+ var node = ComputeUnionActiveOption(state, elt, val, field);
+ if (node != null)
+ result.Add(node);
+ else
+ BuildFieldNode(result, state, addr, field, val, addr);
+ }
+ }
+ //result.Sort(CompareFields);
+ }
+
+ {
+ foreach (var app in f_idx.AppsWithArg(0, elt)) {
+ var addr = app.Result;
+ Model.Element val = null, atp = tp;
+
+ addresses.Add(addr);
+
+ 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[1]);
+ if (tt != null) atp = tt;
+ }
+ }
+
+ if (val != null)
+ val = WrapForUse(val, atp);
+ result.Add(new MapletNode(state, new EdgeName(this, "[%0]", app.Args[1]), val, atp) { Category = NodeCategory.Maplet });
+ if (addr != null)
+ result.Add(new MapletNode(state, new EdgeName(this, "&[%0]", app.Args[1]), addr, GuessPtrTo(atp)) { Category = NodeCategory.Maplet });
+ }
+ }
+
+ foreach (var ptr in f_dot.AppsWithArg(0, elt)) {
+ if (addresses.Contains(ptr.Result)) continue;
+ 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[1])) continue;
+ BuildFieldNode(result, state, ptr.Result, ptr.Args[1], null, ptr.Result);
+ }
+
+ AddSpecialField(state, elt, result, "\\closed", f_closed);
+ 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_prim_emb, tp_object);
+ AddPointerFunction(state, elt, result, "\\addr", f_addr, tp_mathint);
+
+ if (viewOpts.ViewLevel >= 1) {
+ AddPtrType(state, elt, result);
+ AddCasts(state, elt, result);
+ var sets = new SetsNode(state, elt);
+ if (!sets.IsEmpty)
+ result.Add(sets);
+ }
+
+ } else if (kind == DataKind.Map) {
+ var elTp = tpl.Args[1];
+ foreach (var sel in model.Functions)
+ if (sel.Arity == 2 && sel.Name.StartsWith("$select.$map_t")) {
+ foreach (var app in sel.AppsWithArg(0, elt)) {
+ var val = WrapForUse(app.Result, elTp);
+ var edgname = new EdgeName(this, "[%0]", app.Args[1]);
+ result.Add(new MapletNode(state, edgname, val, elTp) { Category = NodeCategory.Maplet });
+ }
+ }
+ } else if (kind == DataKind.Ptrset) {
+ foreach (var sel in f_select_bool.AppsWithArg(0, elt)) {
+ var edgname = new EdgeName(this, "[%0]", sel.Args[1]);
+ result.Add(new MapletNode(state, edgname, sel.Result, tp_bool) { Category = NodeCategory.Maplet });
+ }
+ } else if (kind == DataKind.Flat) {
+ foreach (var tupl in elt.References) {
+ if (tupl.Args.Length == 1 && tupl.Args[0] == elt) {
+ var fname = tupl.Func.Name;
+ var idx = fname.LastIndexOf('.');
+ if (fname.StartsWith("RF#") && idx > 0) {
+ fname = fname.Substring(idx + 1);
+ } else if (fname.StartsWith("DP#p")) {
+ fname = fname.Substring(4);
+ idx = fname.IndexOf('#');
+ if (idx > 0)
+ fname = fname.Substring(idx + 1) + "#" + fname.Substring(0, idx);
+ } else {
+ fname = null;
+ }
+
+ if (fname != null)
+ result.Add(new FieldNode(state, new EdgeName(fname), tupl.Result, GuessType(tupl.Result)) { Category = NodeCategory.SpecField });
+ }
+ }
+ }
+
+ if (!(elt is Model.Boolean)) {
+ var curState = state.State.TryGet("$s");
+
+ foreach (var tupl in elt.References) {
+ {
+ var seenSelf = false;
+ var seenState = false;
+ var seenThisState = false;
+ var args = tupl.Args;
+ for (int i = 0; i < args.Length; ++i) {
+ if (args[i] == elt) seenSelf = true;
+ if (IsThisState(curState, args[i])) seenThisState = true;
+ else if (IsSomeState(args[i])) seenState = true;
+ }
+ if (!seenSelf) continue; // not looking for aliases (maybe we should?)
+ if (seenState && !seenThisState) continue;
+ }
+
+ var argsFmt = new StringBuilder();
+ var name = tupl.Func.Name;
+
+ var score = FunctionScore(name);
+ if (score >= viewOpts.ViewLevel)
+ continue;
+
+ var retTp = GuessType(tupl.Result);
+ var retVal = tupl.Result;
+
+ var cat = NodeCategory.MethodologyProperty;
+ if (name.StartsWith("F#")) {
+ name = name.Substring(2);
+ cat = NodeCategory.UserFunction;
+ }
+
+ if (name.StartsWith("DF#")) {
+ name = name.Substring(3);
+ cat = NodeCategory.UserFunction;
+ }
+
+ if (name.StartsWith("$eq.$"))
+ name = "EQ";
+
+ {
+ Model.Element sktp = null;
+ var sk = SkolemName(tupl.Func, ref sktp);
+ if (sk != null) {
+ name = sk;
+ if (sktp != null)
+ retVal = WrapForUse(tupl.Result, sktp);
+ cat = NodeCategory.Maplet;
+ }
+ }
+
+ {
+ argsFmt.Append(name).Append("(");
+ var args = new List<Model.Element>();
+ foreach (var a in tupl.Args) {
+ if (IsThisState(curState, a))
+ argsFmt.Append("\\now, ");
+ else if (a == elt)
+ argsFmt.Append(selfMarker + ", ");
+ else {
+ argsFmt.AppendFormat("%{0}, ", args.Count);
+ args.Add(a);
+ }
+ }
+ argsFmt.Length -= 2;
+ argsFmt.Append(")");
+ var edgeName = new EdgeName(this, argsFmt.ToString(), args.ToArray());
+ result.Add(new MapletNode(state, edgeName, retVal, retTp) { ViewLevel = score, Category = cat });
+ }
+
+ }
+ }
+
+ return result;
+ }
+
+ 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_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 };
+ return fieldNode;
+ }
+ }
+ return null;
+ }
+
+ private void AddCasts(StateNode state, Model.Element elt, List<ElementNode> result)
+ {
+ foreach (var app in f_phys_ptr_cast.AppsWithArg(0, elt)) {
+ if (app.Result != elt)
+ result.Add(new MapletNode(state, new EdgeName(this, "(" + TypeName(app.Args[1]) + "*)..."), app.Result, PtrTo(app.Args[1], f_ptr_to)));
+ }
+ foreach (var app in f_spec_ptr_cast.AppsWithArg(0, elt)) {
+ if (app.Result != elt)
+ result.Add(new MapletNode(state, new EdgeName(this, "(" + TypeName(app.Args[1]) + "^)..."), app.Result, PtrTo(app.Args[1], f_spec_ptr_to)));
+ }
+ var addr = f_addr.TryEval(elt);
+ if (addr != null) {
+ foreach (var app in f_blob_type.Apps) {
+ var blob = f_address_root.TryEval(addr, app.Result);
+ if (blob != null) {
+ result.Add(new MapletNode(state, new EdgeName(this, TypeName(app.Result) + "..."), blob, app.Result));
+ }
+ }
+ }
+ }
+
+ private void BuildFieldNode(List<ElementNode> result, StateNode state, Model.Element ptr, Model.Element field, Model.Element val, Model.Element addr)
+ {
+ var ftp = f_field_type.TryEval(field);
+ if (val != null)
+ val = WrapForUse(val, ftp);
+
+ if (IsArrayField(ptr)) {
+ val = addr;
+ addr = null;
+ ftp = GuessPtrTo(ftp);
+ }
+
+ var nm = ConstantFieldName(field);
+ var edgname = nm == null ? field.ToString() : nm;
+
+ var cat = NodeCategory.PhysField;
+ if (f_is_ghost_field.IsTrue(field))
+ cat = NodeCategory.SpecField;
+ if (nm != null && nm.Contains("<"))
+ cat = NodeCategory.MethodologyProperty;
+
+ var fieldNode = new FieldNode(state, new EdgeName(edgname), val, ftp) { Category = cat};
+ result.Add(fieldNode);
+
+ if (addr != null) {
+ result.Add(new FieldNode(state, new EdgeName("&" + edgname), addr, GuessPtrTo(ftp)) { Category = cat });
+ }
+ }
+
+ public override IEnumerable<IState> States
+ {
+ get
+ {
+ return states;
+ }
+ }
+
+ private int DataTypeToString(StringBuilder sb, int level, Model.Element elt)
+ {
+ Model.FuncTuple ctor = null;
+ int len = 1;
+ string dataTypeType = null;
+ foreach (var app in elt.References) {
+ var n = app.Func.Name;
+ if (app.Result == elt && n.StartsWith("DF#")) {
+ ctor = app;
+ }
+ var tmp = DataTypeName(elt, app);
+ if (tmp != null) dataTypeType = tmp;
+ }
+
+ if (dataTypeType != null) {
+ if (ctor != null)
+ sb.Append(ctor.Func.Name.Substring(3));
+ else
+ sb.Append(DataTypeShortName(elt, dataTypeType));
+ if (ctor != null && ctor.Args.Length > 0) {
+ if (level <= 0) sb.Append("(...)");
+ else {
+ sb.Append("(");
+ for (int i = 0; i < ctor.Args.Length; ++i) {
+ if (i != 0) sb.Append(", ");
+ len += DataTypeToString(sb, level - 1, ctor.Args[i]);
+ }
+ sb.Append(")");
+ }
+ }
+ } else {
+ sb.Append(CanonicalName(elt));
+ }
+ return len;
+ }
+
+ private string DataTypeShortName(Model.Element elt, string tp)
+ {
+ var baseName = tp;
+
+ var hd = model.MkFunc("DGH#" + tp, 1).TryEval(elt);
+ if (hd != null) {
+ foreach (var nm in hd.References) {
+ if (nm.Func.Arity == 0 && nm.Func.Name.StartsWith("DH#"))
+ baseName = nm.Func.Name.Substring(3);
+ }
+ }
+
+ return baseName;
+ }
+
+ private string CanonicalBaseNameCore(string name, Model.Element elt, bool doDatatypes, ref NameSeqSuffix suff)
+ {
+ var vm = this;
+
+ if (name.Contains("[") || name.Contains("'"))
+ name = "";
+
+ if (name != "")
+ return name;
+
+ var isNull = false;
+ foreach (var tpl in elt.References) {
+ var fn = tpl.Func;
+ if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)
+ return "map";
+ if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)
+ return "map";
+
+ if (fn.Arity >= 1 && tpl.Args[0] == elt) {
+ if (fn == f_select_bool)
+ return "ptrset";
+ }
+
+ if (tpl.Result == elt)
+ if (fn == f_int_to_version)
+ return "version";
+
+ if (fn == f_is_null && tpl.Result == model.True)
+ isNull = true;
+
+ var dtpName = DataTypeName(elt, tpl);
+ if (dtpName != null) {
+ var sb = new StringBuilder();
+ string prev = null;
+ datatypeLongName[elt] = "*SELF*"; // in case we recurse (but this shouldn't happen)
+ for (int lev = 0; lev < 10; lev++) {
+ sb.Length = 0;
+ var len = DataTypeToString(sb, lev, elt);
+ if (prev == null || len <= maxDatatypeNameLength)
+ prev = sb.ToString();
+ }
+
+ datatypeLongName[elt] = prev;
+ suff = NameSeqSuffix.WhenNonZero;
+ return prev;
+ }
+ }
+
+ var fld = vm.f_field.TryEval(elt);
+ if (fld != null) {
+ var tp = vm.f_field_type.TryEval(fld);
+ if (tp != null) {
+ var n = vm.TryTypeName(tp);
+ if (n != null) {
+ if (isNull)
+ return "(" + n + "*)NULL";
+ return n;
+ }
+ }
+ }
+
+ return "";
+ }
+
+ protected override string CanonicalBaseName(Model.Element elt, out NameSeqSuffix suff)
+ {
+ var lit = this.LiteralName(elt);
+ if (lit != null) {
+ suff = NameSeqSuffix.None;
+ return lit;
+ }
+ if (datatypeLongName.TryGetValue(elt, out lit)) {
+ suff = NameSeqSuffix.WhenNonZero;
+ return lit;
+ }
+
+ var name = base.CanonicalBaseName(elt, out suff);
+ name = CanonicalBaseNameCore(name, elt, true, ref suff);
+
+ return name;
+ }
+
+ public override string PathName(IEnumerable<IDisplayNode> path)
+ {
+ var sb = new StringBuilder();
+ foreach (var d in path) {
+ var name = d.Name;
+ if (name == "") continue; // can that happen?
+ if (name.Contains("(") && name.Contains(selfMarker)) {
+ var repl = name.Replace(selfMarker, sb.ToString());
+ sb.Length = 0;
+ sb.Append(repl);
+ } else {
+ if (sb.Length > 0 && name[0] != '[')
+ sb.Append("->");
+ sb.Append(d.Name);
+ }
+ }
+
+ return sb.ToString();
+ }
+ }
+
+ class StateNode : NamedState
+ {
+ internal VccModel vm;
+ internal List<VariableNode> vars;
+ internal List<ElementNode> commons;
+ internal int index;
+ internal string capturedStateName;
+
+ public StateNode(VccModel parent, Model.CapturedState s)
+ : base(s, parent)
+ {
+ this.capturedStateName = s.Name;
+ this.vm = parent;
+ }
+
+ internal void SetupVars()
+ {
+ if (vars != null) return;
+ vars = new List<VariableNode>();
+
+ var names = Util.Empty<string>();
+
+ if (vm.states.Count > 0) {
+ var prev = vm.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) {
+ var localName = vm.GetUserVariableName(v);
+ if (localName != null) {
+ var tp = vm.LocalType(v);
+ var val = state.TryGet(v);
+ val = vm.WrapForUse(val, tp);
+ var vn = new VariableNode(this, v, val, tp) { ShortName = localName };
+ vn.updatedHere = vm.states.Count > 0 && curVars.ContainsKey(v);
+ if (curVars.ContainsKey(v))
+ vm.RegisterLocalValue(vn.Name, val);
+ vars.Add(vn);
+ }
+ }
+
+ vm.Flush(vars);
+
+ commons = new List<ElementNode>();
+ commons.AddRange(vm.CommonNodes(this));
+ }
+
+ public override IEnumerable<IDisplayNode> Nodes
+ {
+ get {
+ return vars.Concat(commons);
+ }
+ }
+
+ public override string CapturedStateName
+ {
+ get
+ {
+ return this.capturedStateName;
+ }
+ }
+ }
+
+ class ElementNode : DisplayNode
+ {
+ protected StateNode stateNode;
+ protected Model.Element tp;
+ protected VccModel vm { get { return stateNode.vm; } }
+
+ public ElementNode(StateNode st, EdgeName name, Model.Element elt, Model.Element tp)
+ : base(st.vm, name, elt)
+ {
+ this.stateNode = st;
+ this.tp = tp;
+ }
+
+ protected override void ComputeChildren()
+ {
+ children.AddRange(vm.GetExpansion(stateNode, element, tp));
+ }
+
+ public override string ToolTip
+ {
+ get
+ {
+ var sb = new StringBuilder();
+ if (tp != null)
+ sb.AppendFormat("Type: {0}\n", vm.TypeName(tp));
+ var i = element as Model.Integer;
+ if (i != null) {
+ var n = System.Numerics.BigInteger.Parse(i.Numeral);
+ sb.AppendFormat("Value: {0} (0x{1:x})\n", n, n);
+ } else if (element != null) {
+ sb.AppendFormat("Value: {0}\n", element);
+ }
+ return sb.ToString();
+ }
+ }
+ }
+
+ class SetsNode : ElementNode
+ {
+ List<Model.Element> refs = new List<Model.Element>();
+
+ public SetsNode(StateNode par, Model.Element elt)
+ : base(par, new EdgeName("\\in ..."), null, null)
+ {
+ children = new List<IDisplayNode>();
+ foreach (var app in vm.f_select_bool.AppsWithArg(1, elt)) {
+ children.Add(
+ new MapletNode(par, new EdgeName(vm, VccModel.selfMarker + " \\in %0", app.Args[0]), app.Result, vm.tp_bool) { Category = NodeCategory.MethodologyProperty });
+ refs.Add(app.Args[0]);
+ }
+ Category = NodeCategory.MethodologyProperty;
+ }
+
+ public override IEnumerable<Model.Element> References
+ {
+ get
+ {
+ return refs;
+ }
+ }
+
+ public bool IsEmpty { get { return children.Count == 0; } }
+ }
+
+
+ class FieldNode : ElementNode
+ {
+ public FieldNode(StateNode par, EdgeName realName, Model.Element elt, Model.Element tp)
+ : base(par, realName, elt, tp)
+ {
+ }
+ }
+
+ class MapletNode : ElementNode
+ {
+ public MapletNode(StateNode par, EdgeName 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, new EdgeName(realName), elt, tp)
+ {
+ this.realName = realName;
+ }
+
+ public override string ShortName
+ {
+ set { this.name = new EdgeName(value); }
+ get { return this.name.ToString(); }
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 12:57:43 +0000