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 
25  const array_string_exprt &res,
26  irep_idt sval,
27  const exprt &guard)
28 {
29  const typet &index_type = res.length().type();
30  const typet &char_type = res.content().type().subtype();
31  std::string c_str=id2string(sval);
32  std::wstring str;
33 
36 #if 0
37  if(mode==ID_java)
38  str=utf8_to_utf16_little_endian(c_str);
39  else
40 #endif
41  str=widen(c_str);
42 
43  for(std::size_t i=0; i<str.size(); i++)
44  {
45  const exprt idx = from_integer(i, index_type);
46  const exprt c = from_integer(str[i], char_type);
47  const equal_exprt lemma(res[idx], c);
48  lemmas.push_back(implies_exprt(guard, lemma));
49  }
50 
51  const exprt s_length = from_integer(str.size(), index_type);
52 
53  lemmas.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
55 }
56 
63 {
64  PRECONDITION(f.arguments().size() == 2);
65  exprt length = f.arguments()[0];
66  lemmas.push_back(equal_exprt(length, from_integer(0, length.type())));
68 }
69 
78  const array_string_exprt &res,
79  const exprt &arg,
80  const exprt &guard)
81 {
82  if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
83  {
84  const and_exprt guard_true(guard, if_expr->cond());
85  const exprt return_code_true =
86  add_axioms_for_cprover_string(res, if_expr->true_case(), guard_true);
87 
88  const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
89  const exprt return_code_false =
90  add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false);
91 
92  return if_exprt(
93  equal_exprt(return_code_true, from_integer(0, get_return_code_type())),
94  return_code_false,
95  return_code_true);
96  }
97  else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
98  return add_axioms_for_constant(res, constant_expr->get_value(), guard);
99  else
100  return from_integer(1, get_return_code_type());
101 }
102 
113 {
115  PRECONDITION(args.size() == 3); // Bad args to string literal?
116  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
117  return add_axioms_for_cprover_string(res, args[2], true_exprt());
118 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3230
Generates string constraints to link results from string functions with their arguments.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
application of (mathematical) function
Definition: std_expr.h:4531
exprt add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
std::wstring widen(const char *s)
Definition: unicode.cpp:56
exprt add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
argumentst & arguments()
Definition: std_expr.h:4564
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
The boolean constant true.
Definition: std_expr.h:4488
exprt add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
exprt::operandst argumentst
Definition: std_expr.h:4562
boolean AND
Definition: std_expr.h:2255
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
bitvector_typet index_type()
Definition: c_types.cpp:16
std::wstring utf8_to_utf16_little_endian(const std::string &in)
Definition: unicode.cpp:281
Base class for all expressions.
Definition: expr.h:42
exprt add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
Definition: type.h:33
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114