Skip to content

Move expr_cast from refinement to util/convert_expr.h #1572

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 7 commits into from
Dec 8, 2017
Merged

Move expr_cast from refinement to util/convert_expr.h #1572

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
20b5366
Add validate and can_cast method to string_exprt
romainbrenguier Nov 9, 2017
946b6e2
Extend numeric_cast for constant expressions
romainbrenguier Nov 15, 2017
fc294f8
Use numeric_cast instead of refinement/expr_cast
romainbrenguier Nov 15, 2017
5683fb5
Use numeric_cast instead of other conversion
romainbrenguier Dec 1, 2017
898f965
Remove solvers/refinement/expr_cast.h
romainbrenguier Nov 8, 2017
77b7d77
Change length argument type to size_t
romainbrenguier Dec 7, 2017
9a811d8
Change type of size to std::size_t
romainbrenguier Dec 7, 2017
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
71 changes: 0 additions & 71 deletions src/solvers/refinement/expr_cast.h
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions src/solvers/refinement/string_constraint_generator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,7 +373,7 @@ exprt get_numeric_value_from_character(

size_t max_printed_string_length(const typet &type, unsigned long ul_radix);

std::string utf16_constant_array_to_java(
const array_exprt &arr, unsigned length);
std::string
utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);

#endif
4 changes: 2 additions & 2 deletions src/solvers/refinement/string_constraint_generator_format.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -417,8 +417,8 @@ exprt string_constraint_generatort::add_axioms_for_format(
/// \param length: an unsigned value representing the length of the array
/// \return String of length `length` represented by the array assuming each
/// field in `arr` represents a character.
std::string utf16_constant_array_to_java(
const array_exprt &arr, unsigned int length)
std::string
utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
{
std::wstring out(length, '?');
unsigned int c;
Expand Down
6 changes: 3 additions & 3 deletions src/solvers/refinement/string_constraint_generator_transformation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Author: Romain Brenguier, [email protected]

#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include "expr_cast.h"
#include <util/arith_tools.h>

/// Reduce or extend a string to have the given length
///
Expand Down Expand Up @@ -442,8 +442,8 @@ static optionalt<std::pair<exprt, exprt>> to_char_pair(
return std::make_pair(expr1, expr2);
const auto expr1_str = get_string_expr(expr1);
const auto expr2_str = get_string_expr(expr2);
const auto expr1_length=expr_cast<size_t>(expr1_str.length());
const auto expr2_length=expr_cast<size_t>(expr2_str.length());
const auto expr1_length = numeric_cast<std::size_t>(expr1_str.length());
const auto expr2_length = numeric_cast<std::size_t>(expr2_str.length());
if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
return { };
Expand Down
45 changes: 23 additions & 22 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,11 @@ Author: Alberto Griggio, [email protected]
#include <iomanip>
#include <stack>
#include <util/expr_iterator.h>
#include <util/optional.h>
#include <util/arith_tools.h>
#include <util/simplify_expr.h>
#include <solvers/sat/satcheck.h>
#include <solvers/refinement/string_constraint_instantiation.h>
#include <java_bytecode/java_types.h>
#include "expr_cast.h"

static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);

Expand Down Expand Up @@ -795,12 +794,13 @@ static optionalt<exprt> get_array(
return {};
}

unsigned n;
if(to_unsigned_integer(to_constant_expr(size_val), n))
auto n_opt = numeric_cast<std::size_t>(size_val);
if(!n_opt)
{
stream << "(sr::get_array) size is not valid" << eom;
return {};
}
std::size_t n = *n_opt;

const array_typet ret_type(char_type, from_integer(n, index_type));
array_exprt ret(ret_type);
Expand All @@ -825,9 +825,11 @@ static optionalt<exprt> get_array(
for(size_t i = 0; i < arr_val.operands().size(); i += 2)
{
exprt index = arr_val.operands()[i];
unsigned idx;
if(!to_unsigned_integer(to_constant_expr(index), idx) && idx<n)
initial_map[idx] = arr_val.operands()[i + 1];
if(auto idx = numeric_cast<std::size_t>(index))
Copy link
Member

Choose a reason for hiding this comment

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

I'd appreciate braces here.

{
if(*idx < n)
initial_map[*idx] = arr_val.operands()[i + 1];
}
}

// Pad the concretized values to the left to assign the uninitialized
Expand All @@ -852,13 +854,11 @@ static optionalt<exprt> get_array(
/// \return a string
static std::string string_of_array(const array_exprt &arr)
{
unsigned n;
if(arr.type().id()!=ID_array)
return std::string("");

exprt size_expr=to_array_type(arr.type()).size();
PRECONDITION(size_expr.id()==ID_constant);
to_unsigned_integer(to_constant_expr(size_expr), n);
auto n = numeric_cast_v<std::size_t>(size_expr);
return utf16_constant_array_to_java(arr, n);
}

Expand Down Expand Up @@ -1010,7 +1010,7 @@ exprt fill_in_array_with_expr(
std::map<std::size_t, exprt> initial_map;

// Set the last index to be sure the array will have the right length
const auto &array_size_opt = expr_cast<std::size_t>(array_type.size());
const auto &array_size_opt = numeric_cast<std::size_t>(array_type.size());
if(array_size_opt && *array_size_opt > 0)
initial_map.emplace(
*array_size_opt - 1,
Expand All @@ -1022,7 +1022,8 @@ exprt fill_in_array_with_expr(
// statements
const with_exprt &with_expr = to_with_expr(it);
const exprt &then_expr=with_expr.new_value();
const auto index=expr_cast_v<std::size_t>(with_expr.where());
const auto index =
numeric_cast_v<std::size_t>(to_constant_expr(with_expr.where()));
if(
index < string_max_length && (!array_size_opt || index < *array_size_opt))
initial_map.emplace(index, then_expr);
Expand All @@ -1047,7 +1048,7 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length)

// Map of the parts of the array that are initialized
std::map<std::size_t, exprt> initial_map;
const auto &array_size_opt = expr_cast<std::size_t>(array_type.size());
const auto &array_size_opt = numeric_cast<std::size_t>(array_type.size());

if(array_size_opt && *array_size_opt > 0)
initial_map.emplace(
Expand Down Expand Up @@ -1180,14 +1181,14 @@ static exprt negation_of_not_contains_constraint(
const exprt &ubu=axiom.univ_upper_bound();
if(lbu.id()==ID_constant && ubu.id()==ID_constant)
{
const auto lb_int=expr_cast<mp_integer>(lbu);
const auto ub_int=expr_cast<mp_integer>(ubu);
const auto lb_int = numeric_cast<mp_integer>(lbu);
const auto ub_int = numeric_cast<mp_integer>(ubu);
if(!lb_int || !ub_int || *ub_int<=*lb_int)
return false_exprt();
}

const auto lbe=expr_cast_v<mp_integer>(axiom.exists_lower_bound());
const auto ube=expr_cast_v<mp_integer>(axiom.exists_upper_bound());
const auto lbe = numeric_cast_v<mp_integer>(axiom.exists_lower_bound());
const auto ube = numeric_cast_v<mp_integer>(axiom.exists_upper_bound());

// If the premise is false, the implication is trivially true, so the
// negation is false.
Expand Down Expand Up @@ -1230,8 +1231,8 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
const exprt &ub=axiom.upper_bound();
if(lb.id()==ID_constant && ub.id()==ID_constant)
{
const auto lb_int=expr_cast<mp_integer>(lb);
const auto ub_int=expr_cast<mp_integer>(ub);
const auto lb_int = numeric_cast<mp_integer>(lb);
const auto ub_int = numeric_cast<mp_integer>(ub);
if(!lb_int || !ub_int || ub_int<=lb_int)
return false_exprt();
}
Expand Down Expand Up @@ -1786,7 +1787,7 @@ static void add_to_index_set(
exprt i)
{
simplify(i, ns);
const bool is_size_t=expr_cast<std::size_t>(i).has_value();
const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
if(i.id()!=ID_constant || is_size_t)
{
std::vector<exprt> sub_arrays;
Expand Down Expand Up @@ -2047,7 +2048,7 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
{
const exprt &index=expr.operands()[i];
const exprt &value=expr.operands()[i+1];
const auto index_value=expr_cast<std::size_t>(index);
const auto index_value = numeric_cast<std::size_t>(index);
if(!index.is_constant() ||
(index_value && *index_value<string_max_length))
ret_expr=with_exprt(ret_expr, index, value);
Expand Down Expand Up @@ -2097,7 +2098,7 @@ exprt string_refinementt::get(const exprt &expr) const
if(set.find(arr) != set.end())
{
exprt length = super_get(arr.length());
if(const auto n = expr_cast<std::size_t>(length))
if(const auto n = numeric_cast<std::size_t>(length))
{
exprt arr_model =
array_exprt(array_typet(arr.type().subtype(), length));
Expand Down
Loading