ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
cmp_three_way2t Class Reference

C++20 three-way comparison a <=> b. More...

#include <irep2_expr.h>

Inheritance diagram for cmp_three_way2t:
[legend]

Public Member Functions

 cmp_three_way2t (const type2tc &t, const expr2tc &v1, const expr2tc &v2)
 cmp_three_way2t (const cmp_three_way2t &ref)=default
expr2tc do_simplify () const override
 expr-specific simplification methods.
Public Member Functions inherited from expr2t
virtual ~expr2t ()=default
expr2tc clone () const
expr2tc with_type (const type2tc &new_type) const
 Build a fresh expression of the same kind and field values as this one, but with a different type.
bool operator== (const expr2t &ref) const
bool operator< (const expr2t &ref) const
bool operator!= (const expr2t &ref) const
std::string pretty (unsigned int indent=0) const
 Produce textual representation of this expr.
DUMP_METHOD void dump () const
 Write textual representation of this object to stdout.
size_t crc () const
 Calculate a hash/digest of the current expr.
bool cmp (const expr2t &ref) const
 Structural comparison.
int lt (const expr2t &ref) const
 Trinary structural ordering.
list_of_memberst tostring (unsigned int indent) const
 Convert fields of subclasses to a string representation.
const expr2tc * get_sub_expr (size_t idx) const
 Fetch a sub-operand.
size_t get_num_sub_exprs () const
 Count the number of sub-exprs there are.
expr2tc simplify () const
 Simplify an expression.
expr2tc simplify (bool suppress_reassoc) const
 Simplify with reassociation suppression.
template<typename T>
void foreach_operand (T &&t) const
 Indirect, abstract operand iteration.
template<typename T>
void Foreach_operand (T &&t)
Public Member Functions inherited from irep2t
 irep2t () noexcept
 irep2t (const irep2t &) noexcept
irep2t & operator= (const irep2t &)=delete
virtual ~irep2t ()=default
void mark_writer () const noexcept
void clear_writer () const noexcept

Public Attributes

expr2tc side_1
expr2tc side_2
Public Attributes inherited from expr2t
const expr_ids expr_id
 Instance of expr_ids recording tihs exprs type.
const type2tc type
 Type of this expr.
std::atomic< size_t > crc_val
Public Attributes inherited from irep2t
std::atomic< unsigned int > refcount
std::atomic< std::uintptr_t > writer_thread

Static Public Attributes

static constexpr auto fields
static std::string field_names [esbmct::num_type_fields]

Additional Inherited Members

Public Types inherited from expr2t
enum  expr_ids { end_expr_id }
 Enumeration identifying each sort of expr. More...
typedef esbmct::function_ref< void(const expr2tc &)> const_op_delegate
typedef esbmct::function_ref< void(expr2tc &)> op_delegate
typedef expr2tc container_type
typedef expr2t base_type
Static Public Member Functions inherited from irep2t
static std::uintptr_t current_thread_tag () noexcept
Protected Member Functions inherited from expr2t
 expr2t (const type2tc &type, expr_ids id)
 Primary constructor.
 expr2t (const expr2t &ref)
 Copy constructor.
void foreach_operand_impl_const (const_op_delegate &expr) const
void foreach_operand_impl (op_delegate &expr)

Detailed Description

C++20 three-way comparison a <=> b.

Result type is the comparison-category struct (std::strong_ordering / std::weak_ordering / std::partial_ordering); the discriminating signed-char member sits at the start of the struct. The expansion to

side_1 < side_2 -> T{-1} (less) side_1 == side_2 -> T{ 0} (equivalent / equal) else -> T{ 1} (greater)

is performed at the SMT layer rather than the AST level so the semantic node survives through symex / value_set / interval analysis, and operands are captured once. Per [expr.spaceship] in N4861.

Constructor & Destructor Documentation

◆ cmp_three_way2t() [1/2]

cmp_three_way2t::cmp_three_way2t ( const type2tc & t,
const expr2tc & v1,
const expr2tc & v2 )
inline

◆ cmp_three_way2t() [2/2]

cmp_three_way2t::cmp_three_way2t ( const cmp_three_way2t & ref)
default

Member Function Documentation

◆ do_simplify()

expr2tc cmp_three_way2t::do_simplify ( ) const
overridevirtual

expr-specific simplification methods.

By default, an expression can't be simplified, and this method returns a nil expression to show that. However if simplification is possible, the subclass overrides this and if it can simplify its operands, returns a new simplified expression. It should attempt to modify itself (it's const).

If simplification failed the first time around, the simplify method will simplify this expressions individual operands, and will then call an expr with the simplified operands to see if it's now become simplifiable. This call occurs whether or not any operands were actually simplified, see below.

The 'second' parameter can be used to avoid invoking expensive attempts to simplify an expression more than once - on the first call to do_simplify this parameter will be false, then on the second it's be true, allowing method implementation to save the expensive stuff until all of its operands have certainly been simplified.

Currently simplification does some things that it shouldn't: pointer arithmetic for example. I'm not sure where this can be relocated to though.

Returns
expr2tc A nil expression if no simplifcation could occur, or a new simplified object if it can.

Reimplemented from expr2t.

Member Data Documentation

◆ field_names

std::string cmp_three_way2t::field_names
static
Initial value:
=
{"side_1", "side_2", "", "", ""}

◆ fields

auto cmp_three_way2t::fields
staticconstexpr
Initial value:
= std::make_tuple(
expr2tc side_1
Definition irep2_expr.h:1250
expr2tc side_2
Definition irep2_expr.h:1251
const type2tc type
Type of this expr.
Definition irep2.h:910

◆ side_1

expr2tc cmp_three_way2t::side_1

◆ side_2

expr2tc cmp_three_way2t::side_2

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