search

gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

Support all floating point operations #1

Open gernst opened 2 years ago

gernst commented 2 years ago

In runtime/Runtime.cpp there are many floating point operations that are just implemented using abort().

These need to be implemented correctly, following runtime/simple_backend/Runtime.cpp from here. We can use functions supported only by Z3 (which are not in the SMT-LIB standard), but we need to figure out primarily how they are represented in scripts, in comparison to the API calls that the original SymCC does.

thuanpv commented 2 years ago

Hi @gernst, Do you have any example program, like examples/simple.c, that has unsupported floating-point operations? Thuan

gernst commented 2 years ago

Here are many examples: https://test-comp.sosy-lab.org/2022/results/results-verified/legion-symcc.2021-10-15_07-39-10.results.Test-Comp22_coverage-branches.ReachSafety-Floats.xml.bz2.merged.xml.bz2.table.html#/table

You can find the respective sources here: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks

gernst commented 2 years ago

You can add some debug output to the floating point operations, e.g. by chaning to _sym_unsupported()(const char *reason) and indicating the correct reasons. _sym_unsupported could then std::cerr << reason << std::endl and you get to see this when running Legion