cprover
Loading...
Searching...
No Matches
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
25template <class smtt>
29
30template <class smtt>
32 : messages{std::move(message)}
33{
34}
35
36template <class smtt>
37response_or_errort<smtt>::response_or_errort(std::vector<std::string> messages)
38 : messages{std::move(messages)}
39{
40}
41
42template <class smtt>
44{
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
52template <class smtt>
53const std::vector<std::string> *response_or_errort<smtt>::get_if_error() const
54{
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.
65template <typename argumentt, typename... argumentst>
67 std::vector<std::string> &collected_messages,
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.
78template <typename argumentt, typename... argumentst>
80 std::vector<std::string> &collected_messages,
82 argumentst &&... arguments)
83{
86}
87
92template <typename... argumentst>
93std::vector<std::string> collect_messages(argumentst &&... arguments)
94{
95 std::vector<std::string> collected_messages;
97 return collected_messages;
98}
99
114template <
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())
123 else
124 {
126 smt_to_constructt{(*arguments.get_if_valid())...}};
127 }
128}
129
136static std::string print_parse_tree(const irept &parse_tree)
137{
138 return parse_tree.pretty(0, 0);
139}
140
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
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 }
182 validate_string_literal(parse_tree.get_sub()[1]));
183}
184
185static 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
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
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
215static 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
226static 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());
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))
257 if(const auto bit_vector_constant = valid_smt_bit_vector_constant(parse_tree))
259 return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
260 print_parse_tree(parse_tree) + "\"."};
261}
262
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];
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 {
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())
300 else
301 {
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
ait()
Definition ai.h:567
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
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
subt & get_sub()
Definition irep.h:456
const irep_idt & id() const
Definition irep.h:396
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
STL namespace.
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
static optionalt< smt_termt > valid_smt_binary(const std::string &text)
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 optionalt< smt_termt > valid_smt_bit_vector_constant(const irept &parse_tree)
static optionalt< response_or_errort< smt_responset > > valid_smt_error_response(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_hex(const std::string &text)
static bool all_subs_are_pairs(const irept &parse_tree)
static response_or_errort< smt_termt > validate_term(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 optionalt< smt_termt > valid_smt_bool(const irept &parse_tree)
static response_or_errort< irep_idt > validate_string_literal(const irept &parse_tree)
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...
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_get_value_response(const irept &parse_tree)
void collect_messages_impl(std::vector< std::string > &collected_messages, argumentt &&argument)
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423