eurecom-s3 / symcc

SymCC: efficient compiler-based symbolic execution
http://www.s3.eurecom.fr/tools/symbolic_execution/symcc.html
GNU General Public License v3.0
773 stars 135 forks source link

Correct Z3 version #51

Closed edrdo closed 3 years ago

edrdo commented 3 years ago

Hi,

I prepared compilation of symcc using

$ cmake -G Ninja -DQSYM_BACKEND=ON -DZ3_TRUST_SYSTEM_VERSION=on  path_for_code

but I am then obtaining compilation errors related to Z3:

$ ninja check
...
FAILED: qsym_backend/CMakeFiles/SymRuntime.dir/expr_builder__gen.cpp.o 
/usr/bin/c++  -DSymRuntime_EXPORTS -I/home/edrdo/symcc/runtime/qsym_backend -I/home/edrdo/symcc/runtime/qsym_backend/.. -isystem /usr/lib/llvm-11/include -isystem /home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool -std=c++17 -Wredundant-decls -Wcast-align -Wmissing-include-dirs -Wswitch-default -Wextra -Wall -Winvalid-pch -Wredundant-decls -Wformat=2 -Wmissing-format-attribute -Wformat-nonliteral -fPIC   -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -MD -MT qsym_backend/CMakeFiles/SymRuntime.dir/expr_builder__gen.cpp.o -MF qsym_backend/CMakeFiles/SymRuntime.dir/expr_builder__gen.cpp.o.d -o qsym_backend/CMakeFiles/SymRuntime.dir/expr_builder__gen.cpp.o -c qsym_backend/expr_builder__gen.cpp
In file included from /usr/include/z3.h:26,
                 from /usr/include/z3++.h:28,
                 from /home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr.h:12,
                 from /home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr_cache.h:4,
                 from /home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr_builder.h:6,
                 from qsym_backend/expr_builder__gen.cpp:1:
/home/edrdo/symcc/runtime/qsym_backend/pin.H:35:18: error: declaration does not declare anything [-fpermissive]
 typedef uint64_t __uint64;
                  ^~~~~~~~
In file included from /home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr_cache.h:4,
                 from /home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr_builder.h:6,
                 from qsym_backend/expr_builder__gen.cpp:1:
/home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr.h: In member function 'virtual z3::expr qsym::ZExtExpr::toZ3ExprRecursively(bool)':
/home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr.h:642:16: error: 'zext' is not a member of 'z3'
     return z3::zext(e->toZ3Expr(verbose), bits_ - e->bits());
                ^~~~
/home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr.h: In member function 'virtual z3::expr qsym::SExtExpr::toZ3ExprRecursively(bool)':
/home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr.h:672:16: error: 'sext' is not a member of 'z3'
     return z3::sext(e->toZ3Expr(verbose), bits_ - e->bits());
                ^~~~
/home/edrdo/symcc/runtime/qsym_backend/qsym/qsym/pintool/expr.h:672:16: note: suggested alternative: 'sat'

...
several other errors of the same kind
...

The Z3 version installed is the standard one for Debian 10, I think.

$ z3 --version
Z3 version 4.4.1

Should I use another Z3 version? Thanks

edrdo commented 3 years ago

Sorry for the spam, I now realize that you do indicate Z3 4.5 or later in the README.md. I will proceed with trying that.

When Z3_TRUST_SYSTEM_VERSION=on no version check is performed but I understood that's intentional.