jfs

jfs copied to clipboard

jfs-smt2cxx can't handle all formulas that jfs can

3

There seems to be a slight mismatch in the set of formulas accepted by jfs-smt2cxx versus jfs. An example is `20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2` (attached), which is quickly solved using jfs but dies...

moyix

Now with the benefit of hindsight I see there is a terrible coupling between `EqualityExtractionPass` and `FreeVariableToBufferAssignmentPass` that means the implementation is unnecessarily complicated. What `EqualityExtractionPass` should really do is...

delcypher

Is it possible to extend JFS to process string constraints?

1

JFS is an impressive tool to strengthen solver's capacity with fuzzing. I'm wondering whether it is possible to extend JFS to process string constraints? What should I do to realize...

lingjunz

jryans

jryans

We should rework our implementation to not require our custom patches to LibFuzzer.

jryans

We currently run Clang at `-O0` when compiling code. We should evaluate using other optimization levels to see what the impact is.

jryans

Clang has the `-fsanitize-coverage-inline-8bit-counters` option. We should experiment with it.

jryans

LibFuzzer supports a `-use_cmp=1` option which relies and compiler instrumentation of comparison instructions (`-fsanitize-coverage-trace-cmp`). Which should experiment with this.

jryans

LibFuzzer has the `-use_value_profile=1`. We should study how it works and evaluate if it has an performance impact.

jryans