cprover
string_constraint_generator_valueof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions generating strings
4  from other types, in particular int, long, float, double, char, bool
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
17 
22  const function_application_exprt &expr)
23 {
24  const refined_string_typet &ref_type=to_refined_string_type(expr.type());
25  return add_axioms_from_int(args(expr, 1)[0], MAX_INTEGER_LENGTH, ref_type);
26 }
27 
32  const function_application_exprt &expr)
33 {
34  const refined_string_typet &ref_type=to_refined_string_type(expr.type());
35  return add_axioms_from_int(args(expr, 1)[0], MAX_LONG_LENGTH, ref_type);
36 }
37 
43 {
44  return add_axioms_from_float(args(f, 1)[0], false);
45 }
46 
52 {
53  return add_axioms_from_float(args(f, 1)[0], true);
54 }
55 
63  const exprt &f, bool double_precision)
64 {
66  const typet &index_type=ref_type.get_index_type();
67  const typet &char_type=ref_type.get_char_type();
68  string_exprt res=fresh_string(ref_type);
69  const exprt &index24=from_integer(24, ref_type.get_index_type());
70  axioms.push_back(res.axiom_for_is_shorter_than(index24));
71 
72  string_exprt magnitude=fresh_string(ref_type);
73  string_exprt sign_string=fresh_string(ref_type);
74  string_exprt nan_string=add_axioms_for_constant("NaN", ref_type);
75 
76  // We add the axioms:
77  // a1 : If the argument is NaN, the result length is that of "NaN".
78  // a2 : If the argument is NaN, the result content is the string "NaN".
79  // a3 : f<0 => |sign_string|=1
80  // a4 : f>=0 => |sign_string|=0
81  // a5 : f<0 => sign_string[0]='-'
82  // a6 : f infinite => |magnitude|=|"Infinity"|
83  // a7 : forall i<|"Infinity"|, f infinite => magnitude[i]="Infinity"[i]
84  // a8 : f=0 => |magnitude|=|"0.0"|
85  // a9 : forall i<|"0.0"|, f=0 => f[i]="0.0"[i]
86 
87  ieee_float_spect fspec=
88  double_precision?ieee_float_spect::double_precision()
90 
91  exprt isnan=float_bvt().isnan(f, fspec);
92  implies_exprt a1(isnan, magnitude.axiom_for_has_same_length_as(nan_string));
93  axioms.push_back(a1);
94 
95  symbol_exprt qvar=fresh_univ_index("QA_equal_nan", index_type);
97  qvar,
98  nan_string.length(),
99  isnan,
100  equal_exprt(magnitude[qvar], nan_string[qvar]));
101  axioms.push_back(a2);
102 
103  // If the argument is not NaN, the result is a string that represents
104  // the sign and magnitude (absolute value) of the argument.
105  // If the sign is negative, the first character of the result is '-';
106  // if the sign is positive, no sign character appears in the result.
107 
109  unsigned width=bv_type.get_width();
110  exprt isneg=extractbit_exprt(f, width-1);
111 
112  implies_exprt a3(isneg, sign_string.axiom_for_has_length(1));
113  axioms.push_back(a3);
114 
115  implies_exprt a4(not_exprt(isneg), sign_string.axiom_for_has_length(0));
116  axioms.push_back(a4);
117 
118  implies_exprt a5(
119  isneg, equal_exprt(sign_string[0], constant_char('-', char_type)));
120  axioms.push_back(a5);
121 
122  // If m is infinity, it is represented by the characters "Infinity";
123  // thus, positive infinity produces the result "Infinity" and negative
124  // infinity produces the result "-Infinity".
125 
126  string_exprt infinity_string=add_axioms_for_constant("Infinity", ref_type);
127  exprt isinf=float_bvt().isinf(f, fspec);
128  implies_exprt a6(
129  isinf, magnitude.axiom_for_has_same_length_as(infinity_string));
130  axioms.push_back(a6);
131 
132  symbol_exprt qvar_inf=fresh_univ_index("QA_equal_infinity", index_type);
133  equal_exprt meq(magnitude[qvar_inf], infinity_string[qvar_inf]);
134  string_constraintt a7(qvar_inf, infinity_string.length(), isinf, meq);
135  axioms.push_back(a7);
136 
137  // If m is zero, it is represented by the characters "0.0"; thus, negative
138  // zero produces the result "-0.0" and positive zero produces "0.0".
139 
140  string_exprt zero_string=add_axioms_for_constant("0.0", ref_type);
141  exprt iszero=float_bvt().is_zero(f, fspec);
142  implies_exprt a8(iszero, magnitude.axiom_for_has_same_length_as(zero_string));
143  axioms.push_back(a8);
144 
145  symbol_exprt qvar_zero=fresh_univ_index("QA_equal_zero", index_type);
146  equal_exprt eq_zero(magnitude[qvar_zero], zero_string[qvar_zero]);
147  string_constraintt a9(qvar_zero, zero_string.length(), iszero, eq_zero);
148  axioms.push_back(a9);
149 
150  return add_axioms_for_concat(sign_string, magnitude);
151 }
152 
153 
159 {
160  const refined_string_typet &ref_type=to_refined_string_type(f.type());
161  return add_axioms_from_bool(args(f, 1)[0], ref_type);
162 }
163 
164 
170  const exprt &b, const refined_string_typet &ref_type)
171 {
172  string_exprt res=fresh_string(ref_type);
173  const typet &index_type=ref_type.get_index_type();
174 
175  assert(b.type()==bool_typet() || b.type().id()==ID_c_bool);
176 
177  typecast_exprt eq(b, bool_typet());
178 
179  string_exprt true_string=add_axioms_for_constant("true", ref_type);
180  string_exprt false_string=add_axioms_for_constant("false", ref_type);
181 
182  // We add axioms:
183  // a1 : eq => res = |"true"|
184  // a2 : forall i < |"true"|. eq => res[i]="true"[i]
185  // a3 : !eq => res = |"false"|
186  // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
187 
188  implies_exprt a1(eq, res.axiom_for_has_same_length_as(true_string));
189  axioms.push_back(a1);
190  symbol_exprt qvar=fresh_univ_index("QA_equal_true", index_type);
192  qvar,
193  true_string.length(),
194  eq,
195  equal_exprt(res[qvar], true_string[qvar]));
196  axioms.push_back(a2);
197 
198  implies_exprt a3(
199  not_exprt(eq), res.axiom_for_has_same_length_as(false_string));
200  axioms.push_back(a3);
201 
202  symbol_exprt qvar1=fresh_univ_index("QA_equal_false", index_type);
204  qvar,
205  false_string.length(),
206  not_exprt(eq),
207  equal_exprt(res[qvar1], false_string[qvar1]));
208  axioms.push_back(a4);
209 
210  return res;
211 }
212 
217 {
218  return power(10, nb-1);
219 }
220 
228  const exprt &i, size_t max_size, const refined_string_typet &ref_type)
229 {
230  string_exprt res=fresh_string(ref_type);
231  const typet &type=i.type();
232  assert(type.id()==ID_signedbv);
233  exprt ten=from_integer(10, type);
234  const typet &char_type=ref_type.get_char_type();
235  const typet &index_type=ref_type.get_index_type();
236  exprt zero_char=constant_char('0', char_type);
237  exprt nine_char=constant_char('9', char_type);
238  exprt minus_char=constant_char('-', char_type);
239  exprt zero=from_integer(0, index_type);
240  exprt max=from_integer(max_size, index_type);
241 
242  // We add axioms:
243  // a1 : 0 <|res|<=max_size
244  // a2 : (res[0]='-')||('0'<=res[0]<='9')
245 
247  res.axiom_for_is_shorter_than(max));
248  axioms.push_back(a1);
249 
250  exprt chr=res[0];
251  exprt starts_with_minus=equal_exprt(chr, minus_char);
252  exprt starts_with_digit=and_exprt(
253  binary_relation_exprt(chr, ID_ge, zero_char),
254  binary_relation_exprt(chr, ID_le, nine_char));
255  or_exprt a2(starts_with_digit, starts_with_minus);
256  axioms.push_back(a2);
257 
258  for(size_t size=1; size<=max_size; size++)
259  {
260  // For each possible size, we add axioms:
261  // all_numbers: forall 1<=i<=size. '0'<=res[i]<='9'
262  // a3 : |res|=size&&'0'<=res[0]<='9' =>
263  // i=sum+str[0]-'0' &&all_numbers
264  // a4 : |res|=size&&res[0]='-' => i=-sum
265  // a5 : size>1 => |res|=size&&'0'<=res[0]<='9' => res[0]!='0'
266  // a6 : size>1 => |res|=size&&res[0]'-' => res[1]!='0'
267  // a7 : size==max_size => i>1000000000
268  exprt sum=from_integer(0, type);
269  exprt all_numbers=true_exprt();
270  chr=res[0];
271  exprt first_value=typecast_exprt(minus_exprt(chr, zero_char), type);
272 
273  for(size_t j=1; j<size; j++)
274  {
275  chr=res[j];
276  sum=plus_exprt(
277  mult_exprt(sum, ten),
278  typecast_exprt(minus_exprt(chr, zero_char), type));
279  first_value=mult_exprt(first_value, ten);
281  binary_relation_exprt(chr, ID_ge, zero_char),
282  binary_relation_exprt(chr, ID_le, nine_char));
283  all_numbers=and_exprt(all_numbers, is_number);
284  }
285 
286  axioms.push_back(all_numbers);
287 
288  equal_exprt premise=res.axiom_for_has_length(size);
289  equal_exprt constr3(i, plus_exprt(sum, first_value));
290  implies_exprt a3(and_exprt(premise, starts_with_digit), constr3);
291  axioms.push_back(a3);
292 
293  implies_exprt a4(
294  and_exprt(premise, starts_with_minus),
295  equal_exprt(i, unary_minus_exprt(sum)));
296  axioms.push_back(a4);
297 
298  // disallow 0s at the beginning
299  if(size>1)
300  {
301  equal_exprt r0_zero(res[zero], zero_char);
302  implies_exprt a5(
303  and_exprt(premise, starts_with_digit),
304  not_exprt(r0_zero));
305  axioms.push_back(a5);
306 
307  exprt one=from_integer(1, index_type);
308  equal_exprt r1_zero(res[one], zero_char);
309  implies_exprt a6(
310  and_exprt(premise, starts_with_minus),
311  not_exprt(r1_zero));
312  axioms.push_back(a6);
313  }
314 
315  // we have to be careful when exceeding the maximal size of integers
316  if(size==max_size)
317  {
318  exprt smallest_with_10_digits=from_integer(
319  smallest_by_digit(max_size), type);
320  binary_relation_exprt big(i, ID_ge, smallest_with_10_digits);
321  implies_exprt a7(premise, big);
322  axioms.push_back(a7);
323  }
324  }
325  return res;
326 }
327 
333 {
334  exprt zero_char=constant_char('0', chr.type());
335  exprt nine_char=constant_char('9', chr.type());
336  exprt a_char=constant_char('a', chr.type());
337  return if_exprt(
338  binary_relation_exprt(chr, ID_gt, nine_char),
339  plus_exprt(constant_char(10, chr.type()), minus_exprt(chr, a_char)),
340  minus_exprt(chr, zero_char));
341 }
342 
348  const exprt &i, const refined_string_typet &ref_type)
349 {
350  string_exprt res=fresh_string(ref_type);
351  const typet &type=i.type();
352  assert(type.id()==ID_signedbv);
353  const typet &index_type=ref_type.get_index_type();
354  const typet &char_type=ref_type.get_char_type();
355  exprt sixteen=from_integer(16, index_type);
356  exprt minus_char=constant_char('-', char_type);
357  exprt zero_char=constant_char('0', char_type);
358  exprt nine_char=constant_char('9', char_type);
359  exprt a_char=constant_char('a', char_type);
360  exprt f_char=constant_char('f', char_type);
361 
362  size_t max_size=8;
363  axioms.push_back(
365  res.axiom_for_is_shorter_than(max_size)));
366 
367  for(size_t size=1; size<=max_size; size++)
368  {
369  exprt sum=from_integer(0, type);
370  exprt all_numbers=true_exprt();
371  exprt chr=res[0];
372 
373  for(size_t j=0; j<size; j++)
374  {
375  chr=res[j];
376  exprt i=int_of_hex_char(chr);
377  sum=plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(i, type));
379  and_exprt(
380  binary_relation_exprt(chr, ID_ge, zero_char),
381  binary_relation_exprt(chr, ID_le, nine_char)),
382  and_exprt(
383  binary_relation_exprt(chr, ID_ge, a_char),
384  binary_relation_exprt(chr, ID_le, f_char)));
385  all_numbers=and_exprt(all_numbers, is_number);
386  }
387 
388  equal_exprt premise(res.axiom_for_has_length(size));
389  axioms.push_back(
390  implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
391 
392  // disallow 0s at the beggining
393  if(size>1)
394  axioms.push_back(
395  implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
396  }
397  return res;
398 }
399 
405 {
406  const refined_string_typet &ref_type=to_refined_string_type(f.type());
407  return add_axioms_from_int_hex(args(f, 1)[0], ref_type);
408 }
409 
415 {
416  const refined_string_typet &ref_type=to_refined_string_type(f.type());
417  return add_axioms_from_char(args(f, 1)[0], ref_type);
418 }
419 
425  const exprt &c, const refined_string_typet &ref_type)
426 {
427  string_exprt res=fresh_string(ref_type);
428  and_exprt lemma(equal_exprt(res[0], c), res.axiom_for_has_length(1));
429  axioms.push_back(lemma);
430  return res;
431 }
432 
439 {
441  if(args.size()==3)
442  {
443  const refined_string_typet &ref_type=to_refined_string_type(f.type());
444  string_exprt res=fresh_string(ref_type);
445  exprt char_array=args[0];
446  exprt offset=args[1];
447  exprt count=args[2];
448 
449  // We add axioms:
450  // a1 : |res| = count
451  // a2 : forall idx<count, str[idx+offset]=res[idx]
452 
454  axioms.push_back(res.axiom_for_has_length(count));
455 
457  "QA_index_value_of", ref_type.get_index_type());
458  equal_exprt eq(str[plus_exprt(idx, offset)], res[idx]);
459  string_constraintt a2(idx, count, eq);
460  axioms.push_back(a2);
461  return res;
462  }
463  else
464  {
465  assert(args.size()==1);
467  }
468 }
469 
475 {
477  const typet &type=f.type();
478  symbol_exprt i=fresh_symbol("parsed_int", type);
479  const refined_string_typet &ref_type=to_refined_string_type(str.type());
480  const typet &char_type=ref_type.get_char_type();
481  exprt zero_char=constant_char('0', char_type);
482  exprt minus_char=constant_char('-', char_type);
483  exprt plus_char=constant_char('+', char_type);
484  assert(type.id()==ID_signedbv);
485  exprt ten=from_integer(10, type);
486 
487  exprt chr=str[0];
488  exprt starts_with_minus=equal_exprt(chr, minus_char);
489  exprt starts_with_plus=equal_exprt(chr, plus_char);
490  exprt starts_with_digit=binary_relation_exprt(chr, ID_ge, zero_char);
491 
492  for(unsigned size=1; size<=10; size++)
493  {
494  exprt sum=from_integer(0, type);
495  exprt first_value=typecast_exprt(minus_exprt(chr, zero_char), type);
496 
497  for(unsigned j=1; j<size; j++)
498  {
499  sum=plus_exprt(
500  mult_exprt(sum, ten),
501  typecast_exprt(minus_exprt(str[j], zero_char), type));
502  first_value=mult_exprt(first_value, ten);
503  }
504 
505  // If the length is `size`, we add axioms:
506  // a1 : starts_with_digit => i=sum+first_value
507  // a2 : starts_with_plus => i=sum
508  // a3 : starts_with_minus => i=-sum
509 
510  equal_exprt premise=str.axiom_for_has_length(size);
511  implies_exprt a1(
512  and_exprt(premise, starts_with_digit),
513  equal_exprt(i, plus_exprt(sum, first_value)));
514  axioms.push_back(a1);
515 
516  implies_exprt a2(and_exprt(premise, starts_with_plus), equal_exprt(i, sum));
517  axioms.push_back(a2);
518 
519  implies_exprt a3(
520  and_exprt(premise, starts_with_minus),
521  equal_exprt(i, unary_minus_exprt(sum)));
522  axioms.push_back(a3);
523  }
524  return i;
525 }
exprt isinf(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:836
The type of an expression.
Definition: type.h:20
Boolean negation.
Definition: std_expr.h:2648
semantic type conversion
Definition: std_expr.h:1725
BigInt mp_integer
Definition: mp_arith.h:19
string_exprt add_axioms_for_java_char_array(const exprt &char_array)
add axioms corresponding to the String.valueOf([C) java function
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
application of (mathematical) function
Definition: std_expr.h:3785
boolean OR
Definition: std_expr.h:1968
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
const typet & get_char_type() const
argumentst & arguments()
Definition: std_expr.h:3805
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:120
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
string_exprt add_axioms_from_double(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(D) java function
The trinary if-then-else operator.
Definition: std_expr.h:2771
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
Definition: string_expr.h:114
typet & type()
Definition: expr.h:60
string_exprt add_axioms_from_long(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(J) java function
The proper Booleans.
Definition: std_types.h:33
binary_relation_exprt axiom_for_is_shorter_than(const string_exprt &rhs) const
Definition: string_expr.h:85
boolean implication
Definition: std_expr.h:1926
static ieee_float_spect double_precision()
Definition: ieee_float.h:69
equality
Definition: std_expr.h:1082
static mp_integer smallest_by_digit(int nb)
gives the smallest integer with the specified number of digits
string_exprt fresh_string(const refined_string_typet &type)
construct a string expression whose length and content are new variables
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
const exprt & length() const
Definition: string_expr.h:35
string_exprt add_axioms_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
exprt::operandst argumentst
Definition: std_expr.h:3803
string_exprt add_axioms_for_value_of(const function_application_exprt &f)
add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) functions ...
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
exprt add_axioms_for_parse_int(const function_application_exprt &f)
add axioms corresponding to the Integer.parseInt java function
boolean AND
Definition: std_expr.h:1852
static ieee_float_spect single_precision()
Definition: ieee_float.h:63
The plus expression.
Definition: std_expr.h:702
const typet & get_index_type() const
bitvector_typet index_type()
Definition: c_types.cpp:15
The unary minus expression.
Definition: std_expr.h:346
Base class of bitvector types.
Definition: std_types.h:1003
std::size_t get_width() const
Definition: std_types.h:1030
binary multiplication
Definition: std_expr.h:806
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
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 ...
bool is_number(const typet &type)
Definition: type.cpp:24
exprt is_zero(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:148
Base class for all expressions.
Definition: expr.h:46
binary_relation_exprt axiom_for_is_strictly_longer_than(const exprt &rhs) const
Definition: string_expr.h:68
exprt int_of_hex_char(const exprt &chr) const
returns the value represented by the character
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
binary minus
Definition: std_expr.h:758
Expression to hold a symbol (variable)
Definition: std_expr.h:82
string_exprt add_axioms_from_int_hex(const exprt &i, const refined_string_typet &ref_type)
add axioms stating that the returned string corresponds to the integer argument written in hexadecima...
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)
bitvector_typet char_type()
Definition: c_types.cpp:113
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
exprt isnan(const exprt &, const ieee_float_spect &)
Definition: float_bv.cpp:872
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2434
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051