Inquire about the output understanding and configuration of jpf-symbc

[BEbillionaireUSD]

Hi, thanks for this wonderful tool! I have several questions regarding its usage.

Z3str configuration

First, in jpf.properties, there is string configuration: strings.z3str=/home/miroslav/Research/jpf/Z3-str/Z3-str.py However, I don't know where to download the corresponding Z3 source code. This causes some confusing results: When I set symbolic.string_dp=z3str2 running PassCheck01.jpf, it reports:

$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$
Calling Z3str2

java.io.IOException: Cannot run program "./lib/z3": error=2, No such file or directory

but when I set symbolic.string_dp=z3str, it works normally. All the files in ./lib are exactly the same as this repo.

Results' meanings

Secondly, I'm a bit confused regarding the meaning of the outputs. I would be truly grateful if you could kindly provide some references to assist me in understanding the outputs. For example, I run PassCheck01.jpf and it outputs:

...
string analysis: SPC # = 0
NPC constraint # = 10
CONST_8 >= Length_0_ &&
CharAt(CONST_7)_8_ == CONST_100 &&
CharAt(CONST_6)_7_ == CONST_114 &&
CharAt(CONST_5)_6_ == CONST_48 &&
CharAt(CONST_4)_5_ == CONST_119 &&
CharAt(CONST_3)_4_ == CONST_36 &&
CharAt(CONST_2)_3_ == CONST_36 &&
CharAt(CONST_1)_2_ == CONST_97 &&
CharAt(CONST_0)_1_ == CONST_80 &&
Length_0_ == CONST_8
numeric PC: constraint # = 10
CONST_8 < Length_0_ &&
CharAt(CONST_7)_8_ == CONST_100 &&
CharAt(CONST_6)_7_ == CONST_114 &&
CharAt(CONST_5)_6_ == CONST_48 &&
CharAt(CONST_4)_5_ == CONST_119 &&
CharAt(CONST_3)_4_ == CONST_36 &&
CharAt(CONST_2)_3_ == CONST_36 &&
CharAt(CONST_1)_2_ == CONST_97 &&
CharAt(CONST_0)_1_ == CONST_80 &&
Length_0_ == CONST_8 -> false

### PCs: total:36 sat:27 unsat:9

Referring to the source code, I can understand that in CONST_8 < Length_0_, CONST_8 indicates integer 8 and Length_0_ is the length of the inputted string; The CONST_<NUM> at the right of == indicates the ascii code of the corresponding string Pa$$W0rd. However, I want to understand the principle behind such representations, like when can I regard CONST_<NUM> as an integer yet when it is an ASCII code?

Alternatively, I wonder if it's possible to obtain a more readable file concerning the symbolic execution results. For example, I used jDart, and it produces a tree-like json output, such as:

[INFO] -('d' < 3.141)
  |-[+]-(('d' >= -1.0) && ('d' <= 1.0))
  |      |-[+]-!'java.lang.Double.isNaN'('asin'('d'))
  |      |      |-[+]_/OK: [ return:='asin'('d'),  ]
  |      |      +-[-]_/DONT_KNOW
  |      +-[-]_/OK: [  ]
  +-[-]_/OK: [  ]

Constraint Settings

Third, I'm wondering how to set the constraints. For example, if I want to limit the length of the input string to eight, then how should I set this constraint in .jpf (or somewhere else)? For example, in the example Arraysbis, we can see the function:

public static int counter_bis(int i, int[] arr) {
        int a = arr[i];
        return 1/(a+1);
    }

I want to set a constraint for i and arr as 0 <= i < arr.length.

Thank you very much for your time and assistance.

[sohah]

Hi,

Thank you for your interest in SPF. Please find the answers to your questions below:

1. To use string solving please use "symbolic.string_dp=z3str3" in your .jpf configuration. Please know that currently SPF does not have a complete support for symbolic string, this is under development. If you want to use the latest symbolic string support please use the sv-comp branch.

2. I haven't looked into the example that you've referred to, but I can see there is some usage of charAt. In essense, SPF, because it works on the bytecode, a char is treated as an unsigned integer. So, my guess this is what is happening here.

3. I do not think SPF has support for this feature, i.e., printing the symbolic tree. @yannicnoller , can you please confirm? have you seen this feature before, perhaps in JPF which we can turn on?

4. I do not think you can do this using the configuration. You can impose assumptions by inserting assumptions by using the assume method within the Debug.java, or the Verifier.java. Not that, you can find the maximum size of string here. You can expose it to the jpf configuration file if this is something that you want to be able to change.

[BEbillionaireUSD]

Many thanks for your reply! My questions are basically solved. For 3, if SPF also maintains a symbolic tree, could you please tell me which class defines this tree? Even though there is currently no such printing feature, I can still make some extensions to it.

I have another question: How can an additional file be set up as part of the configuration? In examples/Test.up, there is

domain{
 x_1_SYMINT:0,1;
 };
 usageProfile{
  x_1_SYMINT>=0:100/100;
 };

And in TestPaths.jpf, there is:

symbolic.reliability.problemSettings=${jpf-symbc}/src/examples/Test.up

I am curious about the purpose of Test.up and what norms I should follow to write such a file. Perhaps it comes from another repository? Can you provide me with some reference links?

Plus, how can I turn to the symcrete mode with specific input values?