From 454265360d92a388be62e98f3b605bec1e7c16be Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2016 13:53:18 +0000 Subject: [PATCH 1/9] stub for correctness witness generation --- src/cbmc/bmc.cpp | 4 ++++ src/goto-programs/graphml_witness.cpp | 16 ++++++++++++++++ src/goto-programs/graphml_witness.h | 3 +++ 3 files changed, 23 insertions(+) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ba970e659c8..5413dc74c40 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -131,6 +131,8 @@ void bmct::output_graphml( graphml_witnesst graphml_witness(ns); if(result==UNSAFE) graphml_witness(safety_checkert::error_trace); + else if(result==SAFE) + graphml_witness(equation); else return; @@ -544,6 +546,7 @@ safety_checkert::resultt bmct::run( symex.remaining_vccs==0) { report_success(); + output_graphml(SAFE, goto_functions); return safety_checkert::SAFE; } @@ -619,6 +622,7 @@ safety_checkert::resultt bmct::stop_on_fail( { case decision_proceduret::D_UNSATISFIABLE: report_success(); + output_graphml(SAFE, goto_functions); return SAFE; case decision_proceduret::D_SATISFIABLE: diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index f5236227de6..d80443c8060 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -316,3 +316,19 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) it=next; } } + +/*******************************************************************\ + +Function: graphml_witnesst::operator() + + Inputs: + + Outputs: + + Purpose: proof witness + +\*******************************************************************/ + +void graphml_witnesst::operator()(const symex_target_equationt &equation) +{ +} diff --git a/src/goto-programs/graphml_witness.h b/src/goto-programs/graphml_witness.h index c68e8b8d4cb..8ec1400938f 100644 --- a/src/goto-programs/graphml_witness.h +++ b/src/goto-programs/graphml_witness.h @@ -11,6 +11,8 @@ Author: Daniel Kroening #include +#include + #include "goto_trace.h" class graphml_witnesst @@ -22,6 +24,7 @@ class graphml_witnesst } void operator()(const goto_tracet &goto_trace); + void operator()(const symex_target_equationt &equation); inline const graphmlt &graph() { From ab25eea6a9d6f5cae051b71dba37b817fa5af7b5 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2016 14:28:49 +0000 Subject: [PATCH 2/9] Add_node_if_not_exists for graphml --- src/xmllang/graphml.h | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index 42170e6562f..c32d2b0ede1 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -34,7 +34,29 @@ struct xml_graph_nodet:public graph_nodet bool is_violation; }; -typedef graph graphmlt; +class graphmlt : public graph +{ +public: + inline bool has_node(const std::string &node_name) const + { + for(const auto & n : nodes) + if(n.node_name==node_name) + return true; + + return false; + } + + const node_indext add_node_if_not_exists(std::string node_name) + { + for(node_indext i=0; i::add_node(); + } +}; bool read_graphml( std::istream &is, From db1e12d75760b5674e2fde8fa5162ffa1e02a7f3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2016 15:10:45 +0000 Subject: [PATCH 3/9] Generate nodes for graphml correctness witness --- src/goto-programs/graphml_witness.cpp | 175 +++++++++++++++++++++++++- 1 file changed, 172 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index d80443c8060..0ed98ff9fa7 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -6,6 +6,8 @@ Author: Daniel Kroening \*******************************************************************/ +#include + #include #include #include @@ -143,6 +145,14 @@ Function: graphml_witnesst::operator() void graphml_witnesst::operator()(const goto_tracet &goto_trace) { + graphml.key_values["witness-type"]="violation_witness"; + graphml.key_values["sourcecodelang"]="C"; + graphml.key_values["producer"]=""; + graphml.key_values["programfile"]=""; + graphml.key_values["programhash"]=""; + graphml.key_values["specification"]=""; + graphml.key_values["architecture"]=""; + const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; graphml[sink].thread_nr=0; @@ -154,7 +164,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin(); it!=goto_trace.steps.end(); - it++) + it++) //we cannot replace this by a ranged for { const source_locationt &source_location=it->pc->source_location; @@ -202,7 +212,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) it!=goto_trace.steps.end(); ) // no ++it { - const unsigned from=step_to_node[it->step_nr]; + const std::size_t from=step_to_node[it->step_nr]; if(from==sink) { @@ -217,7 +227,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) it->pc==next->pc); ++next) ; - const unsigned to= + const std::size_t to= next==goto_trace.steps.end()? sink:step_to_node[next->step_nr]; @@ -331,4 +341,163 @@ Function: graphml_witnesst::operator() void graphml_witnesst::operator()(const symex_target_equationt &equation) { + graphml.key_values["witness-type"]="correctness_witness"; + graphml.key_values["sourcecodelang"]="C"; + graphml.key_values["producer"]=""; + graphml.key_values["programfile"]=""; + graphml.key_values["programhash"]=""; + graphml.key_values["specification"]=""; + graphml.key_values["architecture"]=""; + + const graphmlt::node_indext sink=graphml.add_node(); + graphml[sink].node_name="sink"; + graphml[sink].thread_nr=0; + graphml[sink].is_violation=false; + + // step numbers start at 1 + std::vector step_to_node(equation.SSA_steps.size()+1, 0); + + std::size_t step_nr=1; + for(symex_target_equationt::SSA_stepst::const_iterator + it=equation.SSA_steps.begin(); + it!=equation.SSA_steps.end(); + it++, step_nr++) //we cannot replace this by a ranged for + { + const source_locationt &source_location=it->source.pc->source_location; + + if(it->hidden || + (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || + (it->is_goto() && it->source.pc->guard.is_true()) || + source_location.is_nil() || + source_location.get_file()=="" || + source_location.get_line().empty()) + { + step_to_node[step_nr]=sink; + + continue; + } + + // skip declarations followed by an immediate assignment + symex_target_equationt::SSA_stepst::const_iterator next=it; + ++next; + if(next!=equation.SSA_steps.end() && + next->is_assignment() && + it->ssa_full_lhs==next->ssa_full_lhs && + it->source.pc->source_location==next->source.pc->source_location) + { + step_to_node[step_nr]=sink; + + continue; + } + + const graphmlt::node_indext node=graphml.add_node(); + graphml[node].node_name= + i2string(it->source.pc->location_number)+"."+i2string(step_nr); + graphml[node].file=source_location.get_file(); + graphml[node].line=source_location.get_line(); + graphml[node].thread_nr=it->source.thread_nr; + + step_to_node[step_nr]=node; + } + + // build edges + step_nr=1; + for(symex_target_equationt::SSA_stepst::const_iterator + it=equation.SSA_steps.begin(); + it!=equation.SSA_steps.end(); + ) // no ++it + { + const std::size_t from=step_to_node[step_nr]; + + if(from==sink) + { + ++it; ++step_nr; + continue; + } + + symex_target_equationt::SSA_stepst::const_iterator next=it; + std::size_t next_step_nr=step_nr; + for(++next, ++next_step_nr; + next!=equation.SSA_steps.end() && + (step_to_node[next_step_nr]==sink || + it->source.pc==next->source.pc); + ++next, ++next_step_nr) + ; + const std::size_t to= + next==equation.SSA_steps.end()? + sink:step_to_node[next_step_nr]; + + switch(it->type) + { + case goto_trace_stept::ASSIGNMENT: + case goto_trace_stept::ASSERT: + case goto_trace_stept::GOTO: + { + xmlt edge("edge"); + edge.set_attribute("source", graphml[from].node_name); + edge.set_attribute("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_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(); + + xmlt &val=edge.new_element("data"); + val.set_attribute("key", "invariant"); + code_assignt assign(it->ssa_full_lhs, it->ssa_rhs); + val.data=convert_assign_rec(identifier, assign); + + xmlt &val_s=edge.new_element("data"); + val_s.set_attribute("key", "invariant.scope"); + val_s.data=id2string(it->source.pc->source_location.get_function()); + } + 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->cond_expr); + from_expr(ns, "", not_exprt(it->cond_expr)); + val.data="["+cond+"]"; + } + + graphml[to].in[from].xml_node=edge; + graphml[from].out[to].xml_node=edge; + } + break; + + case goto_trace_stept::DECL: + case goto_trace_stept::FUNCTION_CALL: + case goto_trace_stept::FUNCTION_RETURN: + case goto_trace_stept::LOCATION: + case goto_trace_stept::ASSUME: + case goto_trace_stept::INPUT: + case goto_trace_stept::OUTPUT: + case goto_trace_stept::SHARED_READ: + case goto_trace_stept::SHARED_WRITE: + case goto_trace_stept::SPAWN: + case goto_trace_stept::MEMORY_BARRIER: + case goto_trace_stept::ATOMIC_BEGIN: + case goto_trace_stept::ATOMIC_END: + case goto_trace_stept::DEAD: + case goto_trace_stept::CONSTRAINT: + case goto_trace_stept::NONE: + ; /* ignore */ + } + + it=next; + step_nr=next_step_nr; + } } From 1ed64d3380298fa03560a2bddfdac421565932bb Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2016 16:40:49 +0000 Subject: [PATCH 4/9] generate graph attributes from key value pairs --- src/goto-programs/graphml_witness.cpp | 12 ------------ src/xmllang/graphml.cpp | 11 +++++++---- src/xmllang/graphml.h | 3 +++ 3 files changed, 10 insertions(+), 16 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 0ed98ff9fa7..70c8b0492b6 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -145,13 +145,7 @@ Function: graphml_witnesst::operator() void graphml_witnesst::operator()(const goto_tracet &goto_trace) { - graphml.key_values["witness-type"]="violation_witness"; graphml.key_values["sourcecodelang"]="C"; - graphml.key_values["producer"]=""; - graphml.key_values["programfile"]=""; - graphml.key_values["programhash"]=""; - graphml.key_values["specification"]=""; - graphml.key_values["architecture"]=""; const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; @@ -341,13 +335,7 @@ Function: graphml_witnesst::operator() void graphml_witnesst::operator()(const symex_target_equationt &equation) { - graphml.key_values["witness-type"]="correctness_witness"; graphml.key_values["sourcecodelang"]="C"; - graphml.key_values["producer"]=""; - graphml.key_values["programfile"]=""; - graphml.key_values["programhash"]=""; - graphml.key_values["specification"]=""; - graphml.key_values["architecture"]=""; const graphmlt::node_indext sink=graphml.add_node(); graphml[sink].node_name="sink"; diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index b4a05e63fb5..1fabd9026fd 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -295,7 +295,10 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("for", "edge"); key.set_attribute("id", "originfile"); - key.new_element("default").data=""; + if(src.key_values.find("programfile")!=src.key_values.end()) + key.new_element("default").data=src.key_values.at("programfile"); + else + key.new_element("default").data=""; } // @@ -559,11 +562,11 @@ bool write_graphml(const graphmlt &src, std::ostream &os) xmlt &graph=graphml.new_element("graph"); graph.set_attribute("edgedefault", "directed"); - // C + for(const auto &kv : src.key_values) { xmlt &data=graph.new_element("data"); - data.set_attribute("key", "sourcecodelang"); - data.data="C"; + data.set_attribute("key", kv.first); + data.data=kv.second; } bool entry_done=false; diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index c32d2b0ede1..177076df0e2 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -56,6 +56,9 @@ class graphmlt : public graph return graph::add_node(); } + + typedef std::map key_valuest; + key_valuest key_values; }; bool read_graphml( From 9b4ce66263419d56ffed8844d5e6a3f2f95ad8cc Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 4 Dec 2016 23:10:14 +0000 Subject: [PATCH 5/9] Invariants must be added to nodes --- src/goto-programs/graphml_witness.cpp | 16 +++++++++------- src/xmllang/graphml.cpp | 12 ++++++++++++ src/xmllang/graphml.h | 3 +++ 3 files changed, 24 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 70c8b0492b6..d08367f990d 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -151,6 +151,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) graphml[sink].node_name="sink"; graphml[sink].thread_nr=0; graphml[sink].is_violation=false; + graphml[sink].has_invariant=false; // step numbers start at 1 std::vector step_to_node(goto_trace.steps.size()+1, 0); @@ -196,6 +197,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) graphml[node].thread_nr=it->thread_nr; graphml[node].is_violation= it->type==goto_trace_stept::ASSERT && !it->cond_value; + graphml[node].has_invariant=false; step_to_node[it->step_nr]=node; } @@ -341,6 +343,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) graphml[sink].node_name="sink"; graphml[sink].thread_nr=0; graphml[sink].is_violation=false; + graphml[sink].has_invariant=false; // step numbers start at 1 std::vector step_to_node(equation.SSA_steps.size()+1, 0); @@ -384,6 +387,8 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) 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; step_to_node[step_nr]=node; } @@ -442,14 +447,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) { irep_idt identifier=it->ssa_lhs.get_object_name(); - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "invariant"); + graphml[to].has_invariant=true; code_assignt assign(it->ssa_full_lhs, it->ssa_rhs); - val.data=convert_assign_rec(identifier, assign); - - xmlt &val_s=edge.new_element("data"); - val_s.set_attribute("key", "invariant.scope"); - val_s.data=id2string(it->source.pc->source_location.get_function()); + graphml[to].invariant=convert_assign_rec(identifier, assign); + graphml[to].invariant_scope= + id2string(it->source.pc->source_location.get_function()); } else if(it->is_goto() && it->source.pc->is_goto()) diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 1fabd9026fd..95ed8b10646 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -75,6 +75,7 @@ static bool build_graph_rec( graphmlt::nodet &node=dest[n]; node.node_name=node_name; node.is_violation=false; + node.has_invariant=false; node.thread_nr=0; for(xmlt::elementst::const_iterator @@ -607,6 +608,17 @@ bool write_graphml(const graphmlt &src, std::ostream &os) entry.data="true"; } + if(n.has_invariant) + { + xmlt &val=node.new_element("data"); + val.set_attribute("key", "invariant"); + val.data=n.invariant; + + xmlt &val_s=node.new_element("data"); + val_s.set_attribute("key", "invariant.scope"); + val_s.data=n.invariant_scope; + } + for(graphmlt::edgest::const_iterator e_it=n.out.begin(); e_it!=n.out.end(); diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index 177076df0e2..31fa06fce64 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -32,6 +32,9 @@ struct xml_graph_nodet:public graph_nodet irep_idt line; unsigned thread_nr; bool is_violation; + bool has_invariant; + std::string invariant; + std::string invariant_scope; }; class graphmlt : public graph From 4156c4fb37f26b0b882f9fd3ef39a46d0f7fc2f5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 18 Dec 2016 14:51:02 +0000 Subject: [PATCH 6/9] Fix bugs in witness output of struct assignments Dereferencing may yield the first struct member as left-hand-side. Skipping padding must be done such as not to skip a field on the left-hand side. --- src/goto-programs/graphml_witness.cpp | 50 ++++++++++++++++++++------- 1 file changed, 37 insertions(+), 13 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index d08367f990d..24a8d494045 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening #include +#include +#include #include #include #include @@ -91,32 +93,53 @@ std::string graphml_witnesst::convert_assign_rec( else if(assign.rhs().id()==ID_struct || assign.rhs().id()==ID_union) { + // dereferencing may have resulted in an lhs that is the first + // struct member; undo this + if(assign.lhs().id()==ID_member && + !base_type_eq(assign.lhs().type(), assign.rhs().type(), ns)) + { + code_assignt tmp=assign; + tmp.lhs()=to_member_expr(assign.lhs()).struct_op(); + + return convert_assign_rec(identifier, tmp); + } + else if(assign.lhs().id()==ID_byte_extract_little_endian || + assign.lhs().id()==ID_byte_extract_big_endian) + { + code_assignt tmp=assign; + tmp.lhs()=to_byte_extract_expr(assign.lhs()).op(); + + return convert_assign_rec(identifier, tmp); + } + const struct_union_typet &type= to_struct_union_type(ns.follow(assign.lhs().type())); const struct_union_typet::componentst &components= type.components(); - struct_union_typet::componentst::const_iterator c_it= - components.begin(); - forall_operands(it, assign.rhs()) + exprt::operandst::const_iterator it= + assign.rhs().operands().begin(); + for(const auto & comp : components) { - if(c_it->type().id()==ID_code || - c_it->get_is_padding() || + if(comp.type().id()==ID_code || + comp.get_is_padding() || // for some reason #is_padding gets lost in *some* cases - has_prefix(id2string(c_it->get_name()), "$pad")) - { - ++c_it; + has_prefix(id2string(comp.get_name()), "$pad")) continue; - } - assert(c_it!=components.end()); + assert(it!=assign.rhs().operands().end()); + member_exprt member( assign.lhs(), - c_it->get_name(), + comp.get_name(), it->type()); if(!result.empty()) result+=' '; result+=convert_assign_rec(identifier, code_assignt(member, *it)); - ++c_it; + ++it; + + // for unions just assign to the first member + if(assign.rhs().id()==ID_union) + break; } } else @@ -404,7 +427,8 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) if(from==sink) { - ++it; ++step_nr; + ++it; + ++step_nr; continue; } From 375a2a80d7e574d05639c0b94a03cbb87d53b8fb Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 18 Dec 2016 18:22:40 +0000 Subject: [PATCH 7/9] Filter out duplicate source locations in witness --- src/goto-programs/graphml_witness.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 24a8d494045..3c5c7589d9f 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening \*******************************************************************/ -#include - #include #include #include @@ -179,6 +177,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) // step numbers start at 1 std::vector step_to_node(goto_trace.steps.size()+1, 0); + goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end(); for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin(); it!=goto_trace.steps.end(); @@ -188,6 +187,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) if(it->hidden || (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || + // we filter out steps with the same source location + // TODO: if these are assignments we should accumulate them into + // a single edge + (prev_it!=goto_trace.steps.end() && + prev_it->pc->source_location==it->pc->source_location) || (it->is_goto() && it->pc->guard.is_true()) || source_location.is_nil() || source_location.get_file().empty() || @@ -212,6 +216,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) continue; } + prev_it=it; + const graphmlt::node_indext node=graphml.add_node(); graphml[node].node_name= i2string(it->pc->location_number)+"."+i2string(it->step_nr); From 3679aee3b252ecb775e07f14322f4d8eb957b4e4 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 27 Dec 2016 14:58:47 +0100 Subject: [PATCH 8/9] Fix linter warnings --- src/goto-programs/graphml_witness.cpp | 44 +++++++++++++++------------ src/goto-programs/graphml_witness.h | 1 - src/xmllang/graphml.cpp | 10 ++++-- src/xmllang/graphml.h | 2 +- 4 files changed, 33 insertions(+), 24 deletions(-) diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 3c5c7589d9f..f29a759f8ce 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -81,10 +81,11 @@ std::string graphml_witnesst::convert_assign_rec( forall_operands(it, assign.rhs()) { index_exprt index( - assign.lhs(), - from_integer(i++, signedbv_typet(config.ansi_c.pointer_width)), - type.subtype()); - if(!result.empty()) result+=' '; + assign.lhs(), + from_integer(i++, signedbv_typet(config.ansi_c.pointer_width)), + type.subtype()); + if(!result.empty()) + result+=' '; result+=convert_assign_rec(identifier, code_assignt(index, *it)); } } @@ -128,10 +129,11 @@ std::string graphml_witnesst::convert_assign_rec( assert(it!=assign.rhs().operands().end()); member_exprt member( - assign.lhs(), - comp.get_name(), - it->type()); - if(!result.empty()) result+=' '; + assign.lhs(), + comp.get_name(), + it->type()); + if(!result.empty()) + result+=' '; result+=convert_assign_rec(identifier, code_assignt(member, *it)); ++it; @@ -181,7 +183,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) for(goto_tracet::stepst::const_iterator it=goto_trace.steps.begin(); it!=goto_trace.steps.end(); - it++) //we cannot replace this by a ranged for + it++) // we cannot replace this by a ranged for { const source_locationt &source_location=it->pc->source_location; @@ -248,10 +250,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) goto_tracet::stepst::const_iterator next=it; for(++next; next!=goto_trace.steps.end() && - (step_to_node[next->step_nr]==sink || - it->pc==next->pc); + (step_to_node[next->step_nr]==sink || it->pc==next->pc); ++next) - ; + { + // advance + } const std::size_t to= next==goto_trace.steps.end()? sink:step_to_node[next->step_nr]; @@ -345,7 +348,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::DEAD: case goto_trace_stept::CONSTRAINT: case goto_trace_stept::NONE: - ; /* ignore */ + // ignore + break; } it=next; @@ -381,7 +385,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) for(symex_target_equationt::SSA_stepst::const_iterator it=equation.SSA_steps.begin(); it!=equation.SSA_steps.end(); - it++, step_nr++) //we cannot replace this by a ranged for + it++, step_nr++) // we cannot replace this by a ranged for { const source_locationt &source_location=it->source.pc->source_location; @@ -442,10 +446,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) std::size_t next_step_nr=step_nr; for(++next, ++next_step_nr; next!=equation.SSA_steps.end() && - (step_to_node[next_step_nr]==sink || - it->source.pc==next->source.pc); + (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc); ++next, ++next_step_nr) - ; + { + // advance + } const std::size_t to= next==equation.SSA_steps.end()? sink:step_to_node[next_step_nr]; @@ -514,10 +519,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::DEAD: case goto_trace_stept::CONSTRAINT: case goto_trace_stept::NONE: - ; /* ignore */ + // ignore + break; } - it=next; + it=next; step_nr=next_step_nr; } } diff --git a/src/goto-programs/graphml_witness.h b/src/goto-programs/graphml_witness.h index 8ec1400938f..f8ed1a614d9 100644 --- a/src/goto-programs/graphml_witness.h +++ b/src/goto-programs/graphml_witness.h @@ -39,7 +39,6 @@ class graphml_witnesst std::string convert_assign_rec( const irep_idt &identifier, const code_assignt &assign); - }; #endif // CPROVER_GOTO_PROGRAMS_GRAPHML_WITNESS_H diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 95ed8b10646..57ae2626f57 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -282,8 +282,12 @@ Function: write_graphml bool write_graphml(const graphmlt &src, std::ostream &os) { xmlt graphml("graphml"); - graphml.set_attribute("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"); - graphml.set_attribute("xmlns", "http://graphml.graphdrawing.org/xmlns"); + graphml.set_attribute( + "xmlns:xsi", + "http://www.w3.org/2001/XMLSchema-instance"); + graphml.set_attribute( + "xmlns", + "http://graphml.graphdrawing.org/xmlns"); // @@ -311,7 +315,7 @@ bool write_graphml(const graphmlt &src, std::ostream &os) key.set_attribute("id", "invariant"); } - // { xmlt &key=graphml.new_element("key"); diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index 31fa06fce64..5a56fef1196 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -37,7 +37,7 @@ struct xml_graph_nodet:public graph_nodet std::string invariant_scope; }; -class graphmlt : public graph +class graphmlt:public graph { public: inline bool has_node(const std::string &node_name) const From dd2d3b03abfc0920a29e1218ba39bc2cf099a0f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 28 Dec 2016 10:00:21 +0100 Subject: [PATCH 9/9] Code formatting in bmc.cpp (using string_utils) --- src/cbmc/bmc.cpp | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 5413dc74c40..f3a2c466cbc 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -381,8 +382,9 @@ void bmct::show_program() { std::string string_value; languages.from_expr(step.ssa_lhs, string_value); - std::cout << "(" << count << ") SHARED_" << (step.is_shared_write()?"WRITE":"READ") << "(" - << string_value <<") " << "\n"; + std::cout << "(" << count << ") SHARED_" + << (step.is_shared_write()?"WRITE":"READ") + << "(" << string_value <<")\n"; if(!step.guard.is_true()) { @@ -665,13 +667,11 @@ Function: bmct::setup_unwind void bmct::setup_unwind() { const std::string &set=options.get_option("unwindset"); - std::string::size_type length=set.length(); + std::vector unwindset_loops; + split_string(set, ',', unwindset_loops, true, true); - for(std::string::size_type idx=0; idx