Questions on C operational models #844
Answered
by
mikhailramalho
kunjsong01
asked this question in
Q&A
Replies: 1 comment
-
A couple of questions:
Q1. What are /tmp/esbmc.9191-98d9-226e/headers and
/tmp/esbmc-headers-5b6b-84c3-9c97?
These are generated by esbmc when verifying a program, it's usually gone
when the program exits. The name is always random. They hold the clang
headers and the models (in goto form).
How are they created?
Check clang_headers.cpp, function clang_headers_path.
There are some other places, but they all
call file_operations::create_tmp_dir.
Q2. How strlen and strcopy (in src/c2goto/library/string.c) are
included/linked/used during the verification? I'm not getting the big
picture.
Check the file cprover_library, function add_cprover_library.
Basically, we dump all the model's goto functions and load only the
functions that are used by the program (and their dependencies).
Q3. Why do we have to use c2goto to convert src/c2goto/library/string.c
into a goto binary file and then "flail" the it to generate the char array?
We convert the goto models to text basically, dump them during the
verification and load only the necessary bits.
What's point of doing so? Why not just including content of
src/c2goto/library/string.c in the input C source code being verified?
We save a bit of time (no parsing of the models during verification), and
space (we only load the necessary bits). We can also control the model
definitions without conflicting with any system headers (check the work
done in pthread.h).
The trade-off is that we ship a bigger esbmc binary:
$ bloaty esbmc-v6.3
FILE SIZE VM SIZE
-------------- --------------
68.3% 40.5Mi 66.8% 40.5Mi .text
15.8% 9.37Mi 15.5% 9.37Mi .data
6.3% 3.75Mi 6.2% 3.75Mi .eh_frame
5.0% 2.98Mi 4.9% 2.98Mi .rodata
3.2% 1.87Mi 3.1% 1.87Mi .data.rel.ro
0.0% 0 2.3% 1.40Mi .bss
1.3% 758Ki 1.2% 758Ki .gcc_except_table
0.0% 9.07Ki 0.0% 0 .note.stapsdt
0.0% 6.43Ki 0.0% 6.20Ki .init_array
0.0% 5.95Ki 0.0% 5.95Ki __libc_freeres_fn
0.0% 4.55Ki 0.0% 4.55Ki __libc_thread_freeres_fn
0.0% 3.18Ki 0.0% 0 [Unmapped]
0.0% 2.23Ki 0.0% 2.23Ki __libc_IO_vtables
0.0% 2.00Ki 0.0% 0 [ELF Section Headers]
0.0% 1.12Ki 0.0% 1.12Ki .rela.plt
0.0% 676 0.0% 812 [16 Others]
0.0% 448 0.0% 448 .got
0.0% 416 0.0% 416 .got.plt
0.0% 384 0.0% 384 .plt
0.0% 380 0.0% 0 .shstrtab
0.0% 336 0.0% 336 [ELF Program Headers]
100.0% 59.2Mi 100.0% 60.6Mi TOTAL
Most of esbmc's binary is the clang headers + the models.
…--
Mikhail Ramalho.
|
Beta Was this translation helpful? Give feedback.
0 replies
Answer selected by
kunjsong01
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
I'm trying to connect the dots to see how C operationals models are used in action. Here's the test case I used for C strlen and strcpy:
CMD: ./esbmc 01_cbmc_String_Abstraction3/main.c --unwind 101 --verbosity 10
Below is the search list for
#include
:A couple of questions:
Q1. What are
/tmp/esbmc.9191-98d9-226e/headers
and/tmp/esbmc-headers-5b6b-84c3-9c97
? How are they created?BTW, they don't match the folder names in my /tmp directory. I've got:
esbmc.df15-bacc-9c8b
andesbmc-headers-0798-ffdb-ef83
(the former appears to be a copy ofesbmc/src/c2goto/headers
and the latter looks like a directory containing clang headers?)Q2. How strlen and strcopy (in
src/c2goto/library/string.c
) are included/linked/used during the verification? I'm not getting the big picture.Q3. Why do we have to use c2goto to convert
src/c2goto/library/string.c
into a goto binary file and then "flail" the it to generate the char array? What's point of doing so? Why not just including content ofsrc/c2goto/library/string.c
in the input C source code being verified?Beta Was this translation helpful? Give feedback.
All reactions