Skip to content

Refactor numeric_cast #1

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

Closed
reuk wants to merge 10 commits into from
Closed

Refactor numeric_cast #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
9417823
Add validate and can_cast method to string_exprt
romainbrenguier Nov 9, 2017
c619a5f
Add source type argument to numeric_cast template
romainbrenguier Nov 15, 2017
b1ee09b
Extend numeric_cast for constant expressions
romainbrenguier Nov 13, 2017
f4a4b30
Add a numeric_cast_v function
romainbrenguier Nov 17, 2017
7352f60
Use numeric_cast instead of refinement/expr_cast
romainbrenguier Nov 15, 2017
4c20c4e
Remove solvers/refinement/expr_cast.h
romainbrenguier Nov 8, 2017
873c9eb
Style: remove useless brackets
romainbrenguier Nov 24, 2017
d8511a0
Use numeric_cast instead of other conversion
romainbrenguier Dec 1, 2017
924d664
Adapting static_assert for VS
romainbrenguier Dec 1, 2017
2e3adc0
Refactor numeric_cast
reuk Dec 1, 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.

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<size_t>(expr1_str.length());
const auto expr2_length = numeric_cast<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
47 changes: 25 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<unsigned>(size_val);
if(!n_opt)
{
stream << "(sr::get_array) size is not valid" << eom;
return {};
}
unsigned 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,9 @@ 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))
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 +852,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<unsigned>(size_expr);
return utf16_constant_array_to_java(arr, n);
}

Expand Down Expand Up @@ -1010,7 +1008,8 @@ 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 +1021,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 +1047,8 @@ 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,16 @@ 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>(
to_constant_expr(axiom.exists_lower_bound()));
const auto ube = numeric_cast_v<mp_integer>(
to_constant_expr(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 +1233,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 +1789,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 +2050,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 +2100,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
91 changes: 0 additions & 91 deletions src/util/arith_tools.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,97 +15,6 @@ Author: Daniel Kroening, [email protected]
#include "std_types.h"
#include "std_expr.h"

bool to_integer(const exprt &expr, mp_integer &int_value)
{
if(!expr.is_constant())
return true;
return to_integer(to_constant_expr(expr), int_value);
}

bool to_integer(const constant_exprt &expr, mp_integer &int_value)
{
const irep_idt &value=expr.get_value();
const typet &type=expr.type();
const irep_idt &type_id=type.id();

if(type_id==ID_pointer)
{
if(value==ID_NULL)
{
int_value=0;
return false;
}
}
else if(type_id==ID_integer ||
type_id==ID_natural)
{
int_value=string2integer(id2string(value));
return false;
}
else if(type_id==ID_unsignedbv)
{
int_value=binary2integer(id2string(value), false);
return false;
}
else if(type_id==ID_signedbv)
{
int_value=binary2integer(id2string(value), true);
return false;
}
else if(type_id==ID_c_bool)
{
int_value=binary2integer(id2string(value), false);
return false;
}
else if(type_id==ID_c_enum)
{
const typet &subtype=to_c_enum_type(type).subtype();
if(subtype.id()==ID_signedbv)
{
int_value=binary2integer(id2string(value), true);
return false;
}
else if(subtype.id()==ID_unsignedbv)
{
int_value=binary2integer(id2string(value), false);
return false;
}
}
else if(type_id==ID_c_bit_field)
{
const typet &subtype=type.subtype();
if(subtype.id()==ID_signedbv)
{
int_value=binary2integer(id2string(value), true);
return false;
}
else if(subtype.id()==ID_unsignedbv)
{
int_value=binary2integer(id2string(value), false);
return false;
}
}

return true;
}

/// convert a positive integer expression to an unsigned int
/// \par parameters: a constant expression and a reference to an unsigned int
/// \return an error flag
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
{
mp_integer i;
if(to_integer(expr, i))
return true;
if(i<0)
return true;
else
{
uint_value=integer2unsigned(i);
return false;
}
}

constant_exprt from_integer(
const mp_integer &int_value,
const typet &type)
Expand Down
12 changes: 2 additions & 10 deletions src/util/arith_tools.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,21 +11,13 @@ Author: Daniel Kroening, [email protected]
#define CPROVER_UTIL_ARITH_TOOLS_H

#include "mp_arith.h"
#include "optional.h"
#include "invariant.h"

class exprt;
class constant_exprt;
class typet;

// this one will go away
// returns 'true' on error
bool to_integer(const exprt &expr, mp_integer &int_value);

// returns 'true' on error
bool to_integer(const constant_exprt &expr, mp_integer &int_value);

// returns 'true' on error
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value);

// PRECONDITION(false) in case of unsupported type
constant_exprt from_integer(const mp_integer &int_value, const typet &type);

Expand Down
Loading