From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/ModelViewer/VccProvider.cs | 3052 ++++++++++++++++++------------------- 1 file changed, 1526 insertions(+), 1526 deletions(-) (limited to 'Source/ModelViewer/VccProvider.cs') 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 typeName = new Dictionary(); - Dictionary literalName = new Dictionary(); - Dictionary guessedType = new Dictionary(); - public List states = new List(); - public Dictionary localVariableNames = new Dictionary(); - - Dictionary datatypeLongName = new Dictionary(); - - Dictionary fileNameMapping = new Dictionary(); - - 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(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 simpleName = s => { string dummy; return GetUserVariableNameCore(s, out dummy); }; - var userVars = vars.Where(s => simpleName(s) != null); - var conflictsName = Conflicts(userVars, simpleName).ToArray(); - Func qName = s => { string kind, n = GetUserVariableNameCore(s, out kind); return n + " (" + kind + ")"; }; - var conflictsKind = Conflicts(conflictsName, qName).ToArray(); - - var conflictsNameH = new HashSet(conflictsName); - var conflictsKindH = new HashSet(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 Conflicts(IEnumerable input, Func f) - { - var revMap = new Dictionary(); - var reported = new HashSet(); - - 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 functionScores = new Dictionary(); - - 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 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 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 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 CommonNodes(StateNode state) - { - var skolems = new List(); - - 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 GetExpansion(StateNode state, Model.Element elt, Model.Element tp) - { - List result = new List(); - 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(); - - 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(); - 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 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 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 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 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 vars; - internal List 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(); - - var names = Util.Empty(); - - 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(); - commons.AddRange(vm.CommonNodes(this)); - } - - public override IEnumerable 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 refs = new List(); - - public SetsNode(StateNode par, Model.Element elt) - : base(par, new EdgeName("\\in ..."), null, null) - { - children = new List(); - 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 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 typeName = new Dictionary(); + Dictionary literalName = new Dictionary(); + Dictionary guessedType = new Dictionary(); + public List states = new List(); + public Dictionary localVariableNames = new Dictionary(); + + Dictionary datatypeLongName = new Dictionary(); + + Dictionary fileNameMapping = new Dictionary(); + + 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(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 simpleName = s => { string dummy; return GetUserVariableNameCore(s, out dummy); }; + var userVars = vars.Where(s => simpleName(s) != null); + var conflictsName = Conflicts(userVars, simpleName).ToArray(); + Func qName = s => { string kind, n = GetUserVariableNameCore(s, out kind); return n + " (" + kind + ")"; }; + var conflictsKind = Conflicts(conflictsName, qName).ToArray(); + + var conflictsNameH = new HashSet(conflictsName); + var conflictsKindH = new HashSet(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 Conflicts(IEnumerable input, Func f) + { + var revMap = new Dictionary(); + var reported = new HashSet(); + + 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 functionScores = new Dictionary(); + + 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 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 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 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 CommonNodes(StateNode state) + { + var skolems = new List(); + + 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 GetExpansion(StateNode state, Model.Element elt, Model.Element tp) + { + List result = new List(); + 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(); + + 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(); + 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 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 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 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 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 vars; + internal List 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(); + + var names = Util.Empty(); + + 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(); + commons.AddRange(vm.CommonNodes(this)); + } + + public override IEnumerable 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 refs = new List(); + + public SetsNode(StateNode par, Model.Element elt) + : base(par, new EdgeName("\\in ..."), null, null) + { + children = new List(); + 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 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(); } + } + } +} -- cgit v1.2.3