JPF summary generation test1

Simple Example

A.java

public int sub(int a, int b)
{
    return a - b;
}
public int testRefactored (int refs, int flags) {
    if (flags != 0) 
    	return flags * sub(flags, flags*3);
    else if (refs != 0)
    	return refs;
    return 10;       
}

(or ( and  (distinct  flags_2_SYMINT 0)  (=  RETURN ( * (flags_2_SYMINT- (flags_2_SYMINT * 3)) flags_2_SYMINT)) )
 ( and  (distinct  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN refs_1_SYMINT) )
 ( and  (=  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN 10) )
)

JPF is smart enough to understand sub() method to give the correct constraints

RETURN ( * (flags_2_SYMINT- (flags_2_SYMINT * 3)

B.java

public int sub(int a, int b)
{
    return a - b;
}
public int testRefactored (int refs, int flags) {
    if (flags != 0) 
    	return flags;
    else if (refs != 0)
    	return refs;
    return 10;       
}

(or ( and  (distinct  flags_2_SYMINT 0)  (=  RETURN flags_2_SYMINT) )
 ( and  (distinct  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN refs_1_SYMINT) )
 ( and  (=  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN 10) )
)

More complex

With this example:

public int sub(int a, int b)
{   
	if (a > b)
		return (a - b);
	else
	    return (10*a + b);
}
public int test (int refs, int flags) {		
	if (flags != 0) 
		return flags * sub(flags, flags*3); << This line causes an issue
	else if (refs != 0)
	   	return refs;
	return 10;       
}

JPF works fine to generate the correct summary:

testCase=test(-100,-100);pc=( >  flags_2_SYMINT[-100] ( *  flags_2_SYMINT[-100] CONST_3)) && ( !=  flags_2_SYMINT[-100] CONST_0);effects=RETURN==( *  (flags_2_SYMINT[-100] - (flags_2_SYMINT[-100] * CONST_3)) flags_2_SYMINT[-100]);solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none
testCase=test(1,1);pc=( <=  flags_2_SYMINT[1] ( *  flags_2_SYMINT[1] CONST_3)) && ( !=  flags_2_SYMINT[1] CONST_0);effects=RETURN==( *  ((flags_2_SYMINT[1] * CONST_3) + (flags_2_SYMINT[1] * CONST_10)) flags_2_SYMINT[1]);solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none
testCase=test(-100,-100);pc=( !=  refs_1_SYMINT[-100] CONST_0) && ( ==  flags_2_SYMINT[0] CONST_0);effects=RETURN==refs_1_SYMINT[-100];solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none
testCase=test(0,0);pc=( ==  refs_1_SYMINT[0] CONST_0) && ( ==  flags_2_SYMINT[0] CONST_0);effects=RETURN==10;solverCalls=2;statementsExecuted=[];positionsExecuted=[];constraints=none

Only to get something's wrong with the listener:

(or  ( and  (>  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * (flags_2_SYMINT- (flags_2_SYMINT * 3)) flags_2_SYMINT)) )
 ( and  (<=  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * ((flags_2_SYMINT * 3)+ (flags_2_SYMINT * 10)) flags_2_SYMINT)) )
 ( and  (distinct  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN refs_1_SYMINT) )
 ( and  (=  refs_1_SYMINT 0)  (=  flags_2_SYMINT 0)   (=  RETURN 10) )
)
 ( and  (<=  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * ((flags_2_SYMINT * 3)+ (flags_2_SYMINT * 10)) flags_...
                                                                                                    ^^^^^^^^^^^^^^
(error "Invalid beginning of an identifer: expected either 'as' or '_' here")
Executing the script...
 ( and  (<=  flags_2_SYMINT ( * flags_2_SYMINT 3))  (distinct  flags_2_SYMINT 0)   (=  RETURN ( * ((flags_2_SYMINT * 3)+ (flags_2_SYMINT * 10)) flags_...
                                                                                                    ^^^^^^^^^^^^^^
(error "Invalid beginning of an identifer: expected either 'as' or '_' here")

sub(flags, flags*3)

I think the generated code should have been (* flags_2_SYMINT 3).

Research questions

• How does the listener work to transform summary into S-expression code
• How do I modify the listener to resolve this issue?