cprover
smt_response_validation.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
17 
19 
20 #include <util/mp_arith.h>
21 #include <util/range.h>
22 
23 #include <regex>
24 
25 template <class smtt>
26 response_or_errort<smtt>::response_or_errort(smtt smt) : smt{std::move(smt)}
27 {
28 }
29 
30 template <class smtt>
32  : messages{std::move(message)}
33 {
34 }
35 
36 template <class smtt>
37 response_or_errort<smtt>::response_or_errort(std::vector<std::string> messages)
38  : messages{std::move(messages)}
39 {
40 }
41 
42 template <class smtt>
44 {
45  INVARIANT(
46  smt.has_value() == messages.empty(),
47  "The response_or_errort class must be in the valid state or error state, "
48  "exclusively.");
49  return smt.has_value() ? &smt.value() : nullptr;
50 }
51 
52 template <class smtt>
53 const std::vector<std::string> *response_or_errort<smtt>::get_if_error() const
54 {
55  INVARIANT(
56  smt.has_value() == messages.empty(),
57  "The response_or_errort class must be in the valid state or error state, "
58  "exclusively.");
59  return smt.has_value() ? nullptr : &messages;
60 }
61 
63 
64 // Implementation detail of `collect_messages` below.
65 template <typename argumentt, typename... argumentst>
67  std::vector<std::string> &collected_messages,
68  argumentt &&argument)
69 {
70  if(const auto messages = argument.get_if_error())
71  {
72  collected_messages.insert(
73  collected_messages.end(), messages->cbegin(), messages->end());
74  }
75 }
76 
77 // Implementation detail of `collect_messages` below.
78 template <typename argumentt, typename... argumentst>
80  std::vector<std::string> &collected_messages,
81  argumentt &&argument,
82  argumentst &&... arguments)
83 {
84  collect_messages_impl(collected_messages, argument);
85  collect_messages_impl(collected_messages, arguments...);
86 }
87 
92 template <typename... argumentst>
93 std::vector<std::string> collect_messages(argumentst &&... arguments)
94 {
95  std::vector<std::string> collected_messages;
96  collect_messages_impl(collected_messages, arguments...);
97  return collected_messages;
98 }
99 
114 template <
115  typename smt_to_constructt,
116  typename smt_baset = smt_to_constructt,
117  typename... argumentst>
119 {
120  const auto collected_messages = collect_messages(arguments...);
121  if(!collected_messages.empty())
122  return response_or_errort<smt_baset>(collected_messages);
123  else
124  {
126  smt_to_constructt{(*arguments.get_if_valid())...}};
127  }
128 }
129 
136 static std::string print_parse_tree(const irept &parse_tree)
137 {
138  return parse_tree.pretty(0, 0);
139 }
140 
142 validate_string_literal(const irept &parse_tree)
143 {
144  if(!parse_tree.get_sub().empty())
145  {
147  "Expected string literal, found \"" + print_parse_tree(parse_tree) +
148  "\".");
149  }
150  return response_or_errort<irep_idt>{parse_tree.id()};
151 }
152 
159 valid_smt_error_response(const irept &parse_tree)
160 {
161  // Check if the parse tree looks to be an error response.
162  if(!parse_tree.id().empty())
163  return {};
164  if(parse_tree.get_sub().empty())
165  return {};
166  if(parse_tree.get_sub().at(0).id() != "error")
167  return {};
168  // Parse tree is now considered to be an error response and anything
169  // unexpected in the parse tree is now considered to be an invalid response.
170  if(parse_tree.get_sub().size() == 1)
171  {
173  "Error response is missing the error message."}};
174  }
175  if(parse_tree.get_sub().size() > 2)
176  {
178  "Error response has multiple error messages - \"" +
179  print_parse_tree(parse_tree) + "\"."}};
180  }
181  return validation_propagating<smt_error_responset, smt_responset>(
182  validate_string_literal(parse_tree.get_sub()[1]));
183 }
184 
185 static bool all_subs_are_pairs(const irept &parse_tree)
186 {
187  return std::all_of(
188  parse_tree.get_sub().cbegin(),
189  parse_tree.get_sub().cend(),
190  [](const irept &sub) { return sub.get_sub().size() == 2; });
191 }
192 
194 validate_smt_identifier(const irept &parse_tree)
195 {
196  if(!parse_tree.get_sub().empty() || parse_tree.id().empty())
197  {
199  "Expected identifier, found - \"" + print_parse_tree(parse_tree) + "\".");
200  }
201  return response_or_errort<irep_idt>(parse_tree.id());
202 }
203 
204 static optionalt<smt_termt> valid_smt_bool(const irept &parse_tree)
205 {
206  if(!parse_tree.get_sub().empty())
207  return {};
208  if(parse_tree.id() == ID_true)
209  return {smt_bool_literal_termt{true}};
210  if(parse_tree.id() == ID_false)
211  return {smt_bool_literal_termt{false}};
212  return {};
213 }
214 
215 static optionalt<smt_termt> valid_smt_binary(const std::string &text)
216 {
217  static const std::regex binary_format{"#b[01]+"};
218  if(!std::regex_match(text, binary_format))
219  return {};
220  const mp_integer value = string2integer({text.begin() + 2, text.end()}, 2);
221  // Width is number of bit values minus the "#b" prefix.
222  const std::size_t width = text.size() - 2;
223  return {smt_bit_vector_constant_termt{value, width}};
224 }
225 
226 static optionalt<smt_termt> valid_smt_hex(const std::string &text)
227 {
228  static const std::regex hex_format{"#x[0-9A-Za-z]+"};
229  if(!std::regex_match(text, hex_format))
230  return {};
231  const std::string hex{text.begin() + 2, text.end()};
232  // SMT-LIB 2 allows hex characters to be upper of lower case, but they should
233  // be upper case for mp_integer.
234  const mp_integer value =
235  string2integer(make_range(hex).map<std::function<int(int)>>(toupper), 16);
236  const std::size_t width = (text.size() - 2) * 4;
237  return {smt_bit_vector_constant_termt{value, width}};
238 }
239 
242 {
243  if(!parse_tree.get_sub().empty() || parse_tree.id().empty())
244  return {};
245  const auto value_string = id2string(parse_tree.id());
246  if(const auto smt_binary = valid_smt_binary(value_string))
247  return *smt_binary;
248  if(const auto smt_hex = valid_smt_hex(value_string))
249  return *smt_hex;
250  return {};
251 }
252 
254 {
255  if(const auto smt_bool = valid_smt_bool(parse_tree))
256  return response_or_errort<smt_termt>{*smt_bool};
257  if(const auto bit_vector_constant = valid_smt_bit_vector_constant(parse_tree))
258  return response_or_errort<smt_termt>{*bit_vector_constant};
259  return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
260  print_parse_tree(parse_tree) + "\"."};
261 }
262 
264 validate_valuation_pair(const irept &pair_parse_tree)
265 {
266  PRECONDITION(pair_parse_tree.get_sub().size() == 2);
267  const auto &descriptor = pair_parse_tree.get_sub()[0];
268  const auto &value = pair_parse_tree.get_sub()[1];
269  return validation_propagating<smt_get_value_responset::valuation_pairt>(
270  validate_smt_identifier(descriptor), validate_term(value));
271 }
272 
280 {
281  // Shape matching for does this look like a get value response?
282  if(!parse_tree.id().empty())
283  return {};
284  if(parse_tree.get_sub().empty())
285  return {};
286  if(!all_subs_are_pairs(parse_tree))
287  return {};
288  std::vector<std::string> error_messages;
289  std::vector<smt_get_value_responset::valuation_pairt> valuation_pairs;
290  for(const auto &pair : parse_tree.get_sub())
291  {
292  const auto pair_validation_result = validate_valuation_pair(pair);
293  if(const auto error = pair_validation_result.get_if_error())
294  error_messages.insert(error_messages.end(), error->begin(), error->end());
295  if(const auto valid_pair = pair_validation_result.get_if_valid())
296  valuation_pairs.push_back(*valid_pair);
297  }
298  if(!error_messages.empty())
299  return {response_or_errort<smt_responset>{std::move(error_messages)}};
300  else
301  {
303  smt_get_value_responset{valuation_pairs}}};
304  }
305 }
306 
308 {
309  if(parse_tree.id() == "sat")
312  if(parse_tree.id() == "unsat")
315  if(parse_tree.id() == "unknown")
318  if(const auto error_response = valid_smt_error_response(parse_tree))
319  return *error_response;
320  if(parse_tree.id() == "success")
322  if(parse_tree.id() == "unsupported")
324  if(const auto get_value_response = valid_smt_get_value_response(parse_tree))
325  return *get_value_response;
326  return response_or_errort<smt_responset>{"Invalid SMT response \"" +
327  id2string(parse_tree.id()) + "\""};
328 }
bool empty() const
Definition: dstring.h:88
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
subt & get_sub()
Definition: irep.h:456
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
Holds either a valid parsed response or response sub-tree of type.
const std::vector< std::string > * get_if_error() const
Gets the error messages if the response is invalid, or returns nullptr otherwise.
const smtt * get_if_valid() const
Gets the smt response if the response is valid, or returns nullptr otherwise.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
std::vector< std::string > collect_messages(argumentst &&... arguments)
Builds a collection of messages composed all messages in the response_or_errort typed arguments in ar...
static std::string print_parse_tree(const irept &parse_tree)
Produces a human-readable representation of the given parse_tree, for use in error messaging.
static response_or_errort< smt_termt > validate_term(const irept &parse_tree)
response_or_errort< smt_baset > validation_propagating(argumentst &&... arguments)
Given a class to construct and a set of arguments to its constructor which may include errors,...
static optionalt< response_or_errort< smt_responset > > valid_smt_error_response(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_binary(const std::string &text)
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree)
static bool all_subs_are_pairs(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_bit_vector_constant(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_bool(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_hex(const std::string &text)
static optionalt< response_or_errort< smt_responset > > valid_smt_get_value_response(const irept &parse_tree)
static response_or_errort< smt_get_value_responset::valuation_pairt > validate_valuation_pair(const irept &pair_parse_tree)
static response_or_errort< irep_idt > validate_smt_identifier(const irept &parse_tree)
static response_or_errort< irep_idt > validate_string_literal(const irept &parse_tree)
void collect_messages_impl(std::vector< std::string > &collected_messages, argumentt &&argument)
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423