mc-imperial / jfs Goto Github PK

The ScopedTimerImpl appears to deadlock when the process is pinned to a single CPU.

Here's a reproducer.

rm -rf jfs-stats.yml jfs-wd && taskset -c 0 bin/jfs '-max-time=5' '-v=1' '-redirect-clang-output=1' '-redirect-libfuzzer-output=1' '-output-dir=jfs-wd' '-keep-output-dir' '-stats-file=jfs-stats.yml' ~/dev/jfs/jfs-experiments/test_benchmarks/QF_FP/SAT/eq-has-solution-1355.smt2

In gdb it appears the main thread is waiting because waiter-join() has been called. However the waiter thread for some reason is not woken up by the previous call to cv.notify_one().

This is very problematic because we use CPU pinning in our experiments and it causes JFS to just hang until the set timeout is reached.

We could run multiple copies of LibFuzzer in parallel, each with a different seed but sharing a corpus directory (so that each running copy benefits from inputs found by the other fuzzers).

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

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 with unsupported kind under jfs-smt2cxx:

user@ccbb42e224b5:~$ jfs/build/bin/jfs /out/20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2 
sat
user@ccbb42e224b5:~$ jfs/build/bin/jfs-smt2cxx /out/20170501-Heizmann-UltimateAutomizer/cos_polynomial_true-unreach-call.c_9.smt2 
unsupported kind
UNREACHABLE executed at /home/user/jfs/src/lib/Core/Z3ASTVisitor.cpp:237!
Aborted (core dumped)

I'll try to look into this more when I have some time but thought I'd file the issue in case it was instantly obvious what was going wrong.

cos_polynomial_true-unreach-call.c_9.txt

We should experiment with implementing our own custom mutator and crossover functions.

This would likely be necessary for #10 and #11 so that padding bits are never mutated.

Our mutators can also use the fact we know the type of the BufferElements to perform specific mutatations.

We need a way of measure how much progress was made during fuzzing. A quantity that we can use is the "maximum number of constraints satisfied simultaneously".

We should compare against as many available solvers that support floating-point/bitvectors as possible.

Floating point

COLIBRI

Winner of SMT-COMP 2017 QF_FP division

https://www.starexec.org/starexec/secure/details/solver.jsp?id=12031

I should check the license on this and whether this is the right version.

TODO: Read this paper!

http://smt-workshop.cs.uiowa.edu/2017/papers/SMT2017_paper_21.pdf

http://soprano-project.fr/download_colibri.html

GoSat

https://github.com/abenkhadra/gosat

Similar to XSat, but open source, uses LLVM to JIT code and uses different optimization libraries.

MathSat5

Need to ask Alberto Griggio or Mikhail Ramalho for optimal configuration for floating-point constraints.

XSat

Paper: http://zhoulaifu.com/wp-content/papercite-data/pdf/xsat.pdf

SMT-COMP submission:
http://smtcomp.sourceforge.net/2017/systemDescriptions/XSat.pdf
https://www.starexec.org/starexec/secure/details/solver.jsp?id=11647

Z3

We already support this. We'll just use Z3's default behaviour.

BitVectors

Given JFS's weakness here I'm not sure if it's worth comparing to that many solvers.

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

Currently we just use LibFuzzer's built in mutation strategy. This is likely sub-optimal for several reasons.

• LibFuzzer is unware of the structure of the data. We know where the free variables are what their sort is.
• We could implement custom mutators based on the sort of a free variable. For example we could have IEEE-754 specific mutators that try flipping the sign, adjusting the exponent, adjusting the significand.

It is probably to early to do this because the internals of JFS are still in flux.

However at some point we should implement a public C API and build a library. This library would need statically incorporate the LLVM support library but it should not incorporate libZ3 so that existing users of Z3 can just link against are library too and have a single copy of Z3.

We should hide all the internal symbols of JFS and only expose the C ones so clients don't see the internal details.

Currently we don't support extracting the model found by the fuzzer or checking that it satisfies the constraints in Z3's constraint language.

We should implement this so that we can check the models that we find.

For some constraint sets it might be the case that there exist several independent subsets (i.e. the intersection of each subset is the empty set).

In this case the fuzzer may waste time mutating inputs that already satisfy a subset. There are two possible fixes

• We generate multiple programs for each subset and fuzz them independently
• We implement a custom mutator and track the subsets so that once a subset is completely satisfied we skip trying to mutate the inputs that correspond to that subset.

Is there any plan for supporting quantified SMT formulas?

Based on this article we could implement a LLVM pass that breaks up comparison instructions into byte comparison instructions.

The difficulty here is how to get this pass into JFS's compilation pipeline. I don't really want to use a modified version of LLVM so ideally we'd build this as a clang or opt plug-in. If we do this we can either

• Have Clang run the pass before coverage instrumentation is added but as late as possible.
• Just emit LLVM IR with clang, run the passes we want using the opt tool and then run clang again on the object file to link everything together.

... or another idea?

A question is also whether we want to perform transformation to the runtime library too.

We could potentially hook up with KLEE. JFS could benefit with extra seeds coming from KLEE that are inputs that has satisfied existing paths.

This will likely be tricky to implement because both JFS and KLEE use different versions of LLVM. This makes #17 a necessary pre-requisite.

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

We currently just packing BufferElements tightly in the buffer based on the order we encounter them when traversing the constraints.

This strategy minimises wasted bits (bits that the fuzzer mutates that has no impact on the constraints) but it means that BufferElementss are not byte aligned. We now support byte alignment but the packing algorithm is sub-optimal. We need an algorithm to perform optimal packing of BufferElements that is

• Byte aligned
• Minimises wasted bits
• Is stable (i.e. with a fixed random seed we should get the same result every time)

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

Hello,

I'm using the docker image and noticed that commands like (check-sat) and (exit) are removed by jfs-opt. Is this behavior expected?

It might be useful to support equality constraints where one of the operands is a conversion of a bitvector to a floating-point type.

We added support for generating "smart seeds".

This PR included a test tests/system_tests/CXXFuzzingBackend/SeedGeneration/bool_bv_float.smt2. Unfortunately this test (when REQUIRES: darwin) fails on Linux.

@jryans has looked into this and the problem seems to be that the implementation of std::uniform_int_distribution varies between libstdc++ (Usually used on Linux) and libcxx (Usually used on macOS).

We either need to replace std::uniform_int_distribution with our own version to avoid this divergence in behaviour.

One approach could be to just copy the implementation in libcxx which has a dual license, one of which is MIT which we are already using for JFS.

https://github.com/llvm-mirror/libcxx/blob/6c372355ba83ad4899a66039f32fbca97204cff6/include/algorithm#L2894

Currently we just compile at -O0. The original reason for this is, is that for some benchmarks compilation time was very large. It is likely on those benchmarks that we made no real progress anyway so we should just enable optimizations (e.g. -O1, -O2, -O3?) and see what happens.

Based on this article we could implement a LLVM pass that breaks up comparison instructions into byte comparison instructions.

The difficulty here is how to get this pass into JFS's compilation pipeline. I don't really want to use a modified version of LLVM so ideally we'd build this as a clang or opt plug-in. If we do this we can either

• Have Clang run the pass before coverage instrumentation is added but as late as possible.
• Just emit LLVM IR with clang, run the passes we want using the opt tool and then run clang again on the object file to link everything together.

... or another idea?

A question is also whether we want to perform transformation to the runtime library too.

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 this goal?

Thanks!

This portfolio mode would run both Z3 and the CXXFuzzingSolver backends and return the result of which ever solver finished first.

Implementing this option would turn JFS from an incomplete solver into a complete solver. This would likely be necessary for any real world adoption of JFS.

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

The fuzzer in general is not very good at guessing the correct value for a equality constraint because the probability of picking the correct value is very low.

Other work has suggested breaking down large integer comparisions into byte-wise comparisons

https://lafintel.wordpress.com/2016/08/15/circumventing-fuzzing-roadblocks-with-compiler-transformations/

When speaking to Kostya he asserted that LibFuzzer's "value profile" would effectively do the same thing. Value profiling traces comparison instructions and computes the hamming distance between the operands and uses changes in the value as an additional "feature" to guide selection of interesting inputs.

We need to implement support to give the fuzzer custom seeds.

Once that's implemented we need to implement the smart seeds. These seeds will be generated from a set of interesting values based on the free variable sort (e.g. for float NaN/+Inf/-Inf/+0/-0/1.0, smallest denormal, largest denormal, smallest normal, largest normal). Interesting values can also be pulled by looking for constants in the constraints themselves.

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 modify the constraints so that eliminated free variables are no
longer mentioned anywhere in the constraints. This would mean that
FreeVariableToBufferAssignmentPass would not need to know anything
about EqualityExtractionPass. So really EqualityExtractionPass
should really be PropagateEqualityPass or something like that...

Consider this benchmark QF_FP/wintersteiger/min/min-has-solution-13472.smt2.

There are several interesting things here

• Our current "is trivial" classification method considers this non-trivial because Z3's simplifier will not constant fold fp.min(+zero, -zero) or fp.max(+zero, -zero).

• When JFS runs this benchmark it detects that the fuzzing buffer is empty but that constant folding failed. In this case JFS will perform a single fuzzing run to determine if the constraints are sat/unsat by just evaluating all the constants at run time.

• This benchmark is expected to be sat but JFS reports it as unsat because at runtime we determine fp.min(-zero, +zero) to be -zero.

Unfortunately IEEE-754 isn't very clear what the definition of min (minNum in the standard ) and max (maxNum in the standard) should be for differently signed zeros.

There's an interesting discussion about this very issue on Z3's issue track. It seems that in the end the semantics (see BTRW15) that were decided on use non-deterministic choice.

Note that the underspecification is an issue only when one of the inputs to maxε,σ or minε,σ is −0 and
the other is +0. However, it means that we consider as acceptable models any structures with function
families maxε,σ and minε,σ that satisfy the specifications above, regardless of whether they return −0
or +0 for (−0, +0), and for (+0, −0). This is necessary because IEEE-754 itself allows either value to
be returned, and compliant implementations do vary. For example, on some Intel processors the result
returned by the x87 and SSE units is different

This is a problem for us because an implicit design decision of JFS is that all functions evaluate to a single deterministic value.

We currently don't have any good way to estimate the difficultly of constraints. Being able to have a way of estimating difficultly would hopefully provide a way for us to understand the performance differences of JFS on different constraints.

A way we could do this take constraints, convert floating-point operations to bitvector operations, then bit blast to a sat problem, and then use a SAT model counting (#SAT) tool to count the number of satisfiable models. The number of satisfiable models divided by the number of all possible models gives the probability of guessing (uniform random) a satisfiable model.

We currently copy a byte at a time when reading from an input from LibFuzzer. We should optimise for the byte aligned case by using memcpy().

Kostya Serebryany noted that there is an undocumented feature in the latest LibFuzzer that allows additional signals (other than coverage) to be used for exploration.

This LibFuzzer test illustrates the idea.

Currently there "might" be a bug in the current implementation. I have a patch up for review.

This feature requires an unreleased LibFuzzer (feature is not in LLVM 5, and LLVM 6 has not been released yet).

Using this feature we can implement what I'm calling the Serebryany encoding.
This encoding of constraints to a program is an improvement over my naive encoding that gives the fuzzer a hint that it found an interesting input when ANY constraint is satisfied. This avoids the issue of constraint order that exists in the naive encoding.

__attribute__((section("__libfuzzer_extra_counters"))) static uint8_t Counters[3];
extern "C" int LLVMFuzzerTestOneInput(const uint8_t *Data, size_t Size) {
   uint64_t solvedConstraints = 0;
   if (constraint0) {
     Counters[0]= 1;
     ++solvedConstraints;
   }
   if (constraint1) {
     Counters[1] = 1;
     ++solvedConstraints;
   }
   if (constraint2) {
      Counters[2] = 1;
      ++solvedConstraints;
   }
   if (solvedConstraints == 3) {
     // TARGET
    abort();
   }
   return 0;
}

It's debatable in the above encoding whether we actually need to use libfuzzer counters because we get coverage when we solve a constraint for the first time.

There are smarter ways we could use this though

• Use the counters to indicate when combinations of constraints are satisfied. The number of combinations. In the above we record when a single constraint is satisfied but we could also record when pairs, triplets, ... etc get satisfied. This might not scale well.

• Use the counters to give feedback that the fuzzer is doing well when more constraints get satisfied but don't care about which ones (e.g. when we solve 3 constraints for the first time give the fuzzer feedback).

It might be useful to perform equality extraction on fp.eq constraints. fp.eq is not semantically the same as = so we would need to handle NaN and +/- zero specially.

This line: export LLVM_BUILD_DIR=/home/user/llvm/src. If this variable is set in this way, a compilation error occurs because of in-source compilation not being allowed.