From b2313177c3d835093f24cca3851108b39568d479 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 20 Nov 2017 22:18:45 +0000 Subject: [PATCH 01/16] Remove obsolete graphml frontierNode, nodeType See https://github.com/sosy-lab/sv-witnesses for the most up-to-date format specification. --- regression/cbmc/graphml_witness1/test.desc | 6 ----- src/xmllang/graphml.cpp | 27 ---------------------- 2 files changed, 33 deletions(-) diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index cb22eaba5d0..b5f222e2b8b 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -7,12 +7,6 @@ main.c - - path - - - false - false diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 17dc6fd9577..4bb6e3cbd32 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -255,33 +255,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("id", "invariant.scope"); } - // - // path - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "nodeType"); - key.set_attribute("attr.type", "string"); - key.set_attribute("for", "node"); - key.set_attribute("id", "nodetype"); - - key.new_element("default").data="path"; - } - - // - // false - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "isFrontierNode"); - key.set_attribute("attr.type", "boolean"); - key.set_attribute("for", "node"); - key.set_attribute("id", "frontier"); - - key.new_element("default").data="false"; - } - // // false From bdfd587010b86cef68c0dc94b2527c3918d35d07 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 20 Nov 2017 23:22:06 +0000 Subject: [PATCH 02/16] Remove obsolete sourcecode element in graphml https://github.com/sosy-lab/sv-witnesses documents a "control" node, and examples still include "sourcecode" nodes, but there neither is documented semantics for "control" nodes nor is it clear whether the "sourcecode" node is used by any tool. --- regression/cbmc/graphml_witness1/test.desc | 1 - src/goto-programs/graphml_witness.cpp | 37 ---------------------- src/xmllang/graphml.cpp | 9 ------ 3 files changed, 47 deletions(-) diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index b5f222e2b8b..8da9f6661c2 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -28,7 +28,6 @@ main.c - diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 4e919938376..4d106201be8 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -295,34 +295,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) else if(it->type==goto_trace_stept::typet::GOTO && it->pc->is_goto()) { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "sourcecode"); - const std::string cond = - from_expr(ns, it->function_id, it->cond_expr); - const std::string neg_cond = - from_expr(ns, it->function_id, not_exprt(it->cond_expr)); - val.data="["+(it->cond_value ? cond : neg_cond)+"]"; - - #if 0 - xmlt edge2("edge", { - {"source", graphml[from].node_name}, - {"target", graphml[sink].node_name}}, {}); - - xmlt &data_f2=edge2.new_element("data"); - data_f2.set_attribute("key", "originfile"); - data_f2.data=id2string(graphml[from].file); - - xmlt &data_l2=edge2.new_element("data"); - data_l2.set_attribute("key", "startline"); - data_l2.data=id2string(graphml[from].line); - - xmlt &val2=edge2.new_element("data"); - val2.set_attribute("key", "sourcecode"); - val2.data="["+(it->cond_value ? neg_cond : cond)+"]"; - - graphml[sink].in[from].xml_node=edge2; - graphml[from].out[sink].xml_node=edge2; - #endif } graphml[to].in[from].xml_node=edge; @@ -477,15 +449,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) graphml[to].invariant=convert_assign_rec(identifier, assign); graphml[to].invariant_scope = id2string(it->source.function_id); } - else if(it->is_goto() && - it->source.pc->is_goto()) - { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "sourcecode"); - const std::string cond = - from_expr(ns, it->source.function_id, it->cond_expr); - val.data="["+cond+"]"; - } graphml[to].in[from].xml_node=edge; graphml[from].out[to].xml_node=edge; diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 4bb6e3cbd32..257e45bd07b 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -381,15 +381,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("id", "producer"); } - // - { - xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "sourcecode"); - key.set_attribute("attr.type", "string"); - key.set_attribute("for", "edge"); - key.set_attribute("id", "sourcecode"); - } - // { xmlt &key=graphml.new_element("key"); From 978e22938773b57003207196e8da7a7a7f1463db Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 13 Nov 2017 23:09:52 +0000 Subject: [PATCH 03/16] No outgoing edges from violation nodes The witness format documentation only states "Nodes where this flag is set must not have any leaving transitions" for sink nodes, but quite possibly validators expect the same for violation nodes. --- regression/cbmc/graphml_witness1/test.desc | 8 -------- src/goto-programs/graphml_witness.cpp | 3 ++- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index 8da9f6661c2..10531c7e0d9 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -13,9 +13,6 @@ main.c false - - false - false @@ -38,7 +35,6 @@ main.c C - true @@ -61,10 +57,6 @@ main.c true - - main.c - 31 - -- diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 4d106201be8..8d97b18ca44 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -239,7 +239,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) { const std::size_t from=step_to_node[it->step_nr]; - if(from==sink) + // no outgoing edges from sinks or violation nodes + if(from == sink || graphml[from].is_violation) { ++it; continue; From 20a816aeaa5128ac5d2c1b1262899ccfa24283a2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Nov 2017 09:14:21 +0000 Subject: [PATCH 04/16] expr2ct/clean configuration: Do not output C library macros NULL, NAN, INFINITY are not a keywords, just macros. Do not use them for output under the "clean" configuration. --- src/ansi-c/expr2c.cpp | 63 ++++++++++++++++++++++++++++++------------- src/ansi-c/expr2c.h | 9 +++++-- 2 files changed, 51 insertions(+), 21 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index da3e16c4d11..077c43b2b39 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -42,7 +42,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration true, true, "TRUE", - "FALSE" + "FALSE", + true }; expr2c_configurationt expr2c_configurationt::clean_configuration @@ -51,7 +52,8 @@ expr2c_configurationt expr2c_configurationt::clean_configuration false, false, "1", - "0" + "0", + false }; // clang-format on @@ -1857,14 +1859,39 @@ std::string expr2ct::convert_constant( else if(dest.size()==4 && (dest[0]=='+' || dest[0]=='-')) { - if(dest=="+inf") - dest="+INFINITY"; - else if(dest=="-inf") - dest="-INFINITY"; - else if(dest=="+NaN") - dest="+NAN"; - else if(dest=="-NaN") - dest="-NAN"; + if(configuration.use_library_macros) + { + if(dest == "+inf") + dest = "+INFINITY"; + else if(dest == "-inf") + dest = "-INFINITY"; + else if(dest == "+NaN") + dest = "+NAN"; + else if(dest == "-NaN") + dest = "-NAN"; + } + else + { + // ANSI-C: double is default; float/long-double require annotation + std::string suffix = ""; + if(src.type() == float_type()) + suffix = "f"; + else if( + src.type() == long_double_type() && + double_type() != long_double_type()) + { + suffix = "l"; + } + + if(dest == "+inf") + dest = "(1.0" + suffix + "/0.0" + suffix + ")"; + else if(dest == "-inf") + dest = "(-1.0" + suffix + "/0.0" + suffix + ")"; + else if(dest == "+NaN") + dest = "(0.0" + suffix + "/0.0" + suffix + ")"; + else if(dest == "-NaN") + dest = "(-0.0" + suffix + "/0.0" + suffix + ")"; + } } } else if(type.id()==ID_fixedbv) @@ -1885,16 +1912,14 @@ std::string expr2ct::convert_constant( } else if(type.id()==ID_pointer) { - if(value==ID_NULL) - { - dest="NULL"; - if(type.subtype().id()!=ID_empty) - dest="(("+convert(type)+")"+dest+")"; - } - else if(value==std::string(value.size(), '0') && - config.ansi_c.NULL_is_zero) + if( + value == ID_NULL || + (value == std::string(value.size(), '0') && config.ansi_c.NULL_is_zero)) { - dest="NULL"; + if(configuration.use_library_macros) + dest = "NULL"; + else + dest = "0"; if(type.subtype().id()!=ID_empty) dest="(("+convert(type)+")"+dest+")"; } diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h index 03460c01909..e025a7f8b34 100644 --- a/src/ansi-c/expr2c.h +++ b/src/ansi-c/expr2c.h @@ -36,17 +36,22 @@ struct expr2c_configurationt final /// This is the string that will be printed for the false boolean expression std::string false_string; + /// This is the string that will be printed for null pointers + bool use_library_macros; + expr2c_configurationt( const bool include_struct_padding_components, const bool print_struct_body_in_type, const bool include_array_size, const std::string &true_string, - const std::string &false_string) + const std::string &false_string, + const bool use_library_macros) : include_struct_padding_components(include_struct_padding_components), print_struct_body_in_type(print_struct_body_in_type), include_array_size(include_array_size), true_string(true_string), - false_string(false_string) + false_string(false_string), + use_library_macros(use_library_macros) { } From 0ee567578eb69c0612bdf468bc6d499b01b8c169 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 19 Nov 2018 17:43:43 +0000 Subject: [PATCH 05/16] Use clean-C configuration for GraphML witnesses Witness validators expect syntactically correct C code, not human-friendly pseudo-C. --- src/goto-programs/graphml_witness.cpp | 21 +++++++++++++++++---- src/goto-programs/module_dependencies.txt | 1 + 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 8d97b18ca44..eec9c358c3c 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -18,9 +18,21 @@ Author: Daniel Kroening #include #include +#include + +#include #include "goto_program.h" +static std::string +expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr) +{ + if(get_mode_from_identifier(ns, id) == ID_C) + return expr2c(expr, ns, expr2c_configurationt::clean_configuration); + else + return from_expr(ns, id, expr); +} + void graphml_witnesst::remove_l0_l1(exprt &expr) { if(expr.id()==ID_symbol) @@ -129,11 +141,11 @@ std::string graphml_witnesst::convert_assign_rec( exprt clean_rhs=assign.rhs(); remove_l0_l1(clean_rhs); - std::string lhs=from_expr(ns, identifier, assign.lhs()); + std::string lhs = expr_to_string(ns, identifier, assign.lhs()); if(lhs.find('$')!=std::string::npos) lhs="\\result"; - result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";"; + result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";"; } return result; @@ -286,8 +298,9 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) { xmlt &val=edge.new_element("data"); val.set_attribute("key", "assumption"); - val.data = from_expr(ns, it->function_id, it->full_lhs) + " = " + - from_expr(ns, it->function_id, it->full_lhs_value) + ";"; + val.data = expr_to_string(ns, it->function_id, it->full_lhs) + " = " + + expr_to_string(ns, it->function_id, it->full_lhs_value) + + ";"; xmlt &val_s=edge.new_element("data"); val_s.set_attribute("key", "assumption.scope"); diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt index 817a766a240..b63faa217a6 100644 --- a/src/goto-programs/module_dependencies.txt +++ b/src/goto-programs/module_dependencies.txt @@ -1,4 +1,5 @@ analyses # dubious - concerns call_graph and does_remove_const +ansi-c # for GraphML witnesses goto-programs goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness json From fd278051a772758535267cadcfb09294f944addd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 23 Mar 2019 14:27:17 +0000 Subject: [PATCH 06/16] Make sure SSA suffixes are stripped off GraphML output Witness validators expect syntactically correct C code, and cannot cope with SSA suffixes. --- src/goto-programs/graphml_witness.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index eec9c358c3c..c01bd49c036 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -141,7 +141,9 @@ std::string graphml_witnesst::convert_assign_rec( exprt clean_rhs=assign.rhs(); remove_l0_l1(clean_rhs); - std::string lhs = expr_to_string(ns, identifier, assign.lhs()); + exprt clean_lhs = assign.lhs(); + remove_l0_l1(clean_lhs); + std::string lhs = expr_to_string(ns, identifier, clean_lhs); if(lhs.find('$')!=std::string::npos) lhs="\\result"; From 6760695c3a9413e414ddfc60eb72e6493ab4fc4c Mon Sep 17 00:00:00 2001 From: Marek Trtik Date: Mon, 27 Nov 2017 17:59:25 +0000 Subject: [PATCH 07/16] GraphML: Use the \result symbol in place of return value symbols The witness specification permits use of \result in assumptions (in violation witnesses), but then also requires setting assumption.resultfunction. --- src/goto-programs/graphml_witness.cpp | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index c01bd49c036..889001681d1 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -144,8 +144,14 @@ std::string graphml_witnesst::convert_assign_rec( exprt clean_lhs = assign.lhs(); remove_l0_l1(clean_lhs); std::string lhs = expr_to_string(ns, identifier, clean_lhs); - if(lhs.find('$')!=std::string::npos) + + if( + lhs.find("#return_value") != std::string::npos || + (lhs.find('$') != std::string::npos && + has_prefix(lhs, "return_value___VERIFIER_nondet_"))) + { lhs="\\result"; + } result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";"; } @@ -300,13 +306,23 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) { xmlt &val=edge.new_element("data"); val.set_attribute("key", "assumption"); - val.data = expr_to_string(ns, it->function_id, it->full_lhs) + " = " + - expr_to_string(ns, it->function_id, it->full_lhs_value) + - ";"; + + code_assignt assign{it->full_lhs, it->full_lhs_value}; + irep_idt identifier = irep_idt(); + if(const auto object = it->get_lhs_object()) + identifier = object->get_identifier(); + val.data = convert_assign_rec(identifier, assign); xmlt &val_s=edge.new_element("data"); val_s.set_attribute("key", "assumption.scope"); val_s.data = id2string(it->function_id); + + if(has_prefix(val.data, "\\result =")) + { + xmlt &val_f = edge.new_element("data"); + val_f.set_attribute("key", "assumption.resultfunction"); + val_f.data = id2string(it->function_id); + } } else if(it->type==goto_trace_stept::typet::GOTO && it->pc->is_goto()) From 611cba20e788b346ef8b4ef4db661934723fffab Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 27 Nov 2017 18:44:45 +0000 Subject: [PATCH 08/16] Add violation node for the memory safety benchmarks We must not filter out generated assertions for memory leaks. --- src/goto-programs/graphml_witness.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 889001681d1..4f243f33f5d 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -11,9 +11,10 @@ Author: Daniel Kroening #include "graphml_witness.h" +#include #include #include -#include +#include #include #include @@ -189,7 +190,14 @@ static bool filter_out( source_location.get_file().empty() || source_location.is_built_in() || source_location.get_line().empty()) - return true; + { + const irep_idt id = source_location.get_function(); + // Do not filter out assertions in functions the name of which starts with + // CPROVER_PREFIX, because we need to maintain those as violation nodes: + // these are assertions generated, for examples, for memory leaks. + if(!has_prefix(id2string(id), CPROVER_PREFIX) || !it->is_assert()) + return true; + } return false; } From d0da778309b2ba4c4e74807b905bf3e65b82316d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 26 Nov 2017 22:55:04 +0000 Subject: [PATCH 09/16] GraphML output: Split array-list into assignments Witness validators cannot handle array lists. --- src/goto-programs/graphml_witness.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 4f243f33f5d..9431b8ef7ea 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -66,7 +66,21 @@ std::string graphml_witnesst::convert_assign_rec( { std::string result; - if(assign.rhs().id()==ID_array) + if(assign.rhs().id() == ID_array_list) + { + const array_list_exprt &array_list = to_array_list_expr(assign.rhs()); + const auto &ops = array_list.operands(); + + for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2) + { + const index_exprt index{assign.lhs(), ops[listidx]}; + if(!result.empty()) + result += ' '; + result += + convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]}); + } + } + else if(assign.rhs().id() == ID_array) { const array_typet &type = to_array_type(assign.rhs().type()); From 0aff1c5664fd5abc3908c8485ca43f07061218da Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 26 Nov 2017 22:55:04 +0000 Subject: [PATCH 10/16] GraphML output: hide assignments to dynamic objects These symbols do not occur in the input program. --- src/goto-programs/graphml_witness.cpp | 68 +++++++++++++++++++-------- 1 file changed, 48 insertions(+), 20 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 9431b8ef7ea..3aba0679331 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening #include #include #include +#include #include #include @@ -216,6 +217,23 @@ static bool filter_out( return false; } +static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) +{ + if( + expr.id() == ID_symbol && + has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix)) + { + return true; + } + + forall_operands(it, expr) + { + if(contains_symbol_prefix(*it, prefix)) + return true; + } + return false; +} + /// counterexample witness void graphml_witnesst::operator()(const goto_tracet &goto_trace) { @@ -322,28 +340,38 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) data_l.data=id2string(graphml[from].line); } - if(it->type==goto_trace_stept::typet::ASSIGNMENT && - it->full_lhs_value.is_not_nil() && - it->full_lhs.is_not_nil()) + const auto lhs_object = it->get_lhs_object(); + if( + it->type == goto_trace_stept::typet::ASSIGNMENT && + lhs_object.has_value()) { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "assumption"); - - code_assignt assign{it->full_lhs, it->full_lhs_value}; - irep_idt identifier = irep_idt(); - if(const auto object = it->get_lhs_object()) - identifier = object->get_identifier(); - val.data = convert_assign_rec(identifier, assign); - - xmlt &val_s=edge.new_element("data"); - val_s.set_attribute("key", "assumption.scope"); - val_s.data = id2string(it->function_id); - - if(has_prefix(val.data, "\\result =")) + const std::string &lhs_id = id2string(lhs_object->get_identifier()); + if( + !contains_symbol_prefix( + it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") && + !contains_symbol_prefix( + it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") && + (!it->full_lhs_value.is_constant() || + !it->full_lhs_value.has_operands() || + !has_prefix( + id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-"))) { - xmlt &val_f = edge.new_element("data"); - val_f.set_attribute("key", "assumption.resultfunction"); - val_f.data = id2string(it->function_id); + xmlt &val = edge.new_element("data"); + val.set_attribute("key", "assumption"); + + code_assignt assign{it->full_lhs, it->full_lhs_value}; + val.data = convert_assign_rec(lhs_id, assign); + + xmlt &val_s = edge.new_element("data"); + val_s.set_attribute("key", "assumption.scope"); + val_s.data = id2string(it->function_id); + + if(has_prefix(val.data, "\\result =")) + { + xmlt &val_f = edge.new_element("data"); + val_f.set_attribute("key", "assumption.resultfunction"); + val_f.data = id2string(it->function_id); + } } } else if(it->type==goto_trace_stept::typet::GOTO && From 6d1236dc711d6127a994bda2a9be073fa0ae0d21 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 23 Mar 2019 12:53:49 +0000 Subject: [PATCH 11/16] GraphML witnesses: unwind "with" expressions Witness validators cannot be expected to understand CBMC's "with" expressions. Fixes: #4486 --- src/goto-programs/graphml_witness.cpp | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 3aba0679331..3272d238d37 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -152,6 +152,31 @@ std::string graphml_witnesst::convert_assign_rec( break; } } + else if(assign.rhs().id() == ID_with) + { + const with_exprt &with_expr = to_with_expr(assign.rhs()); + const auto &ops = with_expr.operands(); + + for(std::size_t i = 1; i < ops.size(); i += 2) + { + if(!result.empty()) + result += ' '; + + if(ops[i].id() == ID_member_name) + { + const member_exprt member{ + assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()}; + result += + convert_assign_rec(identifier, code_assignt(member, ops[i + 1])); + } + else + { + const index_exprt index{assign.lhs(), ops[i]}; + result += + convert_assign_rec(identifier, code_assignt(index, ops[i + 1])); + } + } + } else { exprt clean_rhs=assign.rhs(); @@ -527,7 +552,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) irep_idt identifier=it->ssa_lhs.get_object_name(); graphml[to].has_invariant=true; - code_assignt assign(it->ssa_full_lhs, it->ssa_rhs); + code_assignt assign(it->ssa_lhs, it->ssa_rhs); graphml[to].invariant=convert_assign_rec(identifier, assign); graphml[to].invariant_scope = id2string(it->source.function_id); } From 9e303e2874fd200779a103881517fe4afa6e7ac4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 20 Nov 2017 22:18:45 +0000 Subject: [PATCH 12/16] GraphML: add cyclehead node It's actually not clear whether this is necessary or permitted, it's not contained in the official specification. --- src/xmllang/graphml.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 257e45bd07b..28664feb3e4 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -309,6 +309,20 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.new_element("default").data="false"; } + // + // false + // + { + xmlt &key = graphml.new_element("key"); + key.set_attribute("attr.name", "cyclehead"); + key.set_attribute("attr.type", "boolean"); + key.set_attribute("for", "edge"); + key.set_attribute("id", "cyclehead"); + + key.new_element("default").data = "false"; + } + // // TODO: format for multi-threaded programs not defined yet { From 3156ad7fb3843c5825bfd873de90eba252cb9049 Mon Sep 17 00:00:00 2001 From: Marek Trtik Date: Fri, 17 Nov 2017 11:56:05 +0000 Subject: [PATCH 13/16] Using cache to speed up generation of GraphML file Expression-to-string conversion is costly. --- src/goto-programs/graphml_witness.cpp | 16 ++++++++++++++++ src/goto-programs/graphml_witness.h | 24 ++++++++++++++++++++++++ 2 files changed, 40 insertions(+) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 3272d238d37..ffab36c4f68 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening #include #include #include +#include #include #include @@ -65,6 +66,15 @@ std::string graphml_witnesst::convert_assign_rec( const irep_idt &identifier, const code_assignt &assign) { +#ifdef USE_DSTRING + const auto cit = cache.find({identifier.get_no(), &assign.read()}); +#else + const auto cit = + cache.find({get_string_container()[id2string(identifier)], &assign.read()}); +#endif + if(cit != cache.end()) + return cit->second; + std::string result; if(assign.rhs().id() == ID_array_list) @@ -197,6 +207,12 @@ std::string graphml_witnesst::convert_assign_rec( result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";"; } +#ifdef USE_DSTRING + cache.insert({{identifier.get_no(), &assign.read()}, result}); +#else + cache.insert( + {{get_string_container()[id2string(identifier)], &assign.read()}, result}); +#endif return result; } diff --git a/src/goto-programs/graphml_witness.h b/src/goto-programs/graphml_witness.h index 053eb801146..804dbf84a1a 100644 --- a/src/goto-programs/graphml_witness.h +++ b/src/goto-programs/graphml_witness.h @@ -42,6 +42,30 @@ class graphml_witnesst std::string convert_assign_rec( const irep_idt &identifier, const code_assignt &assign); + + template + static void hash_combine(std::size_t &seed, const T &v) + { + std::hash hasher; + seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + } + + template + struct pair_hash // NOLINT(readability/identifiers) + { + std::size_t operator()(const std::pair &v) const + { + std::size_t seed = 0; + hash_combine(seed, v.first); + hash_combine(seed, v.second); + return seed; + } + }; + std::unordered_map< + std::pair, + std::string, + pair_hash> + cache; }; #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H From 7247f3d3a8493aca6575dd21e3d89496125d1863 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 23 Mar 2019 16:10:24 +0000 Subject: [PATCH 14/16] Hack to make CPAchecker parse graphml concurrency witnesses This does likely need more work, but at least got us some points in the past. --- regression/cbmc/graphml_witness1/test.desc | 3 - src/goto-programs/graphml_witness.cpp | 72 +++++++++++++++++++--- src/xmllang/graphml.cpp | 29 ++++----- src/xmllang/graphml.h | 1 - 4 files changed, 80 insertions(+), 25 deletions(-) diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index 10531c7e0d9..5203bd00210 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -16,9 +16,6 @@ main.c false - - 0 - diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index ffab36c4f68..03e04be2f15 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -278,14 +278,61 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) /// counterexample witness void graphml_witnesst::operator()(const goto_tracet &goto_trace) { + unsigned int max_thread_idx = 0; + bool trace_has_violation = false; + for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin(); + it != goto_trace.steps.end(); + ++it) + { + if(it->thread_nr > max_thread_idx) + max_thread_idx = it->thread_nr; + if(it->is_assert() && !it->cond_value) + trace_has_violation = true; + } + graphml.key_values["sourcecodelang"]="C"; const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; - graphml[sink].thread_nr=0; graphml[sink].is_violation=false; graphml[sink].has_invariant=false; + if(max_thread_idx > 0 && trace_has_violation) + { + std::vector nodes; + + for(unsigned int i = 0; i <= max_thread_idx + 1; ++i) + { + nodes.push_back(graphml.add_node()); + graphml[nodes.back()].node_name = "N" + std::to_string(i); + graphml[nodes.back()].is_violation = i == max_thread_idx + 1; + graphml[nodes.back()].has_invariant = false; + } + + for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it) + { + xmlt edge("edge"); + edge.set_attribute("source", graphml[*it].node_name); + edge.set_attribute("target", graphml[*std::next(it)].node_name); + const auto thread_id = std::distance(nodes.cbegin(), it); + xmlt &data = edge.new_element("data"); + data.set_attribute("key", "createThread"); + data.data = std::to_string(thread_id); + if(thread_id == 0) + { + xmlt &data = edge.new_element("data"); + data.set_attribute("key", "enterFunction"); + data.data = "main"; + } + graphml[*std::next(it)].in[*it].xml_node = edge; + graphml[*it].out[*std::next(it)].xml_node = edge; + } + + // we do not provide any further details as CPAchecker does not seem to + // handle more detailed concurrency witnesses + return; + } + // step numbers start at 1 std::vector step_to_node(goto_trace.steps.size()+1, 0); @@ -324,7 +371,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr); graphml[node].file=source_location.get_file(); graphml[node].line=source_location.get_line(); - graphml[node].thread_nr=it->thread_nr; graphml[node].is_violation= it->type==goto_trace_stept::typet::ASSERT && !it->cond_value; graphml[node].has_invariant=false; @@ -332,6 +378,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) step_to_node[it->step_nr]=node; } + unsigned thread_id = 0; + // build edges for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin(); @@ -364,6 +412,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::ASSIGNMENT: case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: + case goto_trace_stept::typet::SPAWN: { xmlt edge( "edge", @@ -379,6 +428,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) xmlt &data_l=edge.new_element("data"); data_l.set_attribute("key", "startline"); data_l.data=id2string(graphml[from].line); + + xmlt &data_t=edge.new_element("data"); + data_t.set_attribute("key", "threadId"); + data_t.data=std::to_string(it->thread_nr); } const auto lhs_object = it->get_lhs_object(); @@ -387,11 +440,19 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) lhs_object.has_value()) { const std::string &lhs_id = id2string(lhs_object->get_identifier()); - if( + if(lhs_id.find("pthread_create::thread") != std::string::npos) + { + xmlt &data_t = edge.new_element("data"); + data_t.set_attribute("key", "createThread"); + data_t.data = std::to_string(++thread_id); + } + else if( !contains_symbol_prefix( it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") && !contains_symbol_prefix( it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") && + lhs_id.find("thread") == std::string::npos && + lhs_id.find("mutex") == std::string::npos && (!it->full_lhs_value.is_constant() || !it->full_lhs_value.has_operands() || !has_prefix( @@ -434,7 +495,6 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::OUTPUT: case goto_trace_stept::typet::SHARED_READ: case goto_trace_stept::typet::SHARED_WRITE: - case goto_trace_stept::typet::SPAWN: case goto_trace_stept::typet::MEMORY_BARRIER: case goto_trace_stept::typet::ATOMIC_BEGIN: case goto_trace_stept::typet::ATOMIC_END: @@ -456,7 +516,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; - graphml[sink].thread_nr=0; graphml[sink].is_violation=false; graphml[sink].has_invariant=false; @@ -502,7 +561,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) std::to_string(step_nr); graphml[node].file=source_location.get_file(); graphml[node].line=source_location.get_line(); - graphml[node].thread_nr=it->source.thread_nr; graphml[node].is_violation=false; graphml[node].has_invariant=false; @@ -543,6 +601,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::ASSIGNMENT: case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: + case goto_trace_stept::typet::SPAWN: { xmlt edge( "edge", @@ -587,7 +646,6 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::OUTPUT: case goto_trace_stept::typet::SHARED_READ: case goto_trace_stept::typet::SHARED_WRITE: - case goto_trace_stept::typet::SPAWN: case goto_trace_stept::typet::MEMORY_BARRIER: case goto_trace_stept::typet::ATOMIC_BEGIN: case goto_trace_stept::typet::ATOMIC_END: diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 28664feb3e4..286912aa089 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -54,7 +54,6 @@ static bool build_graph_rec( node.node_name=node_name; node.is_violation=false; node.has_invariant=false; - node.thread_nr=0; for(xmlt::elementst::const_iterator e_it=xml.elements.begin(); @@ -66,8 +65,6 @@ static bool build_graph_rec( if(e_it->get_attribute("key")=="violation" && e_it->data=="true") node.is_violation=e_it->data=="true"; - else if(e_it->get_attribute("key")=="threadNumber") - node.thread_nr=safe_string2unsigned(e_it->data); else if(e_it->get_attribute("key")=="entry" && e_it->data=="true") entrynode=node_name; @@ -324,13 +321,24 @@ bool write_graphml(const graphmlt &src, std::ostream &os) } // - // TODO: format for multi-threaded programs not defined yet { xmlt &key=graphml.new_element("key"); - key.set_attribute("attr.name", "threadNumber"); + key.set_attribute("attr.name", "threadId"); key.set_attribute("attr.type", "int"); - key.set_attribute("for", "node"); - key.set_attribute("id", "thread"); + key.set_attribute("for", "edge"); + key.set_attribute("id", "threadId"); + + key.new_element("default").data = "0"; + } + + // + { + xmlt &key = graphml.new_element("key"); + key.set_attribute("attr.name", "createThread"); + key.set_attribute("attr.type", "int"); + key.set_attribute("for", "edge"); + key.set_attribute("id", "createThread"); key.new_element("default").data="0"; } @@ -503,13 +511,6 @@ bool write_graphml(const graphmlt &src, std::ostream &os) entry_done=true; } - if(n.thread_nr!=0) - { - xmlt &entry=node.new_element("data"); - entry.set_attribute("key", "threadNumber"); - entry.data=std::to_string(n.thread_nr); - } - // // true // diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index f86dac5648e..cbdcd122828 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -32,7 +32,6 @@ struct xml_graph_nodet:public graph_nodet std::string node_name; irep_idt file; irep_idt line; - unsigned thread_nr; bool is_violation; bool has_invariant; std::string invariant; From a703b763a9914d831c17586c67a75554a2226201 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 23 Mar 2019 17:11:47 +0000 Subject: [PATCH 15/16] GraphML witnesses: clang-format switch/case statement --- src/goto-programs/graphml_witness.cpp | 176 +++++++++++++------------- 1 file changed, 88 insertions(+), 88 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 03e04be2f15..4f657d6c7c7 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -413,78 +413,78 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: case goto_trace_stept::typet::SPAWN: + { + xmlt edge( + "edge", + {{"source", graphml[from].node_name}, + {"target", graphml[to].node_name}}, + {}); + { - xmlt edge( - "edge", - {{"source", graphml[from].node_name}, - {"target", graphml[to].node_name}}, - {}); + xmlt &data_f = edge.new_element("data"); + data_f.set_attribute("key", "originfile"); + data_f.data = id2string(graphml[from].file); - { - xmlt &data_f=edge.new_element("data"); - data_f.set_attribute("key", "originfile"); - data_f.data=id2string(graphml[from].file); + xmlt &data_l = edge.new_element("data"); + data_l.set_attribute("key", "startline"); + data_l.data = id2string(graphml[from].line); - xmlt &data_l=edge.new_element("data"); - data_l.set_attribute("key", "startline"); - data_l.data=id2string(graphml[from].line); + xmlt &data_t = edge.new_element("data"); + data_t.set_attribute("key", "threadId"); + data_t.data = std::to_string(it->thread_nr); + } - xmlt &data_t=edge.new_element("data"); - data_t.set_attribute("key", "threadId"); - data_t.data=std::to_string(it->thread_nr); + const auto lhs_object = it->get_lhs_object(); + if( + it->type == goto_trace_stept::typet::ASSIGNMENT && + lhs_object.has_value()) + { + const std::string &lhs_id = id2string(lhs_object->get_identifier()); + if(lhs_id.find("pthread_create::thread") != std::string::npos) + { + xmlt &data_t = edge.new_element("data"); + data_t.set_attribute("key", "createThread"); + data_t.data = std::to_string(++thread_id); } - - const auto lhs_object = it->get_lhs_object(); - if( - it->type == goto_trace_stept::typet::ASSIGNMENT && - lhs_object.has_value()) + else if( + !contains_symbol_prefix( + it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") && + !contains_symbol_prefix( + it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") && + lhs_id.find("thread") == std::string::npos && + lhs_id.find("mutex") == std::string::npos && + (!it->full_lhs_value.is_constant() || + !it->full_lhs_value.has_operands() || + !has_prefix( + id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-"))) { - const std::string &lhs_id = id2string(lhs_object->get_identifier()); - if(lhs_id.find("pthread_create::thread") != std::string::npos) - { - xmlt &data_t = edge.new_element("data"); - data_t.set_attribute("key", "createThread"); - data_t.data = std::to_string(++thread_id); - } - else if( - !contains_symbol_prefix( - it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") && - !contains_symbol_prefix( - it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") && - lhs_id.find("thread") == std::string::npos && - lhs_id.find("mutex") == std::string::npos && - (!it->full_lhs_value.is_constant() || - !it->full_lhs_value.has_operands() || - !has_prefix( - id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-"))) + xmlt &val = edge.new_element("data"); + val.set_attribute("key", "assumption"); + + code_assignt assign{it->full_lhs, it->full_lhs_value}; + val.data = convert_assign_rec(lhs_id, assign); + + xmlt &val_s = edge.new_element("data"); + val_s.set_attribute("key", "assumption.scope"); + val_s.data = id2string(it->function_id); + + if(has_prefix(val.data, "\\result =")) { - xmlt &val = edge.new_element("data"); - val.set_attribute("key", "assumption"); - - code_assignt assign{it->full_lhs, it->full_lhs_value}; - val.data = convert_assign_rec(lhs_id, assign); - - xmlt &val_s = edge.new_element("data"); - val_s.set_attribute("key", "assumption.scope"); - val_s.data = id2string(it->function_id); - - if(has_prefix(val.data, "\\result =")) - { - xmlt &val_f = edge.new_element("data"); - val_f.set_attribute("key", "assumption.resultfunction"); - val_f.data = id2string(it->function_id); - } + xmlt &val_f = edge.new_element("data"); + val_f.set_attribute("key", "assumption.resultfunction"); + val_f.data = id2string(it->function_id); } } - else if(it->type==goto_trace_stept::typet::GOTO && - it->pc->is_goto()) - { - } - - graphml[to].in[from].xml_node=edge; - graphml[from].out[to].xml_node=edge; } + else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto()) + { + } + + graphml[to].in[from].xml_node = edge; + graphml[from].out[to].xml_node = edge; + break; + } case goto_trace_stept::typet::DECL: case goto_trace_stept::typet::FUNCTION_CALL: @@ -602,40 +602,40 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: case goto_trace_stept::typet::SPAWN: + { + xmlt edge( + "edge", + {{"source", graphml[from].node_name}, + {"target", graphml[to].node_name}}, + {}); + { - xmlt edge( - "edge", - {{"source", graphml[from].node_name}, - {"target", graphml[to].node_name}}, - {}); + xmlt &data_f = edge.new_element("data"); + data_f.set_attribute("key", "originfile"); + data_f.data = id2string(graphml[from].file); - { - xmlt &data_f=edge.new_element("data"); - data_f.set_attribute("key", "originfile"); - data_f.data=id2string(graphml[from].file); + xmlt &data_l = edge.new_element("data"); + data_l.set_attribute("key", "startline"); + data_l.data = id2string(graphml[from].line); + } - xmlt &data_l=edge.new_element("data"); - data_l.set_attribute("key", "startline"); - data_l.data=id2string(graphml[from].line); - } + if( + (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() && + it->ssa_full_lhs.is_not_nil()) + { + irep_idt identifier = it->ssa_lhs.get_object_name(); - if((it->is_assignment() || - it->is_decl()) && - it->ssa_rhs.is_not_nil() && - it->ssa_full_lhs.is_not_nil()) - { - irep_idt identifier=it->ssa_lhs.get_object_name(); + graphml[to].has_invariant = true; + code_assignt assign(it->ssa_lhs, it->ssa_rhs); + graphml[to].invariant = convert_assign_rec(identifier, assign); + graphml[to].invariant_scope = id2string(it->source.function_id); + } - graphml[to].has_invariant=true; - code_assignt assign(it->ssa_lhs, it->ssa_rhs); - graphml[to].invariant=convert_assign_rec(identifier, assign); - graphml[to].invariant_scope = id2string(it->source.function_id); - } + graphml[to].in[from].xml_node = edge; + graphml[from].out[to].xml_node = edge; - graphml[to].in[from].xml_node=edge; - graphml[from].out[to].xml_node=edge; - } break; + } case goto_trace_stept::typet::DECL: case goto_trace_stept::typet::FUNCTION_CALL: From 16a59aadf96f1eb65c96afd87c50c37aa4d112e2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 23 Mar 2019 17:20:23 +0000 Subject: [PATCH 16/16] GraphML witnesses: correctly set the scope of parameters We would previously use the name of the calling function. Instead, parameter assignments require a special case. Regression test kindly provided by @JanSvejda. Fixes: #4418 --- regression/cbmc/graphml_witness1/test.desc | 2 +- regression/cbmc/graphml_witness2/main.c | 31 ++++++++++++++++++++++ regression/cbmc/graphml_witness2/test.desc | 10 +++++++ src/goto-programs/graphml_witness.cpp | 8 +++++- 4 files changed, 49 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc/graphml_witness2/main.c create mode 100644 regression/cbmc/graphml_witness2/test.desc diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc index 5203bd00210..d0428e2738d 100644 --- a/regression/cbmc/graphml_witness1/test.desc +++ b/regression/cbmc/graphml_witness1/test.desc @@ -43,7 +43,7 @@ main.c main.c 29 - main + remove_one diff --git a/regression/cbmc/graphml_witness2/main.c b/regression/cbmc/graphml_witness2/main.c new file mode 100644 index 00000000000..ebe307a73c0 --- /dev/null +++ b/regression/cbmc/graphml_witness2/main.c @@ -0,0 +1,31 @@ +extern void __VERIFIER_error(); + +static float one(float *foo) +{ + return *foo; +} + +static float two(float *foo) +{ + return *foo; +} + +float x = 0; + +void step() +{ + x = one(0); +} + +int main(void) +{ + while(1) + { + step(); + if(x == 0) + { + __VERIFIER_error(); + } + } + return 0; +} diff --git a/regression/cbmc/graphml_witness2/test.desc b/regression/cbmc/graphml_witness2/test.desc new file mode 100644 index 00000000000..6a97a4749fb --- /dev/null +++ b/regression/cbmc/graphml_witness2/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--graphml-witness - --unwindset main.0:1 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +foo = \(\(float \*\)0\); +one +-- +^warning: ignoring diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 4f657d6c7c7..c81bbc9ef6d 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -466,7 +466,13 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) xmlt &val_s = edge.new_element("data"); val_s.set_attribute("key", "assumption.scope"); - val_s.data = id2string(it->function_id); + irep_idt function_id = it->function_id; + const symbolt *symbol_ptr = nullptr; + if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter) + { + function_id = lhs_id.substr(0, lhs_id.find("::")); + } + val_s.data = id2string(function_id); if(has_prefix(val.data, "\\result =")) {