cprover
Loading...
Searching...
No Matches
struct_encoding.cpp File Reference
#include "struct_encoding.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/c_types.h>
#include <util/make_unique.h>
#include <util/namespace.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include <solvers/flattening/boolbv_width.h>
#include <solvers/smt2_incremental/encoding/nondet_padding.h>
#include <algorithm>
#include <numeric>
#include <queue>
+ Include dependency graph for struct_encoding.cpp:

Go to the source code of this file.

Functions

static optionalt< std::size_t > needs_width (const typet &type, const boolbv_widtht &boolbv_width)
 If the given type needs re-encoding as a bit-vector then this function.
 
static std::unordered_map< irep_idt, exprtextricate_updates (const with_exprt &struct_expr)
 Extracts the component/field names and new values from a with_exprt which expresses a new struct value where one or more members of a struct have had their values substituted with new values.
 
static exprt encode (const with_exprt &with, const namespacet &ns)
 
static exprt empty_encoding ()
 Empty structs and unions are encoded as a zero byte.
 
static exprt encode (const struct_exprt &struct_expr)
 Structs are flattened into a large bit vector using concatenation to express all the member operands of struct_expr.
 
static exprt encode (const union_exprt &union_expr, const boolbv_widtht &bit_width)
 
static std::size_t count_trailing_bit_width (const struct_typet &type, const irep_idt name, const boolbv_widtht &boolbv_width)
 

Function Documentation

◆ count_trailing_bit_width()

static std::size_t count_trailing_bit_width ( const struct_typet & type,
const irep_idt name,
const boolbv_widtht & boolbv_width )
static

Definition at line 163 of file struct_encoding.cpp.

◆ empty_encoding()

static exprt empty_encoding ( )
static

Empty structs and unions are encoded as a zero byte.

This has useful properties such as -

  • A zero byte is valid SMT, unlike zero length bit vectors.
  • Any two zero byte instances are always equal. This property would not be true of two instances of a non-det byte for instance.

Definition at line 130 of file struct_encoding.cpp.

◆ encode() [1/3]

static exprt encode ( const struct_exprt & struct_expr)
static

Structs are flattened into a large bit vector using concatenation to express all the member operands of struct_expr.

Definition at line 138 of file struct_encoding.cpp.

◆ encode() [2/3]

static exprt encode ( const union_exprt & union_expr,
const boolbv_widtht & bit_width )
static

Definition at line 148 of file struct_encoding.cpp.

◆ encode() [3/3]

static exprt encode ( const with_exprt & with,
const namespacet & ns )
static

Definition at line 105 of file struct_encoding.cpp.

◆ extricate_updates()

static std::unordered_map< irep_idt, exprt > extricate_updates ( const with_exprt & struct_expr)
static

Extracts the component/field names and new values from a with_exprt which expresses a new struct value where one or more members of a struct have had their values substituted with new values.

Note
This is implemented using direct access to the operands and other underlying irept interfaces, because the interface for with_exprt only supports a single where / new_value pair and does not support extracting the name from the where operand.

Definition at line 82 of file struct_encoding.cpp.

◆ needs_width()

static optionalt< std::size_t > needs_width ( const typet & type,
const boolbv_widtht & boolbv_width )
static

If the given type needs re-encoding as a bit-vector then this function.

Returns
the width of the new bitvector type. The width calculation is delegated to boolbv_width.

Definition at line 38 of file struct_encoding.cpp.