cprover
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_stream.h>
18 #include <util/xml.h>
19 
21 
22 std::string as_string(resultt result)
23 {
24  switch(result)
25  {
26  case resultt::UNKNOWN:
27  return "UNKNOWN";
28  case resultt::PASS:
29  return "PASS";
30  case resultt::FAIL:
31  return "FAIL";
32  case resultt::ERROR:
33  return "ERROR";
34  }
35 
37 }
38 
39 std::string as_string(property_statust status)
40 {
41  switch(status)
42  {
44  return "NOT CHECKED";
46  return "UNKNOWN";
48  return "UNREACHABLE";
50  return "SUCCESS";
52  return "FAILURE";
54  return "ERROR";
55  }
56 
58 }
59 
62  std::string description,
63  property_statust status)
64  : pc(pc), description(std::move(description)), status(status)
65 {
66 }
67 
69 {
70  propertiest properties;
71  update_properties_from_goto_model(properties, goto_model);
72  return properties;
73 }
74 
76  propertiest &properties,
77  const abstract_goto_modelt &goto_model)
78 {
79  const auto &goto_functions = goto_model.get_goto_functions();
80  for(const auto &function_pair : goto_functions.function_map)
81  {
82  const goto_programt &goto_program = function_pair.second.body;
83 
84  // need pointer to goto instruction
85  forall_goto_program_instructions(i_it, goto_program)
86  {
87  if(!i_it->is_assert())
88  continue;
89 
90  std::string description = id2string(i_it->source_location.get_comment());
91  if(description.empty())
92  description = "assertion";
93  properties.emplace(
94  i_it->source_location.get_property_id(),
95  property_infot{i_it, description, property_statust::NOT_CHECKED});
96  }
97  }
98 }
99 
100 std::string
101 as_string(const irep_idt &property_id, const property_infot &property_info)
102 {
103  return "[" + id2string(property_id) + "] " + property_info.description +
104  ": " + as_string(property_info.status);
105 }
106 
107 xmlt xml(const irep_idt &property_id, const property_infot &property_info)
108 {
109  xmlt xml_result("result");
110  xml_result.set_attribute("property", id2string(property_id));
111  xml_result.set_attribute("status", as_string(property_info.status));
112  return xml_result;
113 }
114 
115 template <class json_objectT>
116 static void json(
117  json_objectT &result,
118  const irep_idt &property_id,
119  const property_infot &property_info)
120 {
121  result["property"] = json_stringt(property_id);
122  result["description"] = json_stringt(property_info.description);
123  result["status"] = json_stringt(as_string(property_info.status));
124 }
125 
127 json(const irep_idt &property_id, const property_infot &property_info)
128 {
129  json_objectt result;
130  json<json_objectt>(result, property_id, property_info);
131  return result;
132 }
133 
134 void json(
135  json_stream_objectt &result,
136  const irep_idt &property_id,
137  const property_infot &property_info)
138 {
139  json<json_stream_objectt>(result, property_id, property_info);
140 }
141 
143 {
144  switch(result)
145  {
146  case resultt::PASS:
148  case resultt::FAIL:
150  case resultt::ERROR:
152  case resultt::UNKNOWN:
154  }
155  UNREACHABLE;
156 }
157 
158 std::size_t
160 {
161  std::size_t count = 0;
162  for(const auto &property_pair : properties)
163  {
164  if(property_pair.second.status == status)
165  ++count;
166  }
167  return count;
168 }
169 
171 {
172  return status == property_statust::NOT_CHECKED ||
173  status == property_statust::UNKNOWN;
174 }
175 
176 bool has_properties_to_check(const propertiest &properties)
177 {
178  for(const auto &property_pair : properties)
179  {
180  if(is_property_to_check(property_pair.second.status))
181  return true;
182  }
183  return false;
184 }
185 
193 {
194  // non-monotonic use is likely a bug
195  // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL
196  // clang-format off
197  PRECONDITION(
201  a == b);
202  // clang-format on
203  switch(a)
204  {
207  a = b;
208  return a;
213  return a;
214  }
215  UNREACHABLE;
216 }
217 
227 {
228  switch(a)
229  {
231  return a;
233  a = (b == property_statust::ERROR ? b : a);
234  return a;
236  a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
237  return a;
239  a =
241  : a);
242  return a;
244  a = (b != property_statust::PASS ? b : a);
245  return a;
247  a = (b == property_statust::PASS ? a : b);
248  return a;
249  }
250  UNREACHABLE;
251 }
252 
260 {
262  for(const auto &property_pair : properties)
263  {
264  status &= property_pair.second.status;
265  }
266  switch(status)
267  {
269  // If we have unchecked properties then we don't know.
270  return resultt::UNKNOWN;
272  return resultt::UNKNOWN;
274  // If a property is not reachable then overall it's still a PASS.
275  return resultt::PASS;
277  return resultt::PASS;
279  return resultt::FAIL;
281  return resultt::ERROR;
282  }
283  UNREACHABLE;
284 }
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:37
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst::const_iterator const_targett
Definition: goto_program.h:647
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
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:49
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:192
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:176
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:170
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:259
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:75
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:159
int result_to_exit_code(resultt result)
Definition: properties.cpp:142
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:107
std::string as_string(resultt result)
Definition: properties.cpp:22
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Definition: properties.cpp:68
property_statust & operator&=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:226
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)
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.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#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:60