35 return shared_from_this();
48 if(other->is_bottom())
50 return shared_from_this();
54 auto other_value_set =
58 auto const &other_values = other_value_set->get_values();
59 merged_values.insert(other_values.begin(), other_values.end());
60 return std::make_shared<value_set_abstract_valuet>(
61 type(), std::move(merged_values));
69 :
abstract_objectt{type, values.size() > max_value_set_size, values.empty()},
70 values{std::move(values)}
114 std::vector<std::string> vals;
115 for(
const auto &elem :
values)
117 vals.push_back(
expr2c(elem, ns));
120 std::sort(vals.begin(), vals.end());
123 for(
const auto &val : vals)
131 std::shared_ptr<const value_set_abstract_valuet> &out_value,
133 const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
135 std::vector<exprt> &operands_so_far)
137 if(expr.
operands().size() == operands_so_far.size())
139 exprt expr_with_evaluated_operands_filled_in = expr;
140 expr_with_evaluated_operands_filled_in.
operands() = operands_so_far;
141 simplify(expr_with_evaluated_operands_filled_in, ns);
142 if(expr_with_evaluated_operands_filled_in.
is_constant())
146 std::make_shared<value_set_abstract_valuet>(
149 expr_with_evaluated_operands_filled_in}));
151 auto post_merge_casted =
152 std::dynamic_pointer_cast<const value_set_abstract_valuet>(
155 out_value = post_merge_casted;
159 out_value = std::make_shared<value_set_abstract_valuet>(expr.
type());
163 for(
auto const &operand_value :
164 operand_value_sets[operands_so_far.size()]->get_values())
166 operands_so_far.push_back(operand_value);
168 out_value, expr, operand_value_sets, ns, operands_so_far);
169 operands_so_far.pop_back();
174 static std::shared_ptr<const value_set_abstract_valuet>
177 const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
180 const bool is_top =
false;
181 const bool is_bottom =
true;
182 auto result_abstract_value =
183 std::make_shared<const value_set_abstract_valuet>(
184 expr.
type(), is_top, is_bottom);
185 auto operands_so_far = std::vector<exprt>{};
187 result_abstract_value, expr, operand_value_sets, ns, operands_so_far);
188 return result_abstract_value;
193 const std::vector<abstract_object_pointert> &operands,
200 auto operand_value_sets = std::vector<const value_set_abstract_valuet *>{};
201 for(
auto const &possible_value_set : operands)
204 const auto as_value_set =
207 as_value_set ==
nullptr || as_value_set->is_top() ||
208 as_value_set->is_bottom())
210 return std::make_shared<value_set_abstract_valuet>(expr.
type());
212 operand_value_sets.push_back(as_value_set);
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Base class for all expressions.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The type of an expression, extends irept.
static constexpr CLONE std::size_t max_value_set_size
TODO arbitrary limit, make configurable.
const valuest & get_values() const
Get the possible values for this abstract object.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
valuest values
If BOTTOM then empty.
std::unordered_set< exprt, irep_hash > valuest
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Print the value of the abstract object.
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
value_set_abstract_valuet(const typet &type, bool top=true, bool bottom=false)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION(CONDITION)
static void merge_all_possible_results(std::shared_ptr< const value_set_abstract_valuet > &out_value, const exprt &expr, const std::vector< const value_set_abstract_valuet * > &operand_value_sets, const namespacet &ns, std::vector< exprt > &operands_so_far)
Value sets for primitives.