62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
}
// 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.
|
|
|
|
|
|
|
|
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
}
// 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.index(), instr.value() );
return nullopt;
}
optional< z3::expr > BuildZ3Op( Builder& b, const GetTemporary& instr )
{
const auto* expr = b.retrieveVar( instr.index(), instr.type() );
if( expr )
return *expr;
return BuildZ3ConstantFromType( instr.type(), format( "v{}", instr.index() ) );
}
optional< z3::expr > BuildZ3Op( Builder& b, const GetVar& instr )
{
const auto* expr = b.retrieveVar( instr.index(), instr.type() );
if( expr )
return *expr;
return BuildZ3ConstantFromType( instr.type(), format( "v{}", instr.index() ) );
}
optional< z3::expr > BuildZ3Op( Builder& b, const SetVar& instr )
{
b.setVar( 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.
|