testcases in S2E

[Mukta Debnath]

Hi Mr. Vitaly,

Is there any way to see the testcases generated by s2e? How do I know the total number of test cases generated by s2e on the whole or which explored new paths?

Is there a way to specify a timeout on how long I want s2e to run?

[Vitaly Chipounov]

Hi,

On Thu, Dec 31, 2020 at 12:49 PM Mukta Debnath
<muktapear...@gmail.com> wrote:
>
> Is there any way to see the testcases generated by s2e? How do I know the total number of test cases generated by s2e on the whole or which explored new paths?

You can see them in s2e-last/debug.txt, grep for TestCaseGenerator.
You can also get them from execution traces in json format using the
"s2e execution_trace" command. See [1,2] for details. You can extract
the total number of paths from the execution trace.

>
> Is there a way to specify a timeout on how long I want s2e to run?
>

You can use "s2e run --timeout" for that. Alternatively, you can add a
timer callback to s2e-config.lua using the LuaCoreEvents plugin [3,4]
to exit S2E.

Vitaly

[1] http://s2e.systems/docs/Howtos/ExecutionTracers.html
[2] http://s2e.systems/docs/Plugins/Tracers/ExecutionTracer.html?highlight=testcasegenerator#testcasegenerator
[3] https://github.com/S2E/s2e-env/blob/master/s2e_env/templates/s2e-config.lua#L417
[4] https://github.com/S2E/s2e/blob/master/libs2eplugins/src/s2e/Plugins/Lua/LuaCoreEvents.cpp#L70

[Mukta Debnath]

Hi Mr. Vitaly,

I need to know the branch coverage information for my designs. Is there is any way to get the branch coverage information using S2E? I can get the execution trace but is there any option to view the concrete values of the generated test cases? If I could get those test cases, I can measure the branch coverage using any other coverage measuring tool.

[Vitaly Chipounov]

Hi,

Test cases are recorded in the execution trace, you can extract them
using "s2e execution_trace", as explained in the earlier reply.
Note that if you use symbolic files (with @@ marker in s2e
new_project), TestcaseGenerator also produces concrete test case files
when states terminate and stores them in the s2e-last folder. It may
be easier to use them than trying to parse the json from the trace.

Vitaly

> --
> --
> You received this message because you are a member of the S2E Developer Forum.
> To post to this group, send email to s2e...@googlegroups.com
> To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
> For more options, visit this group at http://groups.google.com/group/s2e-dev
>
> ---
> You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/5cf98818-2238-4424-8c08-4ab9c3eb213en%40googlegroups.com.

[Mukta Debnath]

Thank you for response.

Can you give me a brief explanation of what the states in S2E mean? How long does S2E takes to terminate the states in S2E? I am running my SystemC designs with S2E,

I get the following message:

20 [State 0] LinuxMonitor: mprotect pid=0x4f2 start=0x563531aa2000 size=0xfff prot=0x0
20 [State 0] LinuxMonitor: mprotect pid=0x4f2 start=0x563531ae2000 size=0xfff prot=0x0
20 [State 0] LinuxMonitor: mprotect pid=0x4f2 start=0x563531b22000 size=0xfff prot=0x0
20 [State 0] Forking state 0 at pc = 0x7f7995686634 at pagedir = 0xdbb4000
    state 0
    state 1
22 [State 0] Switching from state 0 to state 1
22 [State 1] Forking state 1 at pc = 0x7f7995686634 at pagedir = 0xdbb4000
    state 1
    state 2
28 [State 1] Switching from state 1 to state 0
33 [State 0] Switching from state 0 to state 1
43 [State 1] Switching from state 1 to state 0
48 [State 0] Switching from state 0 to state 1
53 [State 1] Switching from state 1 to state 0
63 [State 0] Switching from state 0 to state 1
68 [State 1] Switching from state 1 to state 0
79 [State 0] Switching from state 0 to state 1
109 [State 1] Switching from state 1 to state 0
114 [State 0] Switching from state 0 to state 1
135 [State 1] Switching from state 1 to state 0
145 [State 0] Switching from state 0 to state 1
155 [State 1] Switching from state 1 to state 0
181 [State 0] Switching from state 0 to state 1
............................................................................

1220 [State 0] Switching from state 0 to state 1
1225 [State 1] Switching from state 1 to state 0
1230 [State 0] Switching from state 0 to state 1
1236 [State 1] Switching from state 1 to state 0
1246 [State 0] Switching from state 0 to state 1
...............................

I forcibly end the execution.

I am attaching my debug.txt with the e-mail.

I am running the following command to make the file input argument of my design :

s2e new_project --image debian-9.2.1-x86_64 -n bubble_cwom /home/mukta/Mukta/S3CBench_perl/bubble_sort/bubble.exe -infile @@ -goldfile /home/mukta/Mukta/S3CBench_perl/bubble_sort/sort_output_golden.txt

and I am not making any change in the bootstrap.sh.

Please suggest.

[Vitaly Chipounov]

Hi,

A state is essentially an execution path. S2E forks one new state/path
when a branch depends on symbolic data. You seem to have two of them
(0 and 1).
S2E terminates a path/state as soon as the guest calls the
s2e_kill_state() API (see the s2e.h header). This API can be called
either directly by the program or indirectly after the program
terminates and control is passed back to bootstrap.sh ("s2ecmd kill"
command). If this is not called for any reason, the state/path will
run forever. If your program terminates normally, you don't have to
worry about calling it yourself, bootstrap.sh will take care of it for
you.

When there is more than one state, S2E periodically switches between
them. In your case, they seem to take a while to run. It can be due to
many reasons, a common one being that the program is stuck waiting for
user input. S2E runs in unattended mode, you must make sure that all
the required input is provided appropriately, e.g., by redirecting
stdin. This may sometimes require manually tweaking bootstrap.sh. You
can also check serial.txt and enable graphics output in launch-s2e.sh
to see if the guest OS outputs anything helpful.

Note that just attaching debug.txt is not always helpful. Please
export the project together with the content of s2e-last (s2e
export_project --export-results).

Vitaly

On Mon, Jan 4, 2021 at 2:02 PM Mukta Debnath

> To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/8f32cd7a-4628-4f43-b3f1-c3cdd736422fn%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

Thank you for your response. It helped me to find the concrete values for the test cases.

Regards,

Mukta

[Mukta Debnath]

Hello Mr. Vitaly,

I have created the attached project and have used the symbolic file marker (@@) for test case generation. I can see the testcases are generated in the s2e-last folder. I am not able to  view the content of the testcase files. Are the testcases generated by S2E human-readable?

Can you please check my exported project shared via Google Drive and let me know.

https://drive.google.com/file/d/1ssVwRJ9XOiRt8EFKcMBmswc6LLdOYLWQ/view?usp=sharing

Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

The test case files contain binary data, they are not human-readable in general. For example, if you give a jpeg image reader a symbolic file, at the end of the execution, the test case will contain some image date that satisfies the path constraints when the program terminated.

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/97298a85-c97b-4f36-adee-c21781797403n%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

Thank you for the explanation. But, my question is, if I do not get the human/program readable concrete test case files, how do I validate my design executable? If I want to used these test cases generated by S2E as input seeds to my fuzz engine, what is the way out, as the testcases generated will not be recognized by the fuzzer?

Another query is, if I do not use symbolic file marker, rather I use an initial seed, in that case the testcases files are not produced. Then how do I get the testcases generated files? Do I need to get it manually from the ExecutionTracer.jason file? Will that be feasible?

Is there any other usage of "tbcoverage-0.json" file rather than generating the coverage info by S2E?

Thanks and Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

On 1/24/21 7:27 AM, Mukta Debnath wrote:

Thank you for the explanation. But, my question is, if I do not get the human/program readable concrete test case files, how do I validate my design executable? If I want to used these test cases generated by S2E as input seeds to my fuzz engine, what is the way out, as the testcases generated will not be recognized by the fuzzer?

Testcases generated by S2E are directly usable by the program.
If your program expects input in a file and you made that file symbolic, S2E will generate a concrete file that you can directly use as an input to the program to validate it.
Whether that test case contains human-readable or binary data depends entirely on the program that you test.

So if you create a new project like this: s2e new_project my_program @@

You can then validate the test case like that: ./my_program test_case_file

Another query is, if I do not use symbolic file marker, rather I use an initial seed, in that case the testcases files are not produced. Then how do I get the testcases generated files? Do I need to get it manually from the ExecutionTracer.jason file? Will that be feasible?

Test cases will be produced as well. Please refer to [1] for details.
You need to create your project like this: s2e new_project my_program /path/to/seed/file/on/the/host
s2e_env will detect any argument that looks like a file path and will automatically use it as a seed.
You will need to edit the .symranges file to specify which part of the file to make symbolic.

Is there any other usage of "tbcoverage-0.json" file rather than generating the coverage info by S2E?

Currently, no.

Vitaly

[1] http://s2e.systems/docs/Tutorials/BasicLinuxSymbex/s2e.so.html?highlight=seed

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/0b2a4f4b-4617-497f-b15a-aeaf8c2b7c4bn%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

Thank you for the explanations. Can you please guide me on how to write .symranges file. I have no clue on how to specify offset-size pair to make symbolic.

I have attached my exported project with the mail.

Thanks and Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

The symranges file contains an example:

# This file specifies offset-size pairs to make symbolic
# 0-0

So if you want to make the 10th and 11th bytes symbolic, write this:
10-2

You can have multiple lines with different ranges.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/7ea38537-6e92-42e3-9aa0-81ae52ed72a5n%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

Thanks a lot for the reply. I have almost reached my results with your help on using S2E.

I have used the symranges file as mentioned by you in the project I have attached in previous mail, that finds the sum of 5 numbers where the inputs are read from a file, where the file contents for example is as follows:

11 22 33 44 55

So I want to make all these five numbers symbolic which I specified in the symranges file as follows:

0-14

and it worked fine. I got testcases with different values for the 5 numbers.

Now I am trying to run bubble sort program that reads the input data from a file and the file content for example is as given below:

12

10

45

...

Now I want to make the content of each line of the the file, i.e all the numbers as symbolic, So, how do I specify in the symranges file? I tried as follows:

0-2

0-2

0-2

.... and so on. This is only taking the data in the first line of the file as symbolic and generating the test cases but not working for the following lines. Can you tell me where I' am going wrong? I am a bit unsure on how to specify the bytes of a file.

Thanks and Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

On 1/31/21 4:07 AM, Mukta Debnath wrote:

Now I want to make the content of each line of the the file, i.e all the numbers as symbolic, So, how do I specify in the symranges file? I tried as follows:

0-2

0-2

0-2

This will make the first 2 bytes of the file symbolic, 3 times. The offset in the pair is relative to the first byte of the file.

.... and so on. This is only taking the data in the first line of the file as symbolic and generating the test cases but not working for the following lines. Can you tell me where I' am going wrong? I am a bit unsure on how to specify the bytes of a file.

There are two ways:
1. Just keep your original symranges. Your "11 22 33 44 55" is now "11\n22\n33\n44\n55", so nothing really changes.
2. Add one range for each line, assuming your line has 2 characters and don't make the new line character symbolic.
0-2
3-2
6-2
etc.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/89bbec09-ca73-4d52-855f-67164e15bb5cn%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

Thanks a lot for the response. It solved my problems. I am now trying to explore the --use-seeds feature of S2E.  I am using the following command to create the project with seed files feature enabled. Is this the correct way?

"s2e new_project  --use-seeds  --image  <image_name>  <-option> @@" .

My program takes a file as input argument with the option "-infile" which I am placing in <-option> and then providing the symbolic input marker @@.

So by the above technique does S2E considers the seeds I am putting in the seeds folder created as symbolic? Please share me the required knowledge on how to use this --use-seeds features as I want to use the seeds that I am getting from a fuzzer here.

Thanks and Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

A detailed explanation of how seed files work can be found here in the SeedSearcher section: http://s2e.systems/docs/Tutorials/PoV/index.html?highlight=seeds

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/5b8a50dd-554f-45bf-832b-00df77e0d47dn%40googlegroups.com.

[Mukta Debnath]

Thank you for your response.

[Vitaly Chipounov]

You're welcome!

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/562e24c2-1d87-4187-ba24-ef89d322882cn%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

Can you please tell me why I get such error while using the --use-seeds flag of S2E?

I have attached the screen capture of the error.

For every seed in the seed folder, a symranges file will be created?

Thanks and Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

You can use a symranges file to specify which part of the file to make symbolic. You must create it yourself.
This file is optional, the error is benign.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/fc7b9376-0ae7-40cd-ba6b-3cf051def01fn%40googlegroups.com.

[Mukta Debnath]

Thank you for the response.

[Mukta Debnath]

Hello Mr. Vitaly,

Is there any way to restrict the test generation in S2E? Since S2E is generating the test cases in a Brute Force manner, trying all possible inputs, it is generating many redundant test cases. Is there any way to avoid this? Is there any plugin available for this?

Thanks and Regards,

Mukta Debnath

[Vitaly Chipounov]

Hi,

Could you please elaborate what you mean by brute force and redundant test cases? In principle, S2E generates one test case per execution path, i.e., one input per path. Brute forcing may occasionally happen with symbolic pointers, if the fork on symbolic address is enabled [1]. In this case, you may have multiple inputs for the same path.

Vitaly

[1] https://github.com/S2E/s2e/blob/master/libs2ecore/src/S2EExecutor.cpp#L111

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/f418e741-95d9-4d1c-b331-41b999d39698n%40googlegroups.com.

[Mukta Debnath]

Hello Mr. Vitaly,

I may be wrong. I was using S2E in a design written in SystemC program where the input data that I want to make symbolic are floating point data.  In that case S2E generating testcases that are redundant for the design, example the testcases contains symbol like "+, -, /" etc which are not desired. Somehow the testcases are generated in a Brute Force manner by S2E without understanding the semantic of the program. I will try using S2E on other designs too where input data to be made symbolic are floating point numbers and check.

Thanks and Regards,

Mukta Debnath

[vit...@cyberhaven.com]

Ah right, forgot about it. It does not fully support symbolic fp, so like pointers, it will fork many possibly redundant cases. You will have to add fp support to klee to solve this.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/7e686686-6fc5-4ea0-98e8-f32dc21ecb54n%40googlegroups.com.

[Mukta Debnath]

Alright. Thank you for your response.

Regards,

Mukta Debnath

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/eae48c32-7894-4fa0-a3bc-e0970f71af41%40email.android.com.