confusing API for state.addConstraint

Question

Hi, I'm modifying KLEE to enable better string support with dedicated solvers. Inside SpecialFunctionHandler.cpp, I have written various handlers for "hijacking" string functions. In the following code sample I (artificially) ask if some string can satisfy 3 demands:

[1] AB_q_name == "TT8G" [2] strchr(AB_q_name, "8") == 2 [3] strchr(AB_q_name, "T") == 3

And I expect the answer to be no. However, when using this code, KLEE hits the assert. If I remove the comments and add the constraint everything works fine. What am I doing wrong? Thanks in advance!!

ref<Expr> myVar = StrVarExpr::create(AB_q_name);
ref<Expr> AB_q_name_eq_TT8G = 
    StrEqExpr::create(
        myVar,
        StrConstExpr::create("TT8G"));

state.addConstraint(AB_q_name_eq_TT8G);

ref<Expr> RUNNING_EXAMPLE =
//AndExpr::create(AB_q_name_eq_TT8G,
    AndExpr::create(
        EqExpr::create(
            StrFirstIdxOfExpr::create(
                myVar,
                StrConstExpr::create("8")),
            ConstantExpr::create(2,Expr::Int32)),
        EqExpr::create(
            StrFirstIdxOfExpr::create(
                 myVar,
                StrConstExpr::create("T")),
            ConstantExpr::create(3,Expr::Int32)))/*)*/;


success = executor.solver->mayBeTrue(state,RUNNING_EXAMPLE,result);
if (result)
{
    klee_error("THIS SHOULD NOT BE PRINTED !!!");
    assert(0);
}

该提问来源于开源项目：klee/klee

Answer 1

you are right, I'm attaching the missing implementation for StrFirstIdxOfExpr, and hopefully it will help. But before that, just to be sure, if I have two ref Expr e1 and e2, the following are equivalent (for the solver result) (right?)

[-] state.addConstraint(e1); executor.solver->mayBeTrue(state,e2,result); [-] executor.solver->mayBeTrue(state,AndExpr::create(e1,e2),result);

First of all, here is the relevant code from Z3Builder.cpp:

Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) {
// some cases before that ... and then my new cases:
case Expr::Str_FirstIdxOf:
{
    int irrelevant_width=0;

    StrFirstIdxOfExpr *sfioe = (StrFirstIdxOfExpr *) e.get();

    /*******************************************************************/
    /* Build a Z3ASTHandle from the name of the (string-sort) variable */
    /*******************************************************************/
    Z3ASTHandle result = Z3ASTHandle(
        Z3_mk_seq_index(
            ctx,
            constructActual(sfioe->haystack,&irrelevant_width),
            constructActual(sfioe->needle,  &irrelevant_width),
            Z3_mk_int(ctx,0,Z3_mk_int_sort(ctx))),
        ctx);

return Z3ASTHandle(ConvertInt2BitVec32(result),ctx);

And here is the class definition from Expr.h:

/*********************/
/* StrFirstIdxOfExpr */
/*********************/
class StrFirstIdxOfExpr : public Expr {
public:
    ref<Expr> haystack;
    ref<Expr> needle;

    StrFirstIdxOfExpr(
        const ref<Expr> &in_haystack,
        const ref<Expr> &in_needle) :
        haystack(in_haystack),
        needle(in_needle)
        {}
public:
    static ref<Expr> create(
        const ref<Expr> &in_haystack,
        const ref<Expr> &in_needle)
    {
        return StrFirstIdxOfExpr::alloc(in_haystack,in_needle);
    }
    static ref<Expr> alloc(const ref<Expr> &in_haystack,const ref<Expr> &in_needle)
    {
        ref<Expr> res(new StrFirstIdxOfExpr(in_haystack,in_needle));
        res->computeHash();
        return res;
    }
public:
    virtual Kind      getKind()                 const {return   Expr::Str_FirstIdxOf;}  
    virtual Width     getWidth()                const {return   32;}    
    virtual unsigned  getNumKids()              const {return    2;}    
    virtual ref<Expr> getKid(unsigned int i)    const
    {
        if(i==0){return haystack;}
        if(i==1){return needle;}
        return 0;
    }
    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {ref<Expr> moish; return moish;}
    static bool classof(const Expr *E) { return E->getKind() == Expr::Str_FirstIdxOf; }
    static bool classof(const ConstantExpr *) { return false; } 
};