cprover
string_constraint_generator_constants.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for constant strings
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/prefix.h>
15 #include <util/string_constant.h>
16 #include <util/unicode.h>
17 
24 std::pair<exprt, string_constraintst> add_axioms_for_constant(
25  const array_string_exprt &res,
26  irep_idt sval,
27  const exprt &guard)
28 {
29  string_constraintst constraints;
30  const typet &index_type = res.length().type();
31  const typet &char_type = res.content().type().subtype();
32  std::string c_str=id2string(sval);
33  std::wstring str;
34 
37 #if 0
38  if(mode==ID_java)
39  str=utf8_to_utf16_little_endian(c_str);
40  else
41 #endif
42  str=widen(c_str);
43 
44  for(std::size_t i=0; i<str.size(); i++)
45  {
46  const exprt idx = from_integer(i, index_type);
47  const exprt c = from_integer(str[i], char_type);
48  const equal_exprt lemma(res[idx], c);
49  constraints.existential.push_back(implies_exprt(guard, lemma));
50  }
51 
52  const exprt s_length = from_integer(str.size(), index_type);
53 
54  constraints.existential.push_back(
55  implies_exprt(guard, equal_exprt(res.length(), s_length)));
56  return {from_integer(0, get_return_code_type()), std::move(constraints)};
57 }
58 
63 std::pair<exprt, string_constraintst> add_axioms_for_empty_string(
65 {
66  PRECONDITION(f.arguments().size() == 2);
67  string_constraintst constraints;
68  exprt length = f.arguments()[0];
69  constraints.existential.push_back(
70  equal_exprt(length, from_integer(0, length.type())));
71  return {from_integer(0, get_return_code_type()), std::move(constraints)};
72 }
73 
82 std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
83  symbol_generatort &fresh_symbol,
84  const array_string_exprt &res,
85  const exprt &arg,
86  const exprt &guard)
87 {
88  if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
89  {
90  const and_exprt guard_true(guard, if_expr->cond());
91  const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
92  return combine_results(
94  fresh_symbol, res, if_expr->true_case(), guard_true),
96  fresh_symbol, res, if_expr->false_case(), guard_false));
97  }
98  else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
99  return add_axioms_for_constant(res, constant_expr->get_value(), guard);
100  else
101  return {from_integer(1, get_return_code_type()), {}};
102 }
103 
114 std::pair<exprt, string_constraintst> add_axioms_from_literal(
115  symbol_generatort &fresh_symbol,
117  array_poolt &array_pool)
118 {
120  PRECONDITION(args.size() == 3); // Bad args to string literal?
121  const array_string_exprt res =
122  char_array_of_pointer(array_pool, args[1], args[0]);
124  fresh_symbol, res, args[2], true_exprt());
125 }
add_axioms_for_empty_string
std::pair< exprt, string_constraintst > add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
Definition: string_constraint_generator_constants.cpp:63
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
typet
The type of an expression, extends irept.
Definition: type.h:27
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
prefix.h
and_exprt
Boolean AND.
Definition: std_expr.h:2409
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
char_array_of_pointer
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Definition: string_constraint_generator_main.cpp:325
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
array_string_exprt::content
exprt & content()
Definition: string_expr.h:80
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: std_expr.h:4484
combine_results
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
Definition: string_constraint_generator_main.cpp:598
add_axioms_for_cprover_string
std::pair< exprt, string_constraintst > add_axioms_for_cprover_string(symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
Definition: string_constraint_generator_constants.cpp:82
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:339
add_axioms_for_constant
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard)
Add axioms ensuring that the provided string expression and constant are equal.
Definition: string_constraint_generator_constants.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
add_axioms_from_literal
std::pair< exprt, string_constraintst > add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
String corresponding to an internal cprover string.
Definition: string_constraint_generator_constants.cpp:114
unicode.h
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
string_constraint_generator.h
array_string_exprt
Definition: string_expr.h:67
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
not_exprt
Boolean negation.
Definition: std_expr.h:3308