hal::SMT::ConstantPropagation Namespace Reference

Functions
std::vector< BooleanFunction::Value >	And (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Or (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Not (const std::vector< BooleanFunction::Value > &p)
std::vector< BooleanFunction::Value >	Xor (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Add (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Sub (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Mul (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Eq (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Udiv (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Urem (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Sdiv (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Srem (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Shl (const std::vector< BooleanFunction::Value > &p0, const u16 p1)
std::vector< BooleanFunction::Value >	Lshr (const std::vector< BooleanFunction::Value > &p0, const u16 p1)
std::vector< BooleanFunction::Value >	Ashr (const std::vector< BooleanFunction::Value > &p0, const u16 p1)
std::vector< BooleanFunction::Value >	Rol (const std::vector< BooleanFunction::Value > &p0, const u16 p1)
std::vector< BooleanFunction::Value >	Ror (const std::vector< BooleanFunction::Value > &p0, const u16 p1)
std::vector< BooleanFunction::Value >	Sle (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Slt (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Ule (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Ult (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
std::vector< BooleanFunction::Value >	Ite (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1, const std::vector< BooleanFunction::Value > &p2)
Result< std::vector< BooleanFunction::Value > >	fold (const BooleanFunction::Node &node, std::vector< std::vector< BooleanFunction::Value >> &values, const std::vector< u16 > &indices)

Detailed Description

Helper functions for the division and remainder operations below. They operate on little endian vectors of defined values, i.e. ZERO or ONE only, of equal length.

Function Documentation

Add()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Add	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant ADD operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 148 of file symbolic_execution.cpp.

References hal::carry, and hal::BooleanFunction::to_u64().

Referenced by hal::module_identification::check_absolute(), hal::module_identification::check_constant_multiplication(), hal::module_identification::check_constant_multiplication_offset(), hal::module_identification::check_sliced_add(), and fold().

And()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::And	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant AND operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 33 of file symbolic_execution.cpp.

Referenced by hal::Simplification::abc_simplification(), and fold().

Ashr()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Ashr	(	const std::vector< BooleanFunction::Value > &	p0,
		const u16	p1
	)

Helper function to simplify a constant ASHR operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 552 of file symbolic_execution.cpp.

Referenced by fold().

Eq()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Eq	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant EQ operation.

A single undefined bit hides whether the two values are equal, unless some other bit already tells them apart.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 375 of file symbolic_execution.cpp.

Referenced by hal::module_identification::check_equal(), hal::module_identification::check_value_check(), and fold().

fold()

Result<std::vector<BooleanFunction::Value> > hal::SMT::ConstantPropagation::fold	(	const BooleanFunction::Node &	node,
		std::vector< std::vector< BooleanFunction::Value >> &	values,
		const std::vector< u16 > &	indices
	)

Applies a node to operands that have already been folded to constant values.

Shared by SymbolicExecution::constant_propagation(), which wraps the result back into a Boolean function, and by the constant evaluation in SymbolicExecution::evaluate(), which keeps working on plain values.

Parameters

[in]	node	- The node to apply.
[in,out]	values	- The constant operands, some of the cases modify them in place.
[in]	indices	- The index operands, in the order in which they appear.

Returns

Ok() and the resulting value on success, Err() otherwise.

Definition at line 800 of file symbolic_execution.cpp.

References hal::BooleanFunction::NodeType::Add, Add(), hal::BooleanFunction::NodeType::And, And(), hal::BooleanFunction::NodeType::Ashr, Ashr(), hal::BooleanFunction::NodeType::Concat, hal::BooleanFunction::NodeType::Eq, Eq(), ERR, hal::BooleanFunction::NodeType::Ite, Ite(), hal::BooleanFunction::NodeType::Lshr, Lshr(), hal::BooleanFunction::NodeType::Mul, Mul(), hal::BooleanFunction::NodeType::Not, Not(), OK, hal::BooleanFunction::NodeType::Or, Or(), hal::BooleanFunction::NodeType::Rol, Rol(), hal::BooleanFunction::NodeType::Ror, Ror(), hal::BooleanFunction::NodeType::Sdiv, Sdiv(), hal::BooleanFunction::NodeType::Sext, hal::BooleanFunction::NodeType::Shl, Shl(), hal::BooleanFunction::Node::size, hal::BooleanFunction::NodeType::Sle, Sle(), hal::BooleanFunction::NodeType::Slice, hal::BooleanFunction::NodeType::Slt, Slt(), hal::BooleanFunction::NodeType::Srem, Srem(), hal::BooleanFunction::NodeType::Sub, Sub(), hal::BooleanFunction::Node::type, hal::BooleanFunction::NodeType::Udiv, Udiv(), hal::BooleanFunction::NodeType::Ule, Ule(), hal::BooleanFunction::NodeType::Ult, Ult(), UNUSED, hal::BooleanFunction::NodeType::Urem, Urem(), hal::BooleanFunction::NodeType::Xor, Xor(), and hal::BooleanFunction::NodeType::Zext.

Ite()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Ite	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1,
		const std::vector< BooleanFunction::Value > &	p2
	)

Helper function to simplify a constant ITE operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.
[in]	p2	- Boolean function parameter 2.

Returns

Boolean function with a simplified constant value.

Definition at line 772 of file symbolic_execution.cpp.

Referenced by hal::module_identification::check_absolute(), and fold().

Lshr()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Lshr	(	const std::vector< BooleanFunction::Value > &	p0,
		const u16	p1
	)

Helper function to simplify a constant LSHR operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 526 of file symbolic_execution.cpp.

Referenced by fold().

Mul()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Mul	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant MUL operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 234 of file symbolic_execution.cpp.

References hal::carry.

Referenced by fold().

Not()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Not

(

const std::vector< BooleanFunction::Value > &

p

)

Helper function to simplify a constant NOT operation.

Parameters

[in]

p

- Boolean function parameter.

Returns

Boolean function with a simplified constant value.

Definition at line 90 of file symbolic_execution.cpp.

Referenced by hal::Simplification::abc_simplification(), hal::module_identification::check_absolute(), hal::module_identification::check_value_check(), and fold().

Or()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Or	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant OR operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 62 of file symbolic_execution.cpp.

Referenced by hal::Simplification::abc_simplification(), and fold().

Rol()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Rol	(	const std::vector< BooleanFunction::Value > &	p0,
		const u16	p1
	)

Helper function to simplify a constant ROL operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 580 of file symbolic_execution.cpp.

Referenced by fold().

Ror()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Ror	(	const std::vector< BooleanFunction::Value > &	p0,
		const u16	p1
	)

Helper function to simplify a constant ROR operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 608 of file symbolic_execution.cpp.

Referenced by fold().

Sdiv()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Sdiv	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant SDIV operation.

Signed division truncates towards zero, following the SMT-LIB definition of bvsdiv.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 436 of file symbolic_execution.cpp.

Referenced by fold().

Shl()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Shl	(	const std::vector< BooleanFunction::Value > &	p0,
		const u16	p1
	)

Helper function to simplify a constant SHL operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 500 of file symbolic_execution.cpp.

Referenced by fold().

Sle()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Sle	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant SLE operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 635 of file symbolic_execution.cpp.

References hal::carry.

Referenced by fold().

Slt()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Slt	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant SLT operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 675 of file symbolic_execution.cpp.

References hal::carry.

Referenced by fold().

Srem()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Srem	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant SREM operation.

The sign of a signed remainder follows the dividend, following the SMT-LIB definition of bvsrem.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 469 of file symbolic_execution.cpp.

Referenced by fold().

Sub()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Sub	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant SUB operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 191 of file symbolic_execution.cpp.

References hal::carry, and hal::BooleanFunction::to_u64().

Referenced by fold().

Udiv()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Udiv	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant UDIV operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 400 of file symbolic_execution.cpp.

Referenced by fold().

Ule()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Ule	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant ULE operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 713 of file symbolic_execution.cpp.

Referenced by fold().

Ult()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Ult	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant ULT operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 742 of file symbolic_execution.cpp.

Referenced by fold().

Urem()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Urem	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant UREM operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 417 of file symbolic_execution.cpp.

Referenced by fold().

Xor()

std::vector<BooleanFunction::Value> hal::SMT::ConstantPropagation::Xor	(	const std::vector< BooleanFunction::Value > &	p0,
		const std::vector< BooleanFunction::Value > &	p1
	)

Helper function to simplify a constant XOR operation.

Parameters

[in]	p0	- Boolean function parameter 0.
[in]	p1	- Boolean function parameter 1.

Returns

Boolean function with a simplified constant value.

Definition at line 119 of file symbolic_execution.cpp.

Referenced by hal::Simplification::abc_simplification(), and fold().