cprover
c_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes that are internal to the C frontend
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "c_expr.h"
10 
11 #include <util/arith_tools.h>
12 
14  exprt vector1,
15  optionalt<exprt> vector2,
16  exprt::operandst indices)
18  ID_shuffle_vector,
19  {std::move(vector1), nil_exprt{}, exprt{}},
20  typet{})
21 {
22  if(vector2.has_value())
23  op1() = std::move(*vector2);
24 
25  const vector_typet &vt = to_vector_type(op0().type());
26  type() = vector_typet{vt.element_type(),
27  from_integer(indices.size(), vt.size().type())};
28 
29  op2().operands().swap(indices);
30 }
31 
33 {
35  !has_two_input_vectors() || vector1().type() == vector2().type());
36 
37  if(indices().empty())
38  return vector_exprt{exprt::operandst{}, type()};
39 
40  auto input_size =
41  numeric_cast<mp_integer>(to_vector_type(vector1().type()).size());
42  CHECK_RETURN(input_size.has_value());
43 
45  operands.reserve(indices().size());
46 
47  for(const exprt &index : indices())
48  {
50  {
51  operands.push_back(if_exprt{
53  index, ID_lt, from_integer(*input_size, index.type())},
54  index_exprt{vector1(), index},
56  vector2(),
57  minus_exprt{index, from_integer(*input_size, index.type())}}});
58  }
59  else
60  operands.push_back(index_exprt{vector1(), index});
61  }
62 
63  return vector_exprt{std::move(operands), type()};
64 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes that are internal to the C frontend.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
Binary minus.
Definition: std_expr.h:973
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
The NIL expression.
Definition: std_expr.h:2874
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
Definition: c_expr.cpp:13
const vector_typet & type() const
Definition: c_expr.h:27
vector_exprt lower() const
Definition: c_expr.cpp:32
const exprt & vector2() const
Definition: c_expr.h:47
const exprt & vector1() const
Definition: c_expr.h:37
const exprt::operandst & indices() const
Definition: c_expr.h:62
bool has_two_input_vectors() const
Definition: c_expr.h:57
The type of an expression, extends irept.
Definition: type.h:29
Vector constructor from list of elements.
Definition: std_expr.h:1575
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
nonstd::optional< T > optionalt
Definition: optional.h:35
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040