Skip to content

Commit 8140079

Browse files
peterschrammelpeterschrammel
committed
Factor out bmct building blocks int bmc_util
This is an intermediate step in order to reuse the building blocks in the new implementation of bmct. The old implementation is functional until it can be replaced by the new one.
1 parent b420234 commit 8140079

File tree

7 files changed

+346
-0
lines changed

7 files changed

+346
-0
lines changed

‎jbmc/src/jbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
4040
../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
4141
../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
4242
../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
43+
../$(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \
4344
../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
4445
../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
4546
../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \

‎jbmc/unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ java-testing-utils-clean:
8585
BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
8686
$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
8787
$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
88+
$(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \
8889
$(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
8990
$(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
9091
$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \

‎src/cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
SRC = all_properties.cpp \
22
bmc.cpp \
33
bmc_cover.cpp \
4+
bmc_util.cpp \
45
cbmc_languages.cpp \
56
cbmc_main.cpp \
67
cbmc_parse_options.cpp \

‎src/cbmc/bmc.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
2727
#include <goto-checker/bmc_util.h>
2828
#include <goto-checker/solver_factory.h>
2929

30+
#include "bmc_util.h"
3031
#include "counterexample_beautification.h"
3132
#include "fault_localization.h"
3233

‎src/cbmc/bmc_util.cpp

Lines changed: 267 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,267 @@
1+
/*******************************************************************\
2+
3+
Module: Bounded Model Checking Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Bounded Model Checking Utilities
11+
12+
#include "bmc_util.h"
13+
14+
#include <fstream>
15+
#include <iostream>
16+
17+
#include <cbmc/symex_bmc.h>
18+
19+
#include <goto-programs/graphml_witness.h>
20+
#include <goto-programs/json_goto_trace.h>
21+
#include <goto-programs/xml_goto_trace.h>
22+
23+
#include <goto-symex/build_goto_trace.h>
24+
#include <goto-symex/memory_model_pso.h>
25+
#include <goto-symex/slice.h>
26+
#include <goto-symex/slice_by_trace.h>
27+
#include <goto-symex/symex_target_equation.h>
28+
29+
#include <linking/static_lifetime_init.h>
30+
31+
#include <solvers/prop/prop_conv.h>
32+
33+
#include <util/make_unique.h>
34+
#include <util/ui_message.h>
35+
36+
void build_error_trace(
37+
goto_tracet &goto_trace,
38+
const namespacet &ns,
39+
const symex_target_equationt &symex_target_equation,
40+
const prop_convt &prop_conv,
41+
ui_message_handlert &ui_message_handler)
42+
{
43+
messaget msg(ui_message_handler);
44+
msg.status() << "Building error trace" << messaget::eom;
45+
46+
build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace);
47+
}
48+
49+
void output_error_trace(
50+
const goto_tracet &goto_trace,
51+
const namespacet &ns,
52+
const trace_optionst &trace_options,
53+
ui_message_handlert &ui_message_handler)
54+
{
55+
messaget msg(ui_message_handler);
56+
switch(ui_message_handler.get_ui())
57+
{
58+
case ui_message_handlert::uit::PLAIN:
59+
msg.result() << "Counterexample:" << messaget::eom;
60+
show_goto_trace(msg.result(), ns, goto_trace, trace_options);
61+
msg.result() << messaget::eom;
62+
break;
63+
64+
case ui_message_handlert::uit::XML_UI:
65+
{
66+
xmlt xml;
67+
convert(ns, goto_trace, xml);
68+
msg.status() << xml;
69+
}
70+
break;
71+
72+
case ui_message_handlert::uit::JSON_UI:
73+
{
74+
json_stream_objectt &json_result =
75+
ui_message_handler.get_json_stream().push_back_stream_object();
76+
const goto_trace_stept &step = goto_trace.steps.back();
77+
json_result["property"] =
78+
json_stringt(step.pc->source_location.get_property_id());
79+
json_result["description"] =
80+
json_stringt(step.pc->source_location.get_comment());
81+
json_result["status"] = json_stringt("failed");
82+
json_stream_arrayt &json_trace =
83+
json_result.push_back_stream_array("trace");
84+
convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
85+
}
86+
break;
87+
}
88+
}
89+
90+
/// outputs witnesses in graphml format
91+
void output_graphml(
92+
safety_checkert::resultt result,
93+
const goto_tracet &goto_trace,
94+
const symex_target_equationt &symex_target_equation,
95+
const namespacet &ns,
96+
const optionst &options)
97+
{
98+
const std::string graphml = options.get_option("graphml-witness");
99+
if(graphml.empty())
100+
return;
101+
102+
graphml_witnesst graphml_witness(ns);
103+
if(result == safety_checkert::resultt::UNSAFE)
104+
graphml_witness(goto_trace);
105+
else if(result == safety_checkert::resultt::SAFE)
106+
graphml_witness(symex_target_equation);
107+
else
108+
return;
109+
110+
if(graphml == "-")
111+
write_graphml(graphml_witness.graph(), std::cout);
112+
else
113+
{
114+
std::ofstream out(graphml);
115+
write_graphml(graphml_witness.graph(), out);
116+
}
117+
}
118+
119+
void convert_symex_target_equation(
120+
symex_target_equationt &equation,
121+
prop_convt &prop_conv,
122+
message_handlert &message_handler)
123+
{
124+
messaget msg(message_handler);
125+
msg.status() << "converting SSA" << messaget::eom;
126+
127+
// convert SSA
128+
equation.convert(prop_conv);
129+
}
130+
131+
std::unique_ptr<memory_model_baset>
132+
get_memory_model(const optionst &options, const namespacet &ns)
133+
{
134+
const std::string mm = options.get_option("mm");
135+
136+
if(mm.empty() || mm == "sc")
137+
return util_make_unique<memory_model_sct>(ns);
138+
else if(mm == "tso")
139+
return util_make_unique<memory_model_tsot>(ns);
140+
else if(mm == "pso")
141+
return util_make_unique<memory_model_psot>(ns);
142+
else
143+
{
144+
throw "invalid memory model '" + mm + "': use one of sc, tso, pso";
145+
}
146+
}
147+
148+
void setup_symex(
149+
symex_bmct &symex,
150+
const namespacet &ns,
151+
const optionst &options,
152+
ui_message_handlert &ui_message_handler)
153+
{
154+
messaget msg(ui_message_handler);
155+
const symbolt *init_symbol;
156+
if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
157+
symex.language_mode = init_symbol->mode;
158+
159+
msg.status() << "Starting Bounded Model Checking" << messaget::eom;
160+
161+
symex.last_source_location.make_nil();
162+
163+
symex.unwindset.parse_unwind(options.get_option("unwind"));
164+
symex.unwindset.parse_unwindset(options.get_option("unwindset"));
165+
}
166+
167+
void slice(
168+
symex_bmct &symex,
169+
symex_target_equationt &symex_target_equation,
170+
const namespacet &ns,
171+
const optionst &options,
172+
ui_message_handlert &ui_message_handler)
173+
{
174+
messaget msg(ui_message_handler);
175+
if(options.get_option("slice-by-trace") != "")
176+
{
177+
symex_slice_by_tracet symex_slice_by_trace(ns);
178+
179+
symex_slice_by_trace.slice_by_trace(
180+
options.get_option("slice-by-trace"), symex_target_equation);
181+
}
182+
// any properties to check at all?
183+
if(symex_target_equation.has_threads())
184+
{
185+
// we should build a thread-aware SSA slicer
186+
msg.statistics() << "no slicing due to threads" << messaget::eom;
187+
}
188+
else
189+
{
190+
if(options.get_bool_option("slice-formula"))
191+
{
192+
::slice(symex_target_equation);
193+
msg.statistics() << "slicing removed "
194+
<< symex_target_equation.count_ignored_SSA_steps()
195+
<< " assignments" << messaget::eom;
196+
}
197+
else
198+
{
199+
if(options.get_list_option("cover").empty())
200+
{
201+
simple_slice(symex_target_equation);
202+
msg.statistics() << "simple slicing removed "
203+
<< symex_target_equation.count_ignored_SSA_steps()
204+
<< " assignments" << messaget::eom;
205+
}
206+
}
207+
}
208+
msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
209+
<< symex.get_remaining_vccs()
210+
<< " remaining after simplification" << messaget::eom;
211+
}
212+
213+
void report_success(ui_message_handlert &ui_message_handler)
214+
{
215+
messaget msg(ui_message_handler);
216+
msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
217+
218+
switch(ui_message_handler.get_ui())
219+
{
220+
case ui_message_handlert::uit::PLAIN:
221+
break;
222+
223+
case ui_message_handlert::uit::XML_UI:
224+
{
225+
xmlt xml("cprover-status");
226+
xml.data = "SUCCESS";
227+
msg.result() << xml;
228+
}
229+
break;
230+
231+
case ui_message_handlert::uit::JSON_UI:
232+
{
233+
json_objectt json_result;
234+
json_result["cProverStatus"] = json_stringt("success");
235+
msg.result() << json_result;
236+
}
237+
break;
238+
}
239+
}
240+
241+
void report_failure(ui_message_handlert &ui_message_handler)
242+
{
243+
messaget msg(ui_message_handler);
244+
msg.result() << "VERIFICATION FAILED" << messaget::eom;
245+
246+
switch(ui_message_handler.get_ui())
247+
{
248+
case ui_message_handlert::uit::PLAIN:
249+
break;
250+
251+
case ui_message_handlert::uit::XML_UI:
252+
{
253+
xmlt xml("cprover-status");
254+
xml.data = "FAILURE";
255+
msg.result() << xml;
256+
}
257+
break;
258+
259+
case ui_message_handlert::uit::JSON_UI:
260+
{
261+
json_objectt json_result;
262+
json_result["cProverStatus"] = json_stringt("failure");
263+
msg.result() << json_result;
264+
}
265+
break;
266+
}
267+
}

‎src/cbmc/bmc_util.h

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
/*******************************************************************\
2+
3+
Module: Bounded Model Checking Utilities
4+
5+
Author: Daniel Kroening, Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Bounded Model Checking Utilities
11+
12+
#ifndef CPROVER_CBMC_BMC_UTIL_H
13+
#define CPROVER_CBMC_BMC_UTIL_H
14+
15+
#include <memory>
16+
17+
#include <goto-programs/safety_checker.h>
18+
19+
class goto_tracet;
20+
class memory_model_baset;
21+
class message_handlert;
22+
class namespacet;
23+
class optionst;
24+
class prop_convt;
25+
class symex_bmct;
26+
class symex_target_equationt;
27+
struct trace_optionst;
28+
class ui_message_handlert;
29+
30+
void convert_symex_target_equation(
31+
symex_target_equationt &,
32+
prop_convt &,
33+
message_handlert &);
34+
35+
void report_failure(ui_message_handlert &);
36+
void report_success(ui_message_handlert &);
37+
38+
void build_error_trace(
39+
goto_tracet &,
40+
const namespacet &,
41+
const symex_target_equationt &,
42+
const prop_convt &,
43+
ui_message_handlert &);
44+
45+
void output_error_trace(
46+
const goto_tracet &,
47+
const namespacet &,
48+
const trace_optionst &,
49+
ui_message_handlert &);
50+
51+
void output_graphml(
52+
safety_checkert::resultt,
53+
const goto_tracet &,
54+
const symex_target_equationt &,
55+
const namespacet &,
56+
const optionst &);
57+
58+
std::unique_ptr<memory_model_baset>
59+
get_memory_model(const optionst &options, const namespacet &);
60+
61+
void setup_symex(
62+
symex_bmct &,
63+
const namespacet &,
64+
const optionst &,
65+
ui_message_handlert &);
66+
67+
void slice(
68+
symex_bmct &,
69+
symex_target_equationt &symex_target_equation,
70+
const namespacet &,
71+
const optionst &,
72+
ui_message_handlert &);
73+
74+
#endif // CPROVER_CBMC_BMC_UTIL_H

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,7 @@ testing-utils-clean:
8989
BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
9090
../src/cbmc/bmc$(OBJEXT) \
9191
../src/cbmc/bmc_cover$(OBJEXT) \
92+
../src/cbmc/bmc_util$(OBJEXT) \
9293
../src/cbmc/cbmc_languages$(OBJEXT) \
9394
../src/cbmc/cbmc_parse_options$(OBJEXT) \
9495
../src/cbmc/counterexample_beautification$(OBJEXT) \

0 commit comments

Comments
 (0)