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 string ShortName { set { this.name = new EdgeName(value); } get { return this.name.ToString(); } } } }