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 <ansi-c/string_constant.h>
15 #include <util/prefix.h>
16 #include <util/unicode.h>
17 
23  const symbol_exprt &s)
24 {
25  std::string tmp=id2string(s.get_identifier());
26  std::string prefix("java::java.lang.String.Literal.");
27  assert(has_prefix(tmp, prefix));
28  std::string value=tmp.substr(prefix.length());
29  return irep_idt(value);
30 }
31 
37  irep_idt sval, const refined_string_typet &ref_type)
38 {
39  string_exprt res=fresh_string(ref_type);
40  std::string c_str=id2string(sval);
41  std::wstring str;
42 
43  // TODO: we should have a special treatment for java strings when the
44  // conversion function is available:
45 #if 0
46  if(mode==ID_java)
47  str=utf8_to_utf16_little_endian(c_str);
48  else
49 #endif
50  str=widen(c_str);
51 
52  for(std::size_t i=0; i<str.size(); i++)
53  {
54  exprt idx=from_integer(i, ref_type.get_index_type());
55  exprt c=from_integer(str[i], ref_type.get_char_type());
56  equal_exprt lemma(res[idx], c);
57  axioms.push_back(lemma);
58  }
59 
60  exprt s_length=from_integer(str.size(), ref_type.get_index_type());
61 
62  axioms.push_back(res.axiom_for_has_length(s_length));
63  return res;
64 }
65 
71 {
72  assert(f.arguments().empty());
74  string_exprt res=fresh_string(ref_type);
75  axioms.push_back(res.axiom_for_has_length(0));
76  return res;
77 }
78 
86 {
88  assert(args.size()==1); // Bad args to string literal?
89 
90  const exprt &arg=args[0];
91  irep_idt sval;
92 
93  assert(arg.operands().size()==1);
94  if(arg.op0().operands().size()==2 &&
95  arg.op0().op0().id()==ID_string_constant)
96  {
97  // C string constant
98  const exprt &s=arg.op0().op0();
99  sval=to_string_constant(s).get_value();
100  }
101  else
102  {
103  // Java string constant
105  const exprt &s=arg.op0();
106 
107  // It seems the value of the string is lost,
108  // we need to recover it from the identifier
110  }
111 
112  const refined_string_typet &ref_type=to_refined_string_type(f.type());
113  return add_axioms_for_constant(sval, ref_type);
114 }
string_exprt add_axioms_from_literal(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the string literal ...
Generates string constraints to link results from string functions with their arguments.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
application of (mathematical) function
Definition: std_expr.h:3785
std::wstring widen(const char *s)
Definition: unicode.cpp:56
exprt & op0()
Definition: expr.h:84
const typet & get_char_type() const
const irep_idt & get_identifier() const
Definition: std_expr.h:120
argumentst & arguments()
Definition: std_expr.h:3805
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:120
typet & type()
Definition: expr.h:60
string_exprt add_axioms_for_empty_string(const function_application_exprt &f)
add axioms to say that the returned string expression is empty
equality
Definition: std_expr.h:1082
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
static bool is_unrefined_string_type(const typet &type)
exprt::operandst argumentst
Definition: std_expr.h:3803
const refined_string_typet & to_refined_string_type(const typet &type)
const typet & get_index_type() const
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
std::wstring utf8_to_utf16_little_endian(const std::string &in)
Definition: unicode.cpp:283
string_exprt add_axioms_for_constant(irep_idt sval, const refined_string_typet &ref_type)
add axioms saying the returned string expression should be equal to the string constant ...
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
Expression to hold a symbol (variable)
Definition: std_expr.h:82
dstringt irep_idt
Definition: irep.h:32
const irep_idt & get_value() const
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
static irep_idt extract_java_string(const symbol_exprt &s)
extract java string from symbol expression when they are encoded inside the symbol name ...