Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void clear_cache () override

mp_integer get_value (const bvt &bv)

mp_integer get_value (const bvt &bv, std::size_t offset, std::size_t width)

const boolbv_mapt & get_map () const

virtual std::size_t boolbv_width (const typet &type) const

virtual endianness_mapt endianness_map (const typet &type) const

- Public Member Functions inherited from arrayst

arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)

literalt record_array_equality (const equal_exprt &expr)

void record_array_index (const index_exprt &expr)

void record_array_let_binding (const symbol_exprt &symbol, const exprt &value)

Record that symbol is equal to value for the purposes of the array theory.

- Public Member Functions inherited from equalityt

equalityt (propt &_prop, message_handlert &message_handler)

virtual literalt equality (const exprt &e1, const exprt &e2)

void finish_eager_conversion () override

- Public Member Functions inherited from prop_conv_solvert

prop_conv_solvert (propt &_prop, message_handlert &message_handler)

virtual ~prop_conv_solvert ()=default

decision_proceduret::resultt dec_solve (const exprt &) override

Implementation of the decision procedure.

void print_assignment (std::ostream &out) const override

Print satisfying assignment to out.

std::string decision_procedure_text () const override

Return a textual description of the decision procedure.

exprt get (const exprt &expr) const override

Return expr with variables replaced by values from satisfying assignment if available.

tvt l_get (literalt a) const override

Return value of literal l from satisfying assignment.

exprt handle (const exprt &expr) override

Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void set_frozen (literalt)

void set_frozen (const bvt &)

void set_all_frozen ()

literalt convert (const exprt &expr) override

Convert a Boolean expression and return the corresponding literal.

bool is_in_conflict (const exprt &expr) const override

Returns true if an expression is in the final conflict leading to UNSAT.

void set_to (const exprt &expr, bool value) override

For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'.

void push () override

Push a new context on the stack This context becomes a child context nested in the current context.

void push (const std::vector< exprt > &assumptions) override

Push assumptions in form of literal_exprt

void pop () override

Pop whatever is on top of the stack.

const cachet & get_cache () const

const symbolst & get_symbols () const

void set_time_limit_seconds (uint32_t lim) override

Set the limit for the solver to time out in seconds.

std::size_t get_number_of_solver_calls () const override

Return the number of incremental solver calls.

hardness_collectort * get_hardness_collector ()

- Public Member Functions inherited from conflict_providert

virtual ~conflict_providert ()=default

- Public Member Functions inherited from prop_convt

virtual ~prop_convt ()

- Public Member Functions inherited from stack_decision_proceduret

virtual ~stack_decision_proceduret ()=default

- Public Member Functions inherited from decision_proceduret

void set_to_true (const exprt &)

For a Boolean expression expr, add the constraint 'expr'.

void set_to_false (const exprt &)

For a Boolean expression expr, add the constraint 'not expr'.

resultt operator() ()

Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt operator() (const exprt &assumption)

Run the decision procedure to solve the problem under the given assumption.

virtual ~decision_proceduret ()

- Public Member Functions inherited from solver_resource_limitst

virtual ~solver_resource_limitst ()=default

Protected Types

typedef boolbvt SUB

typedef std::list< postponedt > postponed_listt

- Protected Types inherited from boolbvt

typedef arrayst SUB

typedef std::unordered_map< const exprt, bvt, irep_hash > bv_cachet

typedef std::list< quantifiert > quantifier_listt

typedef std::vector< std::size_t > offset_mapt

- Protected Types inherited from arrayst

enum class lazy_typet {
ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF ,
ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_LET
}

enum class constraint_typet {
  ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF ,
  ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY ,
  ARRAY_LET
}

typedef std::list< array_equalityt > array_equalitiest

typedef std::set< exprt > index_sett

typedef std::map< std::size_t, index_sett > index_mapt

typedef std::map< constraint_typet, size_t > array_constraint_countt

- Protected Types inherited from equalityt

typedef std::unordered_map< const exprt, unsigned, irep_hash > elementst

typedef std::map< std::pair< unsigned, unsigned >, literalt > equalitiest

typedef std::map< unsigned, exprt > elements_revt

typedef std::unordered_map< const typet, typestructt, irep_hash > typemapt

Protected Member Functions

std::size_t get_object_width (const pointer_typet &) const

std::size_t get_offset_width (const pointer_typet &) const

std::size_t get_address_width (const pointer_typet &) const

bvt encode (const mp_integer &object, const pointer_typet &) const

virtual bvt convert_pointer_type (const exprt &)

virtual bvt add_addr (const exprt &)

literalt convert_rest (const exprt &) override

bvt convert_bitvector (const exprt &) override

Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit.

exprt bv_get_rec (const exprt &, const bvt &, std::size_t offset) const override

std::optional< bvt > convert_address_of_rec (const exprt &)

bvt offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &)

bvt offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const exprt &index)

bvt offset_arithmetic (const pointer_typet &type, const bvt &bv, const exprt &factor, const exprt &index)

bvt offset_arithmetic (const pointer_typet &, const bvt &, const mp_integer &factor, const bvt &index_bv)

std::pair< exprt, exprt > prepare_postponed_is_dynamic_object (std::vector< symbol_exprt > &placeholders) const

Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholders as input Boolean variables representing object bits.

std::unordered_map< exprt, exprt, irep_hash > prepare_postponed_object_size (std::vector< symbol_exprt > &placeholders) const

Create Boolean functions describing all objects of each known object size over placeholders as input Boolean variables representing object bits.

bvt object_literals (const bvt &bv, const pointer_typet &type) const

Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to.

bvt offset_literals (const bvt &bv, const pointer_typet &type) const

Given a pointer encoded in bv, extract the literals representing the offset into an object that the pointer points to.

- Protected Member Functions inherited from boolbvt

virtual bool boolbv_set_equality_to_true (const equal_exprt &expr)

bvt conversion_failed (const exprt &expr)

Print that the expression of x has failed conversion, then return a vector of x's width.

bool type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)

virtual literalt convert_bv_rel (const binary_relation_exprt &)

Flatten <, >, <= and >= expressions.

virtual literalt convert_typecast (const typecast_exprt &expr)

conversion from bitvector types to boolean

virtual literalt convert_reduction (const unary_exprt &expr)

virtual literalt convert_onehot (const unary_exprt &expr)

virtual literalt convert_extractbit (const extractbit_exprt &expr)

virtual literalt convert_binary_overflow (const binary_overflow_exprt &expr)

virtual literalt convert_unary_overflow (const unary_overflow_exprt &expr)

virtual literalt convert_equality (const equal_exprt &expr)

virtual literalt convert_verilog_case_equality (const binary_relation_exprt &expr)

virtual literalt convert_ieee_float_rel (const binary_relation_exprt &)

virtual literalt convert_quantifier (const quantifier_exprt &expr)

virtual bvt convert_index (const exprt &array, const mp_integer &index)

index operator with constant index

virtual bvt convert_index (const index_exprt &expr)

virtual bvt convert_bswap (const bswap_exprt &expr)

virtual bvt convert_byte_extract (const byte_extract_exprt &expr)

virtual bvt convert_byte_update (const byte_update_exprt &expr)

virtual bvt convert_constraint_select_one (const exprt &expr)

virtual bvt convert_if (const if_exprt &expr)

virtual bvt convert_struct (const struct_exprt &expr)

virtual bvt convert_array (const exprt &expr)

Flatten array.

virtual bvt convert_complex (const complex_exprt &expr)

virtual bvt convert_complex_real (const complex_real_exprt &expr)

virtual bvt convert_complex_imag (const complex_imag_exprt &expr)

virtual bvt convert_array_comprehension (const array_comprehension_exprt &)

virtual bvt convert_let (const let_exprt &)

virtual bvt convert_array_of (const array_of_exprt &expr)

Flatten arrays constructed from a single element.

virtual bvt convert_union (const union_exprt &expr)

virtual bvt convert_empty_union (const empty_union_exprt &expr)

virtual bvt convert_bv_typecast (const typecast_exprt &expr)

virtual bvt convert_add_sub (const exprt &expr)

virtual bvt convert_mult (const mult_exprt &expr)

virtual bvt convert_div (const div_exprt &expr)

virtual bvt convert_mod (const mod_exprt &expr)

virtual bvt convert_floatbv_op (const ieee_float_op_exprt &)

virtual bvt convert_floatbv_mod_rem (const binary_exprt &)

virtual bvt convert_floatbv_fma (const floatbv_fma_exprt &)

virtual bvt convert_floatbv_typecast (const floatbv_typecast_exprt &expr)

virtual bvt convert_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &)

virtual bvt convert_member (const member_exprt &expr)

virtual bvt convert_with (const with_exprt &expr)

virtual bvt convert_update (const update_exprt &)

virtual bvt convert_update_bit (const update_bit_exprt &)

virtual bvt convert_update_bits (const update_bits_exprt &)

virtual bvt convert_cond (const cond_exprt &)

virtual bvt convert_shift (const binary_exprt &expr)

virtual bvt convert_bitwise (const exprt &expr)

virtual bvt convert_unary_minus (const unary_minus_exprt &expr)

virtual bvt convert_abs (const abs_exprt &expr)

virtual bvt convert_concatenation (const concatenation_exprt &expr)

virtual bvt convert_replication (const replication_exprt &expr)

virtual bvt convert_constant (const constant_exprt &expr)

virtual bvt convert_extractbits (const extractbits_exprt &expr)

virtual bvt convert_symbol (const exprt &expr)

virtual bvt convert_bv_reduction (const unary_exprt &expr)

virtual bvt convert_not (const not_exprt &expr)

virtual bvt convert_power (const power_exprt &expr)

virtual bvt convert_function_application (const function_application_exprt &expr)

virtual bvt convert_bitreverse (const bitreverse_exprt &expr)

virtual bvt convert_saturating_add_sub (const binary_exprt &expr)

virtual bvt convert_overflow_result (const overflow_result_exprt &expr)

virtual bvt convert_popcount (const popcount_exprt &expr)

bvt convert_update_bits (bvt src, const exprt &index, const bvt &new_value)

void convert_with (const typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void convert_with_bv (const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void convert_with_array (const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void convert_with_union (const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void convert_with_struct (const struct_typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void convert_update_rec (const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)

virtual exprt bv_get_unbounded_array (const exprt &) const

exprt bv_get (const bvt &bv, const typet &type) const

exprt bv_get_cache (const exprt &expr) const

exprt get_value (const exprt &expr) const

Return the model value for expr.

bool is_unbounded_array (const typet &type) const override

void finish_eager_conversion_quantifiers ()

offset_mapt build_offset_map (const struct_typet &src)

binding_exprt::variablest fresh_binding (const binding_exprt &)

create new, unique variables for the given binding

- Protected Member Functions inherited from arrayst

virtual void finish_eager_conversion_arrays ()

void add_array_constraint (const lazy_constraintt &lazy, bool refine=true)

adds array constraints (refine=true...lazily for the refinement loop)

void display_array_constraint_count ()

std::string enum_to_string (constraint_typet)

void add_array_constraints ()

void add_array_Ackermann_constraints ()

void add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality)

void add_array_constraints (const index_sett &index_set, const exprt &expr)

void add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt)

void add_array_constraints_with (const index_sett &index_set, const with_exprt &expr)

void add_array_constraints_update (const index_sett &index_set, const update_exprt &expr)

void add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt)

void add_array_constraints_array_constant (const index_sett &index_set, const array_exprt &exprt)

void add_array_constraints_comprehension (const index_sett &index_set, const array_comprehension_exprt &expr)

void update_index_map (bool update_all)

void update_index_map (std::size_t i)

merge the indices into the root

void collect_arrays (const exprt &a)

void collect_indices ()

void collect_indices (const exprt &a)

- Protected Member Functions inherited from equalityt

virtual literalt equality2 (const exprt &e1, const exprt &e2)

virtual void add_equality_constraints ()

virtual void add_equality_constraints (const typestructt &typestruct)

- Protected Member Functions inherited from prop_conv_solvert

virtual std::optional< bool > get_bool (const exprt &expr) const

Get a boolean value from the model if the formula is satisfiable.

virtual literalt convert_bool (const exprt &expr)

virtual bool set_equality_to_true (const equal_exprt &expr)

virtual literalt get_literal (const irep_idt &symbol)

virtual void ignoring (const exprt &expr)

Static Protected Member Functions

static bvt object_offset_encoding (const bvt &object, const bvt &offset)

Construct a pointer encoding from given encodings of object and offset.

Protected Attributes

pointer_logict pointer_logic

postponed_listt postponed_list

- Protected Attributes inherited from boolbvt

boolbv_widtht bv_width

bv_utilst bv_utils

functionst functions

boolbv_mapt map

bv_cachet bv_cache

quantifier_listt quantifier_list

numberingt< irep_idt > string_numbering

std::size_t scope_counter = 0

- Protected Attributes inherited from arrayst

const namespacet & ns

messaget log

message_handlert & message_handler

array_equalitiest array_equalities

union_find< exprt, irep_hash > arrays

index_mapt index_map

bool lazy_arrays

bool incremental_cache

bool get_array_constraints

std::list< lazy_constraintt > lazy_array_constraints

std::map< exprt, bool > expr_map

array_constraint_countt array_constraint_count

std::set< std::size_t > update_indices

std::unordered_set< irep_idt > array_comprehension_args

- Protected Attributes inherited from equalityt

typemapt typemap

- Protected Attributes inherited from prop_conv_solvert

bool post_processing_done = false

symbolst symbols

cachet cache

propt & prop

messaget log

bvt assumption_stack

Assumptions on the stack.

std::size_t context_literal_counter = 0

To generate unique literal names for contexts.

std::vector< size_t > context_size_stack

assumption_stack is segmented in contexts; Number of assumptions in each context on the stack

Additional Inherited Members

- Public Types inherited from boolbvt

enum class unbounded_arrayt { U_NONE , U_ALL , U_AUTO }

- Public Types inherited from arrayst

typedef equalityt SUB

- Public Types inherited from equalityt

using SUB = prop_conv_solvert

- Public Types inherited from prop_conv_solvert

typedef std::map< irep_idt, literalt > symbolst

typedef std::unordered_map< exprt, literalt, irep_hash > cachet

- Public Types inherited from decision_proceduret

enum class resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }

Result of running the decision procedure. More...

- Public Attributes inherited from boolbvt

unbounded_arrayt unbounded_array

- Public Attributes inherited from prop_conv_solvert

bool use_cache = true

bool equality_propagation = true

bool freeze_all = false

- Static Protected Attributes inherited from prop_conv_solvert

static const char * context_prefix = "prop_conv::context$"

Detailed Description

Definition at line 16 of file bv_pointers.h.

Member Typedef Documentation

◆ postponed_listt

typedef std::list<postponedt> bv_pointerst::postponed_listt

protected

Definition at line 85 of file bv_pointers.h.

◆ SUB

typedef boolbvt bv_pointerst::SUB

protected

Definition at line 38 of file bv_pointers.h.

Constructor & Destructor Documentation

◆ bv_pointerst()

bv_pointerst::bv_pointerst ( const namespacet & _ns,

propt & _prop,

message_handlert & message_handler,

bool get_array_constraints = false

)

Definition at line 227 of file bv_pointers.cpp.

Member Function Documentation

◆ add_addr()

bvt bv_pointerst::add_addr ( const exprt & expr )

protectedvirtual

Definition at line 879 of file bv_pointers.cpp.

◆ bv_get_rec()

exprt bv_pointerst::bv_get_rec ( const exprt & expr,

const bvt & bv,

std::size_t offset

) const

overrideprotectedvirtual

Reimplemented from boolbvt.

Definition at line 754 of file bv_pointers.cpp.

◆ convert_address_of_rec()

std::optional< bvt > bv_pointerst::convert_address_of_rec ( const exprt & expr )

protected

Definition at line 237 of file bv_pointers.cpp.

◆ convert_bitvector()

bvt bv_pointerst::convert_bitvector ( const exprt & expr )

overrideprotectedvirtual

Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit.

Parameters: expr Expression to convert

Returns: A vector of literals corresponding to the outputs of the Boolean circuit

Reimplemented from boolbvt.

Definition at line 621 of file bv_pointers.cpp.

◆ convert_pointer_type()

bvt bv_pointerst::convert_pointer_type ( const exprt & expr )

protectedvirtual

Definition at line 376 of file bv_pointers.cpp.

◆ convert_rest()

literalt bv_pointerst::convert_rest ( const exprt & expr )

overrideprotectedvirtual

Reimplemented from boolbvt.

Definition at line 126 of file bv_pointers.cpp.

◆ encode()

bvt bv_pointerst::encode ( const mp_integer & object,

const pointer_typet & type

) const

protected

Definition at line 790 of file bv_pointers.cpp.

◆ endianness_map()

endianness_mapt bv_pointerst::endianness_map ( const typet & type,

bool little_endian

) const

overridevirtual

Reimplemented from boolbvt.

Definition at line 72 of file bv_pointers.cpp.

◆ finish_eager_conversion()

void bv_pointerst::finish_eager_conversion ( )

overridevirtual

Reimplemented from boolbvt.

Definition at line 1005 of file bv_pointers.cpp.

◆ get_address_width()

std::size_t bv_pointerst::get_address_width ( const pointer_typet & type ) const

protected

Definition at line 91 of file bv_pointers.cpp.

◆ get_object_width()

std::size_t bv_pointerst::get_object_width ( const pointer_typet & ) const

protected

Definition at line 77 of file bv_pointers.cpp.

◆ get_offset_width()

std::size_t bv_pointerst::get_offset_width ( const pointer_typet & type ) const

protected

Definition at line 83 of file bv_pointers.cpp.

◆ object_literals()

bvt bv_pointerst::object_literals ( const bvt & bv,

const pointer_typet & type

) const

protected

Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to.

Parameters: bv Encoded pointer

type Type of the encoded pointer

Returns: Vector of literals identifying the object part of bv

Definition at line 96 of file bv_pointers.cpp.

◆ object_offset_encoding()

bvt bv_pointerst::object_offset_encoding ( const bvt & object,

const bvt & offset

)

staticprotected

Construct a pointer encoding from given encodings of object and offset.

Parameters: object Encoded object

offset Encoded offset

Returns: Pointer encoding

Definition at line 116 of file bv_pointers.cpp.

◆ offset_arithmetic() [1/4]

bvt bv_pointerst::offset_arithmetic ( const pointer_typet & type,

const bvt & bv,

const mp_integer & x

)

protected

Definition at line 802 of file bv_pointers.cpp.

◆ offset_arithmetic() [2/4]

bvt bv_pointerst::offset_arithmetic ( const pointer_typet & type,

const bvt & bv,

const mp_integer & factor,

const bvt & index_bv

)

protected

Definition at line 853 of file bv_pointers.cpp.

◆ offset_arithmetic() [3/4]

bvt bv_pointerst::offset_arithmetic ( const pointer_typet & type,

const bvt & bv,

const mp_integer & factor,

const exprt & index

)

protected

Definition at line 813 of file bv_pointers.cpp.

◆ offset_arithmetic() [4/4]

bvt bv_pointerst::offset_arithmetic ( const pointer_typet & type,

const bvt & bv,

const exprt & factor,

const exprt & index

)

protected

Definition at line 831 of file bv_pointers.cpp.

◆ offset_literals()

bvt bv_pointerst::offset_literals ( const bvt & bv,

const pointer_typet & type

) const

protected

Given a pointer encoded in bv, extract the literals representing the offset into an object that the pointer points to.

Parameters: bv Encoded pointer

type Type of the encoded pointer

Returns: Vector of literals identifying the offset part of bv

Definition at line 107 of file bv_pointers.cpp.

◆ prepare_postponed_is_dynamic_object()

std::pair< exprt, exprt > bv_pointerst::prepare_postponed_is_dynamic_object ( std::vector< symbol_exprt > & placeholders ) const

protected

Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholders as input Boolean variables representing object bits.

Definition at line 897 of file bv_pointers.cpp.

◆ prepare_postponed_object_size()

std::unordered_map< exprt, exprt, irep_hash > bv_pointerst::prepare_postponed_object_size ( std::vector< symbol_exprt > & placeholders ) const

protected

Create Boolean functions describing all objects of each known object size over placeholders as input Boolean variables representing object bits.

Definition at line 949 of file bv_pointers.cpp.

Member Data Documentation

◆ pointer_logic

pointer_logict bv_pointerst::pointer_logic

protected

Definition at line 31 of file bv_pointers.h.

◆ postponed_list

postponed_listt bv_pointerst::postponed_list

protected

Definition at line 86 of file bv_pointers.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/solvers/flattening/bv_pointers.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/bv_pointers.cpp