CBMC: /home/runner/work/cbmc/cbmc/src/goto-analyzer/static_verifier.cpp Source File

CBMC
Loading...
Searching...
No Matches
static_verifier.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: goto-analyzer
4
5Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7\*******************************************************************/
8
9#include "static_verifier.h"
10
11#include <util/json_irep.h>
12#include <util/message.h>
13#include <util/namespace.h>
14#include <util/options.h>
15#include <util/range.h>
16#include <util/xml_irep.h>
17
18#include <goto-programs/goto_model.h>
19
20#include <analyses/ai.h>
21
23 std::string as_string(const ai_verifier_statust &status)
24{
25 switch(status)
26 {
28 return "SUCCESS";
30 return "FAILURE (if reachable)";
32 return "SUCCESS (unreachable)";
34 return "UNKNOWN";
35 }
37}
38
40{
42 for(const auto &trace_ptr : this->unknown_histories)
43 unknown_json.push_back(trace_ptr->output_json());
44
46 for(const auto &trace_ptr : this->false_histories)
47 false_json.push_back(trace_ptr->output_json());
48
49 return json_objectt{
50 {"status", json_stringt{as_string(this->status)}},
51 {"sourceLocation", json(this->source_location)},
52 {"unknownHistories", unknown_json},
53 {"falseHistories", false_json},
54 };
55}
56
58{
59 xmlt x("result");
60
61 x.set_attribute("status", as_string(this->status));
62
63 // DEPRECATED(SINCE(2020, 12, 2, "Remove and use the structured version"));
64 // Unstructured partial output of source location is not great...
67
68 // ... this is better
70
71 // ( get_comment is not output as part of xml(source_location) )
72 x.set_attribute(
73 "description", id2string(this->source_location.get_comment()));
74
75 xmlt &unknown_xml = x.new_element("unknown");
76 for(const auto &trace_ptr : this->unknown_histories)
77 unknown_xml.new_element(trace_ptr->output_xml());
78
79 xmlt &false_xml = x.new_element("false");
80 for(const auto &trace_ptr : this->false_histories)
81 false_xml.new_element(trace_ptr->output_xml());
82
83 return x;
84}
85
86static ai_verifier_statust
87 check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
88{
89 if(domain.is_bottom())
90 {
92 }
93
94 domain.ai_simplify(e, ns);
95 if(e == true)
96 {
98 }
99 else if(e == false)
100 {
102 }
103 else
104 {
106 }
107
109}
110
112 const ai_baset &ai,
115 const namespacet &ns)
116{
117 PRECONDITION(assert_location->is_assert());
118 exprt e(assert_location->condition());
119
120 // If there are multiple, distinct histories that reach the same location
121 // we can get better results by checking with each individually rather
122 // than merging all of them and doing one check.
124 assert_location); // Keep a pointer so refcount > 0
125 const auto &trace_set = *trace_set_pointer;
126
127 if(trace_set.size() == 0) // i.e. unreachable
128 {
130 }
131 else if(trace_set.size() == 1)
132 {
134
135 status = check_assertion(*dp, e, ns);
137 {
139 }
141 {
143 }
144 }
145 else
146 {
147 // Multiple traces, verify against each one
148 std::size_t unreachable_traces = 0;
149 std::size_t true_traces = 0;
150 std::size_t false_traces = 0;
151 std::size_t unknown_traces = 0;
152
153 for(const auto &trace_ptr : trace_set)
154 {
156
157 status = check_assertion(*dp, e, ns);
158 switch(status)
159 {
162 break;
164 ++true_traces;
165 break;
167 ++false_traces;
169 break;
173 break;
174 default:
176 }
177 }
178
179 // Join the results
180 if(unknown_traces != 0)
181 {
182 // If any trace is unknown, the final result must be unknown
184 }
185 else
186 {
187 if(false_traces == 0)
188 {
189 // Definitely true; the only question is how
190 if(true_traces == 0)
191 {
192 // Definitely not reachable
193 INVARIANT(
195 "All traces must not reach the assertion");
197 }
198 else
199 {
200 // At least one trace (may) reach it.
201 // All traces that reach it are safe.
203 }
204 }
205 else
206 {
207 // At lease one trace (may) reach it and it is false on that trace
208 if(true_traces == 0)
209 {
210 // All traces that (may) reach it are false
212 }
213 else
214 {
215 // The awkward case, there are traces that (may) reach it and
216 // some are true, some are false. It is not entirely fair to say
217 // "FAILURE (if reachable)" because it's a bit more complex than
218 // that, and so the best we can say is UNKNOWN.
220 }
221 }
222 }
223 }
224
225 source_location = assert_location->source_location();
227}
228
231 const ai_baset &ai,
232 propertiest &properties)
233{
234 const namespacet ns{abstract_goto_model.get_symbol_table()};
235 // this is mutable because we want to change the property status
236 // in this loop
237 for(auto &property : properties)
238 {
239 auto &property_status = property.second.status;
240 const goto_programt::const_targett &property_location = property.second.pc;
241
242 const static_verifier_resultt result(ai, property_location, "unused", ns);
243
244 switch(result.status)
245 {
247 // if the condition simplifies to true the assertion always succeeds
249 break;
251 // if the condition simplifies to false the assertion always fails
253 break;
255 // if the domain state is bottom then the assertion is definitely
256 // unreachable
258 break;
260 // if the condition isn't definitely true, false or unreachable
261 // we don't know whether or not it may fail
263 break;
264 default:
266 }
267 }
268}
269
271 const std::vector<static_verifier_resultt> &results,
272 messaget &m,
273 std::ostream &out)
274{
275 m.status() << "Writing JSON report" << messaget::eom;
276 out << make_range(results)
277 .map([](const static_verifier_resultt &result) {
278 return result.output_json();
279 })
281}
282
284 const std::vector<static_verifier_resultt> &results,
285 messaget &m,
286 std::ostream &out)
287{
288 m.status() << "Writing XML report" << messaget::eom;
289
290 xmlt xml_result{"cprover"};
291 for(const auto &result : results)
292 xml_result.new_element(result.output_xml());
293
294 out << xml_result;
295}
296
298 const std::vector<static_verifier_resultt> &results,
299 const namespacet &ns,
300 std::ostream &out)
301{
303
304 for(const auto &result : results)
305 {
306 if(last_function_id != result.function_id)
307 {
308 if(!last_function_id.empty())
309 out << '\n';
310 last_function_id = result.function_id;
311 const auto &symbol = ns.lookup(last_function_id);
312 out << "******** Function " << symbol.display_name() << '\n';
313 }
314
315 out << '[' << result.source_location.get_property_id() << ']' << ' ';
316
317 out << result.source_location;
318
319 if(!result.source_location.get_comment().empty())
320 out << ", " << result.source_location.get_comment();
321
322 out << ": " << as_string(result.status) << '\n';
323 }
324}
325
327 const std::vector<static_verifier_resultt> &results,
328 const namespacet &ns,
329 messaget &m)
330{
333
334 for(const auto &result : results)
335 {
336 if(last_function_id != result.function_id)
337 {
338 if(!last_function_id.empty())
339 m.status() << '\n';
340 last_function_id = result.function_id;
341 const auto &symbol = ns.lookup(last_function_id);
342 m.status() << messaget::underline << "Function " << symbol.display_name();
343 function_file = symbol.location.get_file();
344 if(!function_file.empty())
345 m.status() << ' ' << function_file;
346 if(!symbol.location.get_line().empty())
347 m.status() << ':' << symbol.location.get_line();
349 }
350
351 m.result() << messaget::faint << '['
352 << result.source_location.get_property_id() << ']'
354
355 if(
356 !result.source_location.get_file().empty() &&
357 result.source_location.get_file() != function_file)
358 {
359 m.result() << " file " << result.source_location.get_file();
360 }
361
362 if(!result.source_location.get_line().empty())
363 m.result() << " line " << result.source_location.get_line();
364
365 if(!result.source_location.get_comment().empty())
366 m.result() << ' ' << result.source_location.get_comment();
367
368 m.result() << ": ";
369
370 switch(result.status)
371 {
373 m.result() << m.green << "SUCCESS" << m.reset;
374 break;
375
377 m.result() << m.red << "FAILURE" << m.reset << " (if reachable)";
378 break;
379
381 m.result() << m.green << "SUCCESS" << m.reset << " (unreachable)";
382 break;
383
385 m.result() << m.yellow << "UNKNOWN" << m.reset;
386 break;
387 }
388
389 m.result() << messaget::eom;
390 }
391
392 if(!results.empty())
393 m.result() << '\n';
394}
395
404 const goto_modelt &goto_model,
405 const ai_baset &ai,
406 const optionst &options,
407 message_handlert &message_handler,
408 std::ostream &out)
409{
410 std::size_t pass = 0, fail = 0, unknown = 0;
411
412 namespacet ns(goto_model.symbol_table);
413
414 messaget m(message_handler);
415 m.status() << "Checking assertions" << messaget::eom;
416
417 std::vector<static_verifier_resultt> results;
418
419 for(const auto &f : goto_model.goto_functions.function_map)
420 {
421 const auto &symbol = ns.lookup(f.first);
422
423 m.progress() << "Checking " << symbol.display_name() << messaget::eom;
424
425 if(!f.second.body.has_assertion())
426 continue;
427
429 {
430 if(!i_it->is_assert())
431 continue;
432
433 results.push_back(static_verifier_resultt(ai, i_it, f.first, ns));
434
435 switch(results.back().status)
436 {
438 ++pass;
439 break;
441 ++pass;
442 break;
444 ++fail;
445 break;
447 ++unknown;
448 break;
449 default:
451 }
452 }
453 }
454
455 if(options.get_bool_option("json"))
456 {
458 }
459 else if(options.get_bool_option("xml"))
460 {
462 }
463 else if(options.get_bool_option("text"))
464 {
466 }
467 else
468 {
470 }
471
472 m.status() << m.bold << "Summary: " << pass << " pass, " << fail
473 << " fail if reachable, " << unknown << " unknown" << m.reset
474 << messaget::eom;
475
476 return false;
477}
Abstract Interpretation.
Abstract interface to eager or lazy GOTO models.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:117
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
Definition ai.h:198
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition ai.h:225
virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition ai.cpp:136
virtual jsont output_json(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
Definition ai.cpp:83
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
virtual bool is_bottom() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition ai_domain.h:149
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
function_mapt function_map
Definition goto_model.h:27
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
instructionst::const_iterator const_targett
Definition goto_program.h:614
Definition json.h:165
jsont & push_back(const jsont &json)
Definition json.h:212
Definition json.h:298
Definition json.h:270
Definition json.h:27
Definition message.h:27
source_locationt source_location
Definition message.h:239
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static const commandt yellow
render text with yellow foreground color
Definition message.h:344
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:335
static const commandt green
render text with green foreground color
Definition message.h:341
static const commandt faint
render text with faint font
Definition message.h:377
mstreamt & progress() const
Definition message.h:426
static const commandt bold
render text with bold font
Definition message.h:374
static const commandt underline
render underlined text
Definition message.h:383
mstreamt & result() const
Definition message.h:411
static const commandt red
render text with red foreground color
Definition message.h:338
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:416
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition namespace.cpp:134
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
const irep_idt & get_file() const
const irep_idt & get_line() const
const irep_idt & get_comment() const
The result of verifying a single assertion As well as the status of the assertion (see above),...
ai_verifier_statust status
static_verifier_resultt(const ai_baset &ai, goto_programt::const_targett assert_location, irep_idt func_id, const namespacet &ns)
jsont output_json(void) const
irep_idt function_id
source_locationt source_location
ai_history_baset::trace_sett unknown_histories
ai_history_baset::trace_sett false_histories
xmlt output_xml(void) const
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition xml.cpp:198
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Util.
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition properties.cpp:120
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition properties.cpp:110
@ UNKNOWN
The checker was unable to determine the status of the property.
@ NOT_REACHABLE
The property was proven to be unreachable.
@ PASS
The property was not violated.
@ FAIL
The property was violated.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
static ai_verifier_statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
static void static_verifier_text(const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
std::string as_string(const ai_verifier_statust &)
Makes a status message string from a status.
ai_verifier_statust
An ai_baset contains zero or more histories that reach a location.
@ FALSE_IF_REACHABLE
@ UNKNOWN
@ NOT_REACHABLE
@ TRUE

AltStyle によって変換されたページ (->オリジナル) /