Fix proposal for unsoundness issue #13 + test case

This patch addresses the unsoundness issue #13. The idea is to first collect the UB constraints and then add them together with the Phi node predicates. If no Phi nodes exist, add the UB constraints directly as instruction conditions. The recursive parsing at each Phi node can be improved, but we should discuss the proposed solution first.
LLVM has no such constraint that I know of, rather this comes from how 
code gets unwound when being turned into souper.


On 09/05/2014 07:46 PM, Raimondas Sasnauskas wrote:
> In lib/Extractor/KLEEBuilder.cpp:
>
>> @@ -52,6 +52,8 @@ struct ExprBuilder {
>>          InstCondition(klee::ConstantExpr::create(1, Expr::Bool)) {}
>>
>>    std::map<Inst *, ref<Expr> > ExprMap;
>> +  std::map<Inst *, std::vector<ref<Expr> >> PhiPredMap;
>
> It is unclear for me where that constrain comes from that phis of the
> same basic block must have the same number of operands that must be
> consistently selected. I couldn't find any explanation in the LLVM phi
> node ref. Is this a requirement of the SSA form?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/google/souper/pull/37/files#r17206074>.
>