Code Monkey home page Code Monkey logo

map2check's People

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar

map2check's Issues

Improving the code style

  • Add code style scripts
  • Add documentation to apply code style
  • Update build script to validate code style

Fix incorrect results in NoOverflows-Other

Verification tasks in SV-COMP

  • ../../sv-benchmarks/c/bitvector/byte_add-2.i

    Fix check for shift operation r3 << 24U, see ISO/IEC 9899:2011 6.5.7#4, in that case r3<<24U will exceed INT_MAX

  • ../../sv-benchmarks/c/bitvector/byte_add_1-2.i

    Not identified bug root, but we have modeling issues with shift operation

  • ../../sv-benchmarks/c/bitvector/byte_add_2-1.i

    Not identified bug root, but we have modeling issues with shift operation

Fix incorrect results in ReachSafety-Heap

Verification results from SV-COMP

  • ../../sv-benchmarks/c/ldv-regression/sizeofparameters_test.i

    Incorrect long int a = __VERIFIER_nondet_long(); representation

  • ../../sv-benchmarks/c/ldv-regression/test27-2.c

    Expected FALSE, but the result is TRUE
    Check:
    libfuzzer -> ERROR: UndefinedBehaviorSanitizer: SEGV on unknown address
    KLEE -> memory error: out of bound pointer
    OR -> Struct modeling error

  • ../../sv-benchmarks/c/ldv-regression/test28-1.c
    >> Same ERROR as the ldv-regression/test27-2.c

Add new subcategories from SV-COMP

New subcategories from SV-COMP not supported yet

Apply minor changes to support:

  • ReachSafety-ECA
  • ReachSafety-Floats
  • ReachSafety-ProductLines
  • ReachSafety-Sequentialized
  • SoftwareSystems-AWS-C-Common-ReachSafety
  • SoftwareSystems-BusyBox-MemSafety
  • SoftwareSystems-BusyBox-NoOverflows
  • SoftwareSystems-DeviceDriversLinux64-ReachSafety
  • SoftwareSystems-OpenBSD-MemSafety

Caller Refactoring

We should use the Clang/LLVM API instead of calling external binaries. For example, the older version used this

Places where refactoring is needed:

Also, some other fixes for caller (we should open an issue for Caller class only):

Originally posted by @RafaelSa94 in #8 (comment)

Crucible support as a Symbolic Engine

Is your feature request related to a problem? Please describe.
Currently, we only have support for KLEE as a symbolic engine, the issue is that it contains a limitation for floating numbers. Crucible supports enconding for floats, has support for SV-COMP notation and it's API contains all that is needed for a Generator.

Describe the solution you'd like
Implement a NonDetGeneratorCrucible and compare it with KLEE specially for floats.

Fix incorrect results in MemSafety-Other

Verification tasks from SV-COMP

  • ../../sv-benchmarks/c/memsafety-ext3/derefInLoop1.c

Expected FALSE, but result is TRUE
Incorrect mapping = BUG

  • ../../sv-benchmarks/c/memsafety-ext3/scopes1.c

LOC 16, not checked ptr scope

  • ../../sv-benchmarks/c/memsafety-ext3/scopes3.c

Incorrect mapping = ptr not initialized

  • ../../sv-benchmarks/c/memsafety-ext3/scopes5.c

Incorrect mapping = incorrect initialized

  • ../../sv-benchmarks/c/pthread-memsafety/list1.i

pthread not modelling, I suggest you to create a new issue

  • ../../sv-benchmarks/c/memsafety-bftpd/bftpd_2.i

Incorrect modelling struct and void

Fix build crab-llvm

  • Update fork
  • Port sea-dsa fork to LLVM 6.0
  • Frozen build adopting commits
  • Update crab-llvm fork from hbgit user on github
  • Fix Crabllvm build broken

Updating front-end

  • Review tool input options
  • Improve how the tool modes are executed
  • Review the counterexample generation

LLVM Optimizations with KLEE

Is your feature request related to a problem? Please describe.
Not related to a problem. Currently, we default to -O3 optimizations and let KLEE decides which solver to be used. The -O3 may not be the best for Symbolic Execution and the SMT formula generated by KLEE may not be the best for the selected solver.

Describe the solution you'd like
We should select which solver and the best optimization for Symbolic Execution.

Describe alternatives you've considered
Extend Map2Check to have a class to select which optimizations will be done.

Additional context
The paper Studying the influence of standard compiler optimizations on symbolic execution contains details on how LLVM optimizations affects KLEE and the solvers

Add a argument to specify the name of the target function

Is your feature request related to a problem? Please describe.
FuseBMC is trying to use map2check to create coverage for C programs. However, its targets consists in functions named GOAL_N (where N is a number).

Describe the solution you'd like
Add the option --target-function-name which will set the target function name for map2check. This will require patches over the TargetPass and over the opt calls.

Describe alternatives you've considered
The tool that is using map2check could instead rename the current target into __VERIFIER_error()

Additional context
Some reference:

Clean up branches

Checkout the following branches, aiming to update or remove from the project:

  • feature/code_style
  • feature/dockerfiles
  • feature/force_predassume
  • feature/llvmbc-input
  • feature/loops
  • crabllvm
  • feature/memderef-fix
  • feature/new-build
  • feature/sqlite
  • feature/svcomp19
  • quickfix/allocation_test_fix
  • feature/regressiontest

Support to check floating-point arithmetic

KLEE-Float
Check out https://srg.doc.ic.ac.uk/projects/klee-float/

That is an extension project to the KLEE symbolic execution engine that supports reasoning about floating-point arithmetic. For more details see:

Floating-Point Symbolic Execution: A Case Study in N-version Programming. Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair Donaldson, Rafael Zähl, Klaus Wehrle. IEEE/ACM International Conference on Automated Software Engineering (ASE 2017)

Update strategy to apply smt solver

Improving testing tool

  • Create a new flow to test tool
  • Adopting benchexec to test regression
  • Setting up Travis to run the tests
  • Create a docker to run benchexec for regression test
  • Create testing for production
  • Create testing for deploy

Fix incorrect result in ReachSafety-ControlFlow

Verification tasks from SV-COMP

One possible solution for the incorrect true results is to adopt a redundant check.

  • Add program invariant result in ERROR

  • libfuzzer out: fuzzing was not performed, you have only executed the target code on a fixed set of inputs.

  • ../../sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-1.c
    - Checking KLEE options
    - Bug in process KLEE result "KLEE: WARNING: error opening file"

  • ../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c
    - Bug in process KLEE result "KLEE: WARNING: error opening file"

  • ../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c
    - Bug in process KLEE result "KLEE: WARNING: error opening file"

KLEE was not able to find the bug:

  • ../../sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c
  • ../../sv-benchmarks/c/ssh-simplified/s3_clnt_2.cil-1.c
  • ../../sv-benchmarks/c/ssh-simplified/s3_clnt_3.cil-2.c
  • ../../sv-benchmarks/c/ssh-simplified/s3_clnt_4.cil-2.c
  • ../../sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c
  • ../../sv-benchmarks/c/ssh/s3_clnt.blast.02.i.cil-1.c
  • ../../sv-benchmarks/c/ssh/s3_clnt.blast.03.i.cil-1.c
  • ../../sv-benchmarks/c/ssh/s3_clnt.blast.04.i.cil-1.c
  • ../../sv-benchmarks/c/ssh/s3_srvr.blast.08.i.cil-2.c
  • ../../sv-benchmarks/c/ssh/s3_srvr.blast.10.i.cil-2.c
  • ../../sv-benchmarks/c/ssh/s3_srvr.blast.11.i.cil-1.c
  • ../../sv-benchmarks/c/ssh/s3_srvr.blast.15.i.cil-1.c

Improving counterexample generation

  • Identify failures
  • Fix bugs on counterexample generation
  • Propose a method to simplify the counterexample size
  • Coding a method to simplify the counterexample size

Fix incorrect CRAB call to fuzzer

Fix incorrect call of CRABLLVM

I would like to suggest you skip the CRABLLVM call to run fuzzing.
Start at:

  • Map2Check::NonDetGenerator::LibFuzzer >> map2check.cpp line 421
  • caller->compileToCrabLlvm(); >> incorrect call at map2check.cpp line 202

Fix incorrect results in MemSafety-MemCleanup

Verification tasks from SV-COMP

  • ../../sv-benchmarks/c/list-ext3-properties/dll_nullified-1.i

    You need to improve memory leak check, bug root new_head->data_2 = __VERIFIER_nondet_int() == len? 1 : 0;
    expected_verdict: false but the result is TRUE

KLEE crash incorrect results

Check KLEE output after the map2check verification

KLEE crashes and incorrect TRUE results for Map2Check mode (e.g., target generate prt error).

I would like to suggest you check out the KLEE output before to show TRUE answer for the verification task.

Add option to use a specific generator

Is your feature request related to a problem? Please describe.
I'd like to run only KLEE or only libFuzzer (or any future generator)

Describe the solution you'd like
Add the --generator option with klee and libfuzerr as valid values

Describe alternatives you've considered
None

Additional context
It should be simple, the major change will be at the wrapper of the interaction between klee and libFuzzer will have to be refactored.

Add support to Termination Analysis

Termination Analysis

Add support to verify the category Termination-MainControlFlow on SV-COMP that contains programs for which termination should be decided.

I suggest you check out the follows paper:

  • T2: Temporal Property Verification
  • Termination-Checking for LLVM Peephole Optimizations
  • Termination Analysis of C Programs Using Compiler Intermediate Languages

Also suggest you to check SeaHorn tool.

Add support to verify concurrent programs

Add support for concurrency programs, e.g., the category ConcurrencySafety.

One possible solution is to adopt Lazy-Cseq* (https://www.southampton.ac.uk/~gp1y10/cseq/) tool to generate the C code, then apply Map2Check tool with its features to improve de verification. Note that Lazy-Cseq generates nondet calls for KLEE.

*CSeq is a framework that facilitates the development of code-to-code translations for concurrent C programs with POSIX threads based on sequentialization.

Skip call nondet generator

Skipping to call nondet generator

I would like to suggest to avoid call fuzzer or symbolic execution when a program does not have a nondet function.

  • Line 422 map2check.ccp. I guess is possible to apply a static analysis to identify nondet functions call

Fix incorrect results in NoOverflows-BitVectors

Verification tasks from SV-COMP

  • ../../sv-benchmarks/c/signedintegeroverflow-regression/AdditionIntMax.i

    It hasn't nondet, thus you could improve the analysis turn off libfuzzer and klee for nondet
    the sum result (2147483647 + 1) is not allowed in int type of sizeof(int) = 4

  • ../../sv-benchmarks/c/signedintegeroverflow-regression/Multiplication-2.i

    It hasn't nondet, thus you could improve the analysis turn off libfuzzer and klee for nondet
    the mult result (65536 * 32768) is not allowed in int type of sizeof(int) = 4

  • ../../sv-benchmarks/c/signedintegeroverflow-regression/NoConversion.i

    It hasn't nondet, thus you could improve the analysis turn off libfuzzer and klee for nondet
    the sum result long x = 2147483647 + 1; is not allowed in long type of sizeof(long or long int) = 4

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.