From 321ceeee73433b2a772cd3435cb2ffaa346fb113 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Mon, 24 Oct 2011 18:00:28 -0700 Subject: VCC: improvements in showing arrays, addresses, and embeddings --- Source/ModelViewer/Namer.cs | 1 + Source/ModelViewer/VccProvider.cs | 71 +++++++++++++++++++++++++++------------ 2 files changed, 51 insertions(+), 21 deletions(-) (limited to 'Source/ModelViewer') diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index fce9522d..49ff93ea 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -106,6 +106,7 @@ namespace Microsoft.Boogie.ModelViewer public virtual string CanonicalName(Model.Element elt) { string res; + if (elt == null) return "?"; if (canonicalName.TryGetValue(elt, out res)) return res; NameSeqSuffix suff; var baseName = CanonicalBaseName(elt, out suff); diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index cbaecbd8..b5ba6c22 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -39,7 +39,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc f_owners, f_closed, f_roots, f_timestamps, f_select_bool, f_select_int, f_is_null, f_good_state, f_int_to_version, f_int_to_ptrset, f_set_in0, f_is_ghost_field, f_is_phys_field, f_idx, f_field_plus, f_is_sequential_field, f_is_volatile_field, f_type_project_0, f_array, f_active_option, f_int_to_field, - f_blob_type, f_array_emb, f_addr, f_address_root; + f_blob_type, f_array_emb, f_addr, f_address_root, f_base, f_field_arr_size, f_field_arr_root, f_field_arr_index; 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(); @@ -95,7 +95,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc 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_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(); @@ -233,7 +237,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc static string[][] totals = new string[][] { new string[] { - "$addr", "$current_timestamp", + "$current_timestamp", "$full_stop", "$function_entry", "$ptr_to_i4", "$ptr_to_i8", "$ptr_to_u4", "$ptr_to_u8", "$span", "$sizeof", "$in_domain", @@ -246,7 +250,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc }, new string[] { - "$dot", "$emb0", "$fetch_from_domain", "$in_range_phys_ptr", + "$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", @@ -793,6 +797,16 @@ namespace Microsoft.Boogie.ModelViewer.Vcc } } + 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); @@ -924,32 +938,45 @@ namespace Microsoft.Boogie.ModelViewer.Vcc } if (elt != null) { - foreach (var app in f_idx.AppsWithArg(0, elt)) { - var addr = app.Result; - Model.Element val = null, atp = tp; - - addresses.Add(app.Result); - - foreach (var papp in f_ptr.AppsWithResult(addr)) { - var tmp = f_select_value.OptEval(f_select_field.OptEval(heap, papp.Args[0]), papp.Args[1]); - if (tmp != null) { - val = tmp; - var tt = f_field_type.TryEval(papp.Args[0]); - if (tt != null) atp = tt; + var eltBase = f_base.TryEval(elt); + var eltField = f_field.TryEval(elt); + if (eltBase != null && eltField != null) { + foreach (var app in f_field_plus.AppsWithArg(0, eltField)) { + var fieldName = app.Result; + var addr = f_ptr.TryEval(fieldName, eltBase); + if (addr == null) continue; + + Model.Element val = null, atp = tp; + + addresses.Add(addr); + + foreach (var papp in f_ptr.AppsWithResult(addr)) { + var tmp = f_select_value.OptEval(f_select_field.OptEval(heap, papp.Args[0]), papp.Args[1]); + if (tmp != null) { + val = tmp; + var tt = f_field_type.TryEval(papp.Args[0]); + 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 }); + 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 }); + } } } if (elt != null) { foreach (var ptr in f_ptr.AppsWithArg(1, elt)) { if (addresses.Contains(ptr.Result)) continue; + var fld = ptr.Args[0]; + var idx = f_field_arr_index.TryEval(fld); + if (idx != null) { + var xtp = f_field_type.TryEval(fld); + result.Add(new MapletNode(state, new EdgeName(this, "&[%0] of %1", idx, f_field_arr_size.TryEval(fld)), ptr.Result, GuessPtrTo(xtp)) { Category = NodeCategory.Maplet }); + } if (!IsConstantField(ptr.Args[0])) continue; BuildFieldNode(result, state, ptr.Result, ptr.Args[0], null, ptr.Result); } @@ -959,6 +986,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc AddSpecialField(state, elt, result, "\\owner", f_owners); AddSpecialField(state, elt, result, "\\root", f_roots); AddSpecialField(state, elt, result, "\\timestamp", f_timestamps); + AddPointerFunction(state, elt, result, "\\embedding", f_base, tp_object); + AddPointerFunction(state, elt, result, "\\addr", f_addr, tp_mathint); if (viewOpts.ViewLevel >= 1 && elt != null) { AddPtrType(state, elt, result); -- cgit v1.2.3