CBMC
properties.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Properties
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "properties.h"
13 
14 #include <util/exit_codes.h>
15 #include <util/invariant.h>
16 #include <util/json.h>
17 #include <util/json_irep.h>
18 #include <util/json_stream.h>
19 #include <util/xml.h>
20 #include <util/xml_irep.h>
21 
23 
24 std::string as_string(resultt result)
25 {
26  switch(result)
27  {
28  case resultt::UNKNOWN:
29  return "UNKNOWN";
30  case resultt::PASS:
31  return "PASS";
32  case resultt::FAIL:
33  return "FAIL";
34  case resultt::ERROR:
35  return "ERROR";
36  }
37 
39 }
40 
41 std::string as_string(property_statust status)
42 {
43  switch(status)
44  {
46  return "NOT CHECKED";
48  return "UNKNOWN";
50  return "UNREACHABLE";
52  return "SUCCESS";
54  return "FAILURE";
56  return "ERROR";
57  }
58 
60 }
61 
64  std::string description,
65  property_statust status)
66  : pc(pc), description(std::move(description)), status(status)
67 {
68 }
69 
71 {
72  propertiest properties;
73  update_properties_from_goto_model(properties, goto_model);
74  return properties;
75 }
76 
78  propertiest &properties,
79  const abstract_goto_modelt &goto_model)
80 {
81  const auto &goto_functions = goto_model.get_goto_functions();
82  for(const auto &function_pair : goto_functions.function_map)
83  {
84  const goto_programt &goto_program = function_pair.second.body;
85 
86  // need pointer to goto instruction
87  forall_goto_program_instructions(i_it, goto_program)
88  {
89  if(!i_it->is_assert())
90  continue;
91 
92  std::string description =
93  id2string(i_it->source_location().get_comment());
94  if(description.empty())
95  description = "assertion";
96  properties.emplace(
97  i_it->source_location().get_property_id(),
98  property_infot{i_it, description, property_statust::NOT_CHECKED});
99  }
100  }
101 }
102 
103 std::string
104 as_string(const irep_idt &property_id, const property_infot &property_info)
105 {
106  return "[" + id2string(property_id) + "] " + property_info.description +
107  ": " + as_string(property_info.status);
108 }
109 
110 xmlt xml(const irep_idt &property_id, const property_infot &property_info)
111 {
112  xmlt xml_result("result");
113  xml_result.set_attribute("property", id2string(property_id));
114  xml_result.set_attribute("status", as_string(property_info.status));
115  xml_result.new_element(xml(property_info.pc->source_location()));
116  return xml_result;
117 }
118 
119 template <class json_objectT>
120 static void json(
121  json_objectT &result,
122  const irep_idt &property_id,
123  const property_infot &property_info)
124 {
125  result["property"] = json_stringt(property_id);
126  result["description"] = json_stringt(property_info.description);
127  result["status"] = json_stringt(as_string(property_info.status));
128  result["sourceLocation"] = json(property_info.pc->source_location());
129 }
130 
132 json(const irep_idt &property_id, const property_infot &property_info)
133 {
134  json_objectt result;
135  json<json_objectt>(result, property_id, property_info);
136  return result;
137 }
138 
139 void json(
140  json_stream_objectt &result,
141  const irep_idt &property_id,
142  const property_infot &property_info)
143 {
144  json<json_stream_objectt>(result, property_id, property_info);
145 }
146 
148 {
149  switch(result)
150  {
151  case resultt::PASS:
153  case resultt::FAIL:
155  case resultt::ERROR:
157  case resultt::UNKNOWN:
159  }
160  UNREACHABLE;
161 }
162 
163 std::size_t
165 {
166  std::size_t count = 0;
167  for(const auto &property_pair : properties)
168  {
169  if(property_pair.second.status == status)
170  ++count;
171  }
172  return count;
173 }
174 
176 {
177  return status == property_statust::NOT_CHECKED ||
178  status == property_statust::UNKNOWN;
179 }
180 
181 bool has_properties_to_check(const propertiest &properties)
182 {
183  for(const auto &property_pair : properties)
184  {
185  if(is_property_to_check(property_pair.second.status))
186  return true;
187  }
188  return false;
189 }
190 
198 {
199  // non-monotonic use is likely a bug
200  // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL
201  // clang-format off
202  PRECONDITION(
206  a == b);
207  // clang-format on
208  switch(a)
209  {
212  a = b;
213  return a;
218  return a;
219  }
220  UNREACHABLE;
221 }
222 
232 {
233  switch(a)
234  {
236  return a;
238  a = (b == property_statust::ERROR ? b : a);
239  return a;
241  a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
242  return a;
244  a =
246  : a);
247  return a;
249  a = (b != property_statust::PASS ? b : a);
250  return a;
252  a = (b == property_statust::PASS ? a : b);
253  return a;
254  }
255  UNREACHABLE;
256 }
257 
265 {
267  for(const auto &property_pair : properties)
268  {
269  status &= property_pair.second.status;
270  }
271  switch(status)
272  {
274  // If we have unchecked properties then we don't know.
275  return resultt::UNKNOWN;
277  return resultt::UNKNOWN;
279  // If a property is not reachable then overall it's still a PASS.
280  return resultt::PASS;
282  return resultt::PASS;
284  return resultt::FAIL;
286  return resultt::ERROR;
287  }
288  UNREACHABLE;
289 }
Abstract interface to eager or lazy GOTO models.
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:615
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
Definition: xml.h:21
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
xmlt & new_element(const std::string &key)
Definition: xml.h:95
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
Definition: exit_codes.h:21
#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE
Verification inconclusive indicates the analysis has been performed without error AND the software is...
Definition: exit_codes.h:30
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
Definition: exit_codes.h:25
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:197
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:181
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:175
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:264
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
Definition: properties.cpp:77
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:164
int result_to_exit_code(resultt result)
Definition: properties.cpp:147
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
std::string as_string(resultt result)
Definition: properties.cpp:24
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Definition: properties.cpp:70
property_statust & operator&=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:231
Properties.
property_statust
The status of a property.
Definition: properties.h:26
@ 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.
@ ERROR
An error occurred during goto checking.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
resultt
The result of goto verifying.
Definition: properties.h:45
@ UNKNOWN
No property was violated, neither was there an error.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
Some properties were violated.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
property_statust status
The status of the property.
Definition: properties.h:72
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:69
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)
Definition: properties.cpp:62
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:66