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 
20 std::string as_string(resultt result)
21 {
22  switch(result)
23  {
24  case resultt::UNKNOWN:
25  return "UNKNOWN";
26  case resultt::PASS:
27  return "PASS";
28  case resultt::FAIL:
29  return "FAIL";
30  case resultt::ERROR:
31  return "ERROR";
32  }
33 
35 }
36 
37 std::string as_string(property_statust status)
38 {
39  switch(status)
40  {
42  return "NOT CHECKED";
44  return "UNKNOWN";
46  return "UNREACHABLE";
48  return "SUCCESS";
50  return "FAILURE";
52  return "ERROR";
53  }
54 
56 }
57 
60  std::string description,
61  property_statust status)
62  : pc(pc), description(std::move(description)), status(status)
63 {
64 }
65 
67 {
68  propertiest properties;
69  update_properties_from_goto_model(properties, goto_model);
70  return properties;
71 }
72 
74  propertiest &properties,
75  const abstract_goto_modelt &goto_model)
76 {
77  const auto &goto_functions = goto_model.get_goto_functions();
78  for(const auto &function_pair : goto_functions.function_map)
79  {
80  const goto_programt &goto_program = function_pair.second.body;
81 
82  // need pointer to goto instruction
83  forall_goto_program_instructions(i_it, goto_program)
84  {
85  if(!i_it->is_assert())
86  continue;
87 
88  std::string description = id2string(i_it->source_location.get_comment());
89  if(description.empty())
90  description = "assertion";
91  properties.emplace(
92  i_it->source_location.get_property_id(),
93  property_infot{i_it, description, property_statust::NOT_CHECKED});
94  }
95  }
96 }
97 
98 std::string
99 as_string(const irep_idt &property_id, const property_infot &property_info)
100 {
101  return "[" + id2string(property_id) + "] " + property_info.description +
102  ": " + as_string(property_info.status);
103 }
104 
105 xmlt xml(const irep_idt &property_id, const property_infot &property_info)
106 {
107  xmlt xml_result("result");
108  xml_result.set_attribute("property", id2string(property_id));
109  xml_result.set_attribute("status", as_string(property_info.status));
110  return xml_result;
111 }
112 
113 template <class json_objectT>
114 static void json(
115  json_objectT &result,
116  const irep_idt &property_id,
117  const property_infot &property_info)
118 {
119  result["property"] = json_stringt(property_id);
120  result["description"] = json_stringt(property_info.description);
121  result["status"] = json_stringt(as_string(property_info.status));
122 }
123 
125 json(const irep_idt &property_id, const property_infot &property_info)
126 {
127  json_objectt result;
128  json<json_objectt>(result, property_id, property_info);
129  return result;
130 }
131 
132 void json(
133  json_stream_objectt &result,
134  const irep_idt &property_id,
135  const property_infot &property_info)
136 {
137  json<json_stream_objectt>(result, property_id, property_info);
138 }
139 
141 {
142  switch(result)
143  {
144  case resultt::PASS:
146  case resultt::FAIL:
148  case resultt::ERROR:
150  case resultt::UNKNOWN:
152  }
153  UNREACHABLE;
154 }
155 
156 std::size_t
158 {
159  std::size_t count = 0;
160  for(const auto &property_pair : properties)
161  {
162  if(property_pair.second.status == status)
163  ++count;
164  }
165  return count;
166 }
167 
169 {
170  return status == property_statust::NOT_CHECKED ||
171  status == property_statust::UNKNOWN;
172 }
173 
174 bool has_properties_to_check(const propertiest &properties)
175 {
176  for(const auto &property_pair : properties)
177  {
178  if(is_property_to_check(property_pair.second.status))
179  return true;
180  }
181  return false;
182 }
183 
191 {
192  // non-monotonic use is likely a bug
193  // UNKNOWN is neutral element w.r.t. ERROR/PASS/NOT_REACHABLE/FAIL
194  // clang-format off
195  PRECONDITION(
199  a == b);
200  // clang-format on
201  switch(a)
202  {
205  a = b;
206  return a;
211  return a;
212  }
213  UNREACHABLE;
214 }
215 
225 {
226  switch(a)
227  {
229  a = b;
230  return a;
232  a = (b == property_statust::ERROR ? b : a);
233  return a;
235  a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
236  return a;
238  a =
240  : a);
241  return a;
243  a = (b != property_statust::PASS ? b : a);
244  return a;
246  a = (b == property_statust::PASS ? a : b);
247  return a;
248  }
249  UNREACHABLE;
250 }
251 
259 {
261  for(const auto &property_pair : properties)
262  {
263  status &= property_pair.second.status;
264  }
265  switch(status)
266  {
268  // If we have unchecked properties then we don't know.
269  return resultt::UNKNOWN;
271  return resultt::UNKNOWN;
273  // If a property is not reachable then overall it's still a PASS.
274  return resultt::PASS;
276  return resultt::PASS;
278  return resultt::FAIL;
280  return resultt::ERROR;
281  }
282  UNREACHABLE;
283 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
property_statust::FAIL
@ FAIL
The property was violated.
property_statust
property_statust
The status of a property.
Definition: properties.h:25
CPROVER_EXIT_VERIFICATION_UNSAFE
#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
determine_result
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
Definition: properties.cpp:258
property_statust::ERROR
@ ERROR
An error occurred during goto checking.
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
json_stream.h
invariant.h
operator|=
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:190
CPROVER_EXIT_VERIFICATION_SAFE
#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
resultt::PASS
@ PASS
No properties were violated.
resultt::UNKNOWN
@ UNKNOWN
No property was violated, neither was there an error.
property_statust::NOT_REACHABLE
@ NOT_REACHABLE
The property was proven to be unreachable.
xml.h
update_properties_from_goto_model
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:73
property_infot::description
std::string description
A description (usually derived from the assertion's comment)
Definition: properties.h:68
resultt::FAIL
@ FAIL
Some properties were violated.
json_objectt
Definition: json.h:300
initialize_properties
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
Definition: properties.cpp:66
property_infot::status
property_statust status
The status of the property.
Definition: properties.h:71
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
has_properties_to_check
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:174
operator&=
property_statust & operator&=(property_statust &a, property_statust const &b)
Update with the preference order.
Definition: properties.cpp:224
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
is_property_to_check
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:168
property_statust::NOT_CHECKED
@ NOT_CHECKED
The property was not checked (also used for initialization)
count_properties
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:157
xmlt
Definition: xml.h:21
resultt::ERROR
@ ERROR
An error occurred during goto checking.
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
abstract_goto_modelt::get_goto_functions
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
property_infot
Definition: properties.h:58
result_to_exit_code
int result_to_exit_code(resultt result)
Definition: properties.cpp:140
CPROVER_EXIT_VERIFICATION_INCONCLUSIVE
#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE
Verification inconclusive indicates the analysis has been performed without error AND the software is...
Definition: exit_codes.h:30
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
as_string
std::string as_string(resultt result)
Definition: properties.cpp:20
json.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
property_statust::PASS
@ PASS
The property was not violated.
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
CPROVER_EXIT_INTERNAL_ERROR
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
properties.h
Properties.
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
property_infot::property_infot
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)
Definition: properties.cpp:58
json_stringt
Definition: json.h:270