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 =
91  id2string(i_it->source_location().get_comment());
92  if(description.empty())
93  description = "assertion";
94  properties.emplace(
95  i_it->source_location().get_property_id(),
96  property_infot{i_it, description, property_statust::NOT_CHECKED});
97  }
98  }
99 }
100 
101 std::string
102 as_string(const irep_idt &property_id, const property_infot &property_info)
103 {
104  return "[" + id2string(property_id) + "] " + property_info.description +
105  ": " + as_string(property_info.status);
106 }
107 
108 xmlt xml(const irep_idt &property_id, const property_infot &property_info)
109 {
110  xmlt xml_result("result");
111  xml_result.set_attribute("property", id2string(property_id));
112  xml_result.set_attribute("status", as_string(property_info.status));
113  return xml_result;
114 }
115 
116 template <class json_objectT>
117 static void json(
118  json_objectT &result,
119  const irep_idt &property_id,
120  const property_infot &property_info)
121 {
122  result["property"] = json_stringt(property_id);
123  result["description"] = json_stringt(property_info.description);
124  result["status"] = json_stringt(as_string(property_info.status));
125 }
126 
128 json(const irep_idt &property_id, const property_infot &property_info)
129 {
130  json_objectt result;
131  json<json_objectt>(result, property_id, property_info);
132  return result;
133 }
134 
135 void json(
136  json_stream_objectt &result,
137  const irep_idt &property_id,
138  const property_infot &property_info)
139 {
140  json<json_stream_objectt>(result, property_id, property_info);
141 }
142 
144 {
145  switch(result)
146  {
147  case resultt::PASS:
149  case resultt::FAIL:
151  case resultt::ERROR:
153  case resultt::UNKNOWN:
155  }
156  UNREACHABLE;
157 }
158 
159 std::size_t
161 {
162  std::size_t count = 0;
163  for(const auto &property_pair : properties)
164  {
165  if(property_pair.second.status == status)
166  ++count;
167  }
168  return count;
169 }
170 
172 {
173  return status == property_statust::NOT_CHECKED ||
174  status == property_statust::UNKNOWN;
175 }
176 
177 bool has_properties_to_check(const propertiest &properties)
178 {
179  for(const auto &property_pair : properties)
180  {
181  if(is_property_to_check(property_pair.second.status))
182  return true;
183  }
184  return false;
185 }
186 
194 {
195  // non-monotonic use is likely a bug
196  // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL
197  // clang-format off
198  PRECONDITION(
202  a == b);
203  // clang-format on
204  switch(a)
205  {
208  a = b;
209  return a;
214  return a;
215  }
216  UNREACHABLE;
217 }
218 
228 {
229  switch(a)
230  {
232  return a;
234  a = (b == property_statust::ERROR ? b : a);
235  return a;
237  a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
238  return a;
240  a =
242  : a);
243  return a;
245  a = (b != property_statust::PASS ? b : a);
246  return a;
248  a = (b == property_statust::PASS ? a : b);
249  return a;
250  }
251  UNREACHABLE;
252 }
253 
261 {
263  for(const auto &property_pair : properties)
264  {
265  status &= property_pair.second.status;
266  }
267  switch(status)
268  {
270  // If we have unchecked properties then we don't know.
271  return resultt::UNKNOWN;
273  return resultt::UNKNOWN;
275  // If a property is not reachable then overall it's still a PASS.
276  return resultt::PASS;
278  return resultt::PASS;
280  return resultt::FAIL;
282  return resultt::ERROR;
283  }
284  UNREACHABLE;
285 }
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:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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:47
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:193
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:177
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:171
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:260
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:160
int result_to_exit_code(resultt result)
Definition: properties.cpp:143
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
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:227
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: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