Skip to content

Improve cprover_string_literal argument handling TG-1245 #1691

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jan 12, 2018
Merged

Improve cprover_string_literal argument handling TG-1245 #1691

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
c6c1b3f
Add an optional guard to add_axioms_for_constant
romainbrenguier Jan 2, 2018
74144fc
Handle if_exprt in add_axioms_for_string_literal
romainbrenguier Jan 2, 2018
4699c13
Extend symbol resolution to string_typet
romainbrenguier Jan 8, 2018
3dd3877
Refactor has_char_pointer_subtype with has_subtype
romainbrenguier Jan 8, 2018
954060e
Add unit test for has_subtype
romainbrenguier Jan 8, 2018
ae4deff
Debug information for string equations
romainbrenguier Jan 11, 2018
c13e602
Adding only needed equations in symbol resolution
romainbrenguier Jan 10, 2018
23c3561
Unit test for string symbol resolution
romainbrenguier Jan 11, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion src/solvers/refinement/string_constraint_generator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,11 @@ class string_constraint_generatort final
const exprt &end_index);
exprt add_axioms_for_concat(const function_application_exprt &f);
exprt add_axioms_for_concat_code_point(const function_application_exprt &f);
exprt add_axioms_for_constant(const array_string_exprt &res, irep_idt sval);
exprt add_axioms_for_constant(
const array_string_exprt &res,
irep_idt sval,
const exprt &guard = true_exprt());

exprt add_axioms_for_delete(
const array_string_exprt &res,
const array_string_exprt &str,
Expand Down Expand Up @@ -195,6 +199,11 @@ class string_constraint_generatort final
exprt add_axioms_for_insert_char(const function_application_exprt &f);
exprt add_axioms_for_insert_float(const function_application_exprt &f);
exprt add_axioms_for_insert_double(const function_application_exprt &f);

exprt add_axioms_for_cprover_string(
const array_string_exprt &res,
const exprt &arg,
const exprt &guard);
exprt add_axioms_from_literal(const function_application_exprt &f);
exprt add_axioms_from_int(const function_application_exprt &f);
exprt add_axioms_from_int(
Expand Down
45 changes: 39 additions & 6 deletions src/solvers/refinement/string_constraint_generator_constants.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,12 @@ Author: Romain Brenguier, [email protected]
/// equal.
/// \param res: array of characters for the result
/// \param sval: a string constant
/// \param guard: condition under which the axiom should apply, true by default
/// \return integer expression equal to zero
exprt string_constraint_generatort::add_axioms_for_constant(
const array_string_exprt &res,
irep_idt sval)
irep_idt sval,
const exprt &guard)
{
const typet &index_type = res.length().type();
const typet &char_type = res.content().type().subtype();
Expand All @@ -43,12 +45,12 @@ exprt string_constraint_generatort::add_axioms_for_constant(
const exprt idx = from_integer(i, index_type);
const exprt c = from_integer(str[i], char_type);
const equal_exprt lemma(res[idx], c);
axioms.push_back(lemma);
axioms.push_back(implies_exprt(guard, lemma));
}

const exprt s_length = from_integer(str.size(), index_type);

axioms.push_back(res.axiom_for_has_length(s_length));
axioms.push_back(implies_exprt(guard, equal_exprt(res.length(), s_length)));
return from_integer(0, get_return_code_type());
}

Expand All @@ -65,6 +67,39 @@ exprt string_constraint_generatort::add_axioms_for_empty_string(
return from_integer(0, get_return_code_type());
}

/// Convert an expression of type string_typet to a string_exprt
/// \param res: string expression for the result
/// \param arg: expression of type string typet
/// \param guard: condition under which `res` should be equal to arg
/// \return 0 if constraints were added, 1 if expression could not be handled
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what is with the return value of if_exprt ? This reads as if only 1 or 0 can be returned.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, in case of if_expr we return the maximum of the true case or false case, so it will always be 0 or 1

/// and no constraint was added. Expression we can handle are of the
/// form \f$ e := "<string constant>" | (expr)? e : e \f$
exprt string_constraint_generatort::add_axioms_for_cprover_string(
const array_string_exprt &res,
const exprt &arg,
const exprt &guard)
{
if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(arg))
{
const and_exprt guard_true(guard, if_expr->cond());
const exprt return_code_true =
add_axioms_for_cprover_string(res, if_expr->true_case(), guard_true);

const and_exprt guard_false(guard, not_exprt(if_expr->cond()));
const exprt return_code_false =
add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false);

return if_exprt(
equal_exprt(return_code_true, from_integer(0, get_return_code_type())),
return_code_false,
return_code_true);
}
else if(const auto constant_expr = expr_try_dynamic_cast<constant_exprt>(arg))
return add_axioms_for_constant(res, constant_expr->get_value(), guard);
else
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A comment explaining why in this case a 1 expression is a reasonable return might be good.

return from_integer(1, get_return_code_type());
}

/// String corresponding to an internal cprover string
///
/// Add axioms ensuring that the returned string expression is equal to the
Expand All @@ -79,7 +114,5 @@ exprt string_constraint_generatort::add_axioms_from_literal(
const function_application_exprt::argumentst &args=f.arguments();
PRECONDITION(args.size() == 3); // Bad args to string literal?
const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
const exprt &arg = args[2];
irep_idt sval=to_constant_expr(arg).get_value();
return add_axioms_for_constant(res, sval);
return add_axioms_for_cprover_string(res, args[2], true_exprt());
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be good to see a test for whatever case is now supported. I can't say the changes in this file mean much to me

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There will be tests in other repositories: https://github.com/diffblue/test-gen/pull/1327
But it is difficule to test on CBMC because we don't have a model for Class and the main affected method is Object.getClass.

An example that should work afterwards is the following:

public class testMaybeNull1
{
    public Object x;
    public String check()
    {
        return x.getClass().getName();
    }
}

The reason is that getClass converts a cprover_string to a java string (the @class_identifier), but since the object could be null, the argument passed to cprover_string_literal is more complicated than a constant.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would it not be sufficent to have a:

public class simpleClaz {
  String getStr() { return "hello"; }
}
/////////////
public class testMaybeNull1
{
    public simpleClaz x;
    public String check()
    {
        return x.getStr();
    }
}

Since x may or may not be null isn't it the same?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No this example is already handled correctly. It is the @class_identifier field that is a problem, and as far as I now it can only be access via instanceof and getClass. And I think getClass is the only function which generate a cprover_string_literal with something else than a constant.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But it is difficule to test on CBMC because we don't have a model for Class and the main affected method is Object.getClass.

Getting 'java core models' into the cbmc repo would help. @cesaro has started some work on that.

}
Loading