#include "analyze.h"
#include "builtins/builtins.h"
namespace goose::analyze
{
optional< z3::expr > BuildZ3ValFromConstant( const Value& val )
{
auto& c = GetZ3Context();
// TODO: what about very large int types? Can z3 represent them?
if( auto b = FromValue< bool >( val ) )
return c.bool_val( *b );
else if( auto intVal = FromValue< APSInt >( val ) )
return c.int_val( intVal->getExtValue() );
return nullopt;
}
optional< z3::expr > BuildZ3ConstantFromType( const Term& type, const string& name )
{
auto& c = GetZ3Context();
// TODO: what about very large int types? Can z3 represent them?
if( type == GetValueType< bool >() )
return c.bool_const( name.c_str() );
else if( FromValue< builtins::IntegerType >( *ValueFromIRExpr( type ) ) )
return c.int_const( name.c_str() );
return nullopt;
}
template< typename I, typename F >
optional< z3::expr > BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
{
auto operand = BuildZ3ExprFromValue( b, instr.operand() );
if( !operand )
return nullopt;
return func( *operand );
}
template< typename I, typename F >
optional< z3::expr > BuildZ3BinExpr( Builder& b, const I& instr, F&& func )
{
auto lhs = BuildZ3ExprFromValue( b, instr.lhs() );
if( !lhs )
return nullopt;
auto rhs = BuildZ3ExprFromValue( b, instr.rhs() );
if( !rhs )
return nullopt;
return func( *lhs, *rhs );
}
template< typename T >
optional< z3::expr > BuildZ3Op( Builder& b, const T& instr )
{
return nullopt;
}
// TODO: inline cfg. We'll need those functions to take some context with a z3 solver and an optional precondition (indicating which basic block we're in)
// so that they can push assertions directly from the inline CFG (this will have to recurse into the code that builds assertions from a cfg, which doesn't even exist yet)
// Implemented in call.cpp
extern optional< z3::expr > BuildZ3Op( Builder& b, const Call& instr );
optional< z3::expr > BuildZ3Op( Builder& b, const CreateTemporary& instr )
{
b.setVar( instr.cfgId(), instr.index(), instr.value() );
return nullopt;
}
optional< z3::expr > BuildZ3Op( Builder& b, const GetTemporary& instr )
{
const auto* expr = b.retrieveVar( instr.cfgId(), instr.index(), instr.type() );
if( expr )
return *expr;
return BuildZ3ConstantFromType( instr.type(), format( "v{}_{}", instr.cfgId(), instr.index() ) );
}
optional< z3::expr > BuildZ3Op( Builder& b, const GetVar& instr )
{
const auto* expr = b.retrieveVar( instr.cfgId(), instr.index(), instr.type() );
if( expr )
return *expr;
return BuildZ3ConstantFromType( instr.type(), format( "v{}_{}", instr.cfgId(), instr.index() ) );
}
optional< z3::expr > BuildZ3Op( Builder& b, const SetVar& instr )
{
b.setVar( instr.cfgId(), instr.index(), instr.value() );
return nullopt;
}
// TODO: Phi. Construct an expression combining all of the incoming z3 expressions from all the possible incoming blocks.
// TODO: LoadConstStr. Build a z3 str value.
// TODO: bitwise operators. They need to work on bitvecs, so we'll need a param indicating that we want to
// build bitvecs rather than ints, and use it when building the sub expression of something that needs bitvecs.
optional< z3::expr > BuildZ3Op( Builder& b, const Not& instr )
{
// TODO this works only for bools, have to use ~ for bitvecs
return BuildZ3UnaryExpr( b, instr, []( auto&& operand ) { return !operand; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const And& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) -> optional< z3::expr >
{
// TODO handle non bools (use & for bitvecs)
if( !lhs.is_bool() || !rhs.is_bool() )
return nullopt;
return lhs && rhs;
} );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Or& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) -> optional< z3::expr >
{
// TODO handle non bools (use | for bitvecs)
if( !lhs.is_bool() || !rhs.is_bool() )
return nullopt;
return lhs || rhs;
} );
}
// TODO: Xor, Shl, LShr, AShr
optional< z3::expr > BuildZ3Op( Builder& b, const Add& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs + rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Sub& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs - rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Mul& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs * rhs; } );
}
// TODO: UDiv (check how unsigneds need to be handled. I've seen somewhere saying to use bitvectors,
// but the api have unsigned methods for nums? Maybe in current versions of z3 we don't need to use bitvectors for unsigned?)
optional< z3::expr > BuildZ3Op( Builder& b, const SDiv& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs / rhs; } );
}
// TODO: URem
optional< z3::expr > BuildZ3Op( Builder& b, const SRem& instr )
{
// TODO: need to use a different function for bitvectors
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return z3::rem( lhs, rhs ); } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Eq& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs == rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Neq& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs != rhs; } );
}
// TODO: UGT, UGE, ULT, ULE
optional< z3::expr > BuildZ3Op( Builder& b, const SGT& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs > rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const SGE& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs >= rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const SLT& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs < rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const SLE& instr )
{
return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs ) { return lhs <= rhs; } );
}
optional< z3::expr > BuildZ3Op( Builder& b, const Assert& instr )
{
auto cond = BuildZ3ExprFromValue( b, instr.cond() );
if( cond )
b.addAssertion( *cond, instr.cond().locationId() );
return nullopt;
}
optional< z3::expr > BuildZ3Op( Builder& b, const Placeholder& instr )
{
const auto* expr = b.retrievePlaceholder( instr.name() );
if( expr )
return *expr;
return BuildZ3ConstantFromType( instr.type(), format( "p{}", instr.name() ) );
}
optional< z3::expr > BuildZ3Op( Builder& b, const llr::Instruction& instr )
{
return visit( [&]( auto&& e )
{
return BuildZ3Op( b, e );
}, instr.content() );
}
optional< z3::expr > BuildZ3ExprFromValue( Builder& b, const Value& val )
{
if( val.isPoison() )
return nullopt;
if( val.isConstant() )
return BuildZ3ValFromConstant( val );
if( auto expr = BuildZ3Op( b, *val.llr() ) )
return expr;
return BuildZ3ConstantFromType( val.type(), format( "val{}", b.newUniqueId() ) );
}
}