cprover
Loading...
Searching...
No Matches
c_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes that are internal to the C frontend
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_expr.h"
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/namespace.h>
14#include <util/simplify_expr.h>
15
18 std::optional<exprt> vector2,
21 ID_shuffle_vector,
22 {std::move(vector1), nil_exprt{}, exprt{}},
23 typet{})
24{
25 if(vector2.has_value())
26 op1() = std::move(*vector2);
27
28 const vector_typet &vt = to_vector_type(op0().type());
29 type() = vector_typet{
30 vt.index_type(),
31 vt.element_type(),
32 from_integer(indices.size(), vt.size().type())};
33
34 op2().operands().swap(indices);
35}
36
38{
41
42 if(indices().empty())
44
45 auto input_size =
47 CHECK_RETURN(input_size.has_value());
48
50 operands.reserve(indices().size());
51
52 for(const exprt &index : indices())
53 {
55 {
56 operands.push_back(if_exprt{
58 index, ID_lt, from_integer(*input_size, index.type())},
59 index_exprt{vector1(), index},
61 vector2(),
62 minus_exprt{index, from_integer(*input_size, index.type())}}});
63 }
64 else
65 operands.push_back(index_exprt{vector1(), index});
66 }
67
68 return vector_exprt{std::move(operands), type()};
69}
70
72{
73 const auto &enum_type = to_c_enum_tag_type(op().type());
74 const c_enum_typet &c_enum_type = ns.follow_tag(enum_type);
75 const c_enum_typet::memberst enum_values = c_enum_type.members();
76
77 exprt::operandst disjuncts;
78 for(const auto &enum_value : enum_values)
79 {
80 constant_exprt val{enum_value.get_value(), enum_type};
81 disjuncts.push_back(equal_exprt(op(), std::move(val)));
82 }
83
84 return simplify_expr(disjunction(disjuncts), ns);
85}
86
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
API to expression classes that are internal to the C frontend.
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
byte_extract_exprt lower() const
Definition c_expr.cpp:87
Expression of type type extracted from some object op starting at position offset (given in number of...
The type of C enums.
Definition c_types.h:239
memberst & members()
Definition c_types.h:283
std::vector< c_enum_membert > memberst
Definition c_types.h:275
A constant literal expression.
Definition std_expr.h:3117
exprt lower(const namespacet &ns) const
Definition c_expr.cpp:71
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
exprt()
Definition expr.h:61
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
void swap(irept &irep)
Definition irep.h:434
Binary minus.
Definition std_expr.h:1061
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition std_expr.h:914
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3208
const vector_typet & type() const
Definition c_expr.h:28
const exprt & vector2() const
Definition c_expr.h:48
const exprt::operandst & indices() const
Definition c_expr.h:63
vector_exprt lower() const
Definition c_expr.cpp:37
shuffle_vector_exprt(exprt vector1, std::optional< exprt > vector2, exprt::operandst indices)
Definition c_expr.cpp:16
bool has_two_input_vectors() const
Definition c_expr.h:58
const exprt & vector1() const
Definition c_expr.h:38
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
Vector constructor from list of elements.
Definition std_expr.h:1734
The vector type.
Definition std_types.h:1064
const constant_exprt & size() const
typet index_type() const
The type of any index expression into an instance of this type.
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1080
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:71
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116