pku-msv-lab / angelix Goto Github PK

Semantic program repair system for C programs

License: MIT License

Makefile 0.85% CMake 0.08% C++ 5.41% Python 9.21% C 2.19% Shell 0.69% Perl 11.42% Java 69.52% HTML 0.42% Dockerfile 0.21%

program-repair

angelix's Introduction

Angelix

Semantics-based automated program repair tool for C programs. Angelix fixes bugs manifested by failing test cases and searches for the minimal change in order to preserve the original source code. Powered by KLEE symbolic execution engine and Z3 SMT solver.

If you use Angelix in your research project, please include the following citation:

@inproceedings{mechtaev2016angelix,
    title={Angelix: Scalable multiline program patch synthesis via symbolic analysis},
    author={Mechtaev, Sergey and Yi, Jooyong and Roychoudhury, Abhik},
    booktitle={Proceedings of the 38th International Conference on Software Engineering},
    pages={691--701},
    year={2016},
    organization={ACM}
}

Installation

Angelix is distributed in source code form and pre-installed in VirtualBox image. The VirtualBox image also contains Angelix ICSE'16 and SemFix ICSE'13 evaluation results.

Option 1: VirtualBox image

You can download VirtualBox image with pre-installed Angelix. Note that it contains an outdated version of Angelix and is distributed only for the demonstration purpose.

Please download the following files: https://s3-ap-southeast-1.amazonaws.com/angelix/angelix-icse16-v2.vbox https://s3-ap-southeast-1.amazonaws.com/angelix/angelix-icse16-v2.vdi (9.7 GB) https://s3-ap-southeast-1.amazonaws.com/angelix/md5sum.txt

Execute "md5sum -c md5sum.txt" to verify your download.

The image includes Ubuntu 14.04 64-bit with pre-installed Angelix.

The user/password are angelix/angelix.

Option 2: Build from source

The following is required to install Angelix from source code:

40GB Hard drive
8GB Memory
Ubuntu 14.04 64-bit*

* Angelix can run on other 64-bit Linux distributions, however installation scripts were tested only on Ubuntu 14.04. If you want to install Angelix on a different system, you may need to modify Makefile and activate scripts.

Clone repository recursively:

git clone --recursive https://github.com/mechtaev/angelix.git

Install dependencies:

sudo apt-get install git wget xz-utils build-essential time
sudo apt-get install curl dejagnu subversion bison flex bc libcap-dev
sudo apt-get install cmake libncurses5-dev libboost-all-dev

Install Java 8 (for Ubuntu 14.04) and Maven:

sudo apt-get install software-properties-common
sudo apt-add-repository ppa:webupd8team/java
sudo apt-get update
sudo apt-get install oracle-java8-installer
sudo apt-get install maven

Install SBT by following intructions.

Set Angelix environment:

. activate

Download and build required modules:

make default

Run tests:

make test

Documentation

To set optimal configuration for your subject, refer to the Configuration section of the manual.

Changelog

1.1 (2017-Mar-20)

Implemented enhancements:

New experimental synthesizer (--use-nsynth option)
Automatically instrumenting printf arguments with ANGELIX_OUTPUT (--instr-printf option)
Finding all patches (--generate-all option)
Improved language support

Fixed bugs:

Various bugs in frontend, inference and synthesis.

1.0 (2016-Jul-8)

Implemented enhancements:

Supported NULL pointer, break and continue statements, 64-bit long in ANGELIX_OUTPUT.

Fixed bugs:

Various reported bugs in frontend and localization.

icse16 (2016-Feb-19)

Initial release used to reproduce ICSE'16 experiments. Available on VirtualBox VM.

Publications

Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis. S. Mechtaev, J. Yi, A. Roychoudhury. ICSE'16. [pdf]

DirectFix: Looking for Simple Program Repairs. S. Mechtaev, J. Yi, A. Roychoudhury. ICSE'15. [pdf]

SemFix: Program Repair via Semantic Analysis. H.D.T. Nguyen, D. Qi, A. Roychoudhury, S. Chandra. ICSE'13. [pdf]

Contributors

Principal investigator:

Abhik Roychoudhury

Developers:

Sergey Mechtaev
Jooyong Yi

Contributors:

Shin Hwei Tan
Yulis

angelix's People

Contributors

Stargazers

Watchers

angelix's Issues

Files are never closed after being written (in src/repair)

This issue exists in almost all python code in src/repair. Every time a "file.write()" is invoked, a corresponding "file.close()" is forgotten.
Here is an example from src/repair/transformation.py of class FixInjector:

        patch_file = join(dirpath, 'patch')
        with open(patch_file, 'w') as file:
            for e, p in patch.items():
                file.write('{} {} {} {}\n'.format(*e))
                file.write(p + "\n")

The "file" is not closed after being written.
I think it would also be better to add an exception handler for file writing.

Can't pass tutorial test

Hello,

I also am having trouble passing the tutorial test. I successfully built Angelix from source on a virtual machine running Ubuntu 14.04. I followed the tutorial, but the exact command I used to run Angelix was angelix /home/gilbert/Documents/angelix/src distance.c oracle 1 2 3 --assert assert.json --group-size 2 --verbose. Here is the output:

INFO     repair          option max_angelic_paths = None
INFO     repair          option klee_ignore_errors = False
INFO     repair          option klee_debug = False
INFO     repair          option init_uninit_vars = False
INFO     repair          option localize_only = False
INFO     repair          option verbose = True
INFO     repair          option synthesis_bool_only = False
INFO     repair          option klee_solver_timeout = None
INFO     repair          option mute_warning = False
INFO     repair          option synthesis_func_params = False
INFO     repair          option mute_test_message = False
INFO     repair          option synthesis_ptr_vars = False
INFO     repair          option group_by_score = False
INFO     repair          option invalid_localization = False
INFO     repair          option klee_search = None
INFO     repair          option use_semfix_syn = False
INFO     repair          option mute_build_message = False
INFO     repair          option max_z3_trials = 2
INFO     repair          option synthesis_global_vars = False
INFO     repair          option use_nsynth = False
INFO     repair          option generate_all = False
INFO     repair          option defect = ['if-conditions', 'assignments']
INFO     repair          option build_before_instr = False
INFO     repair          option group_size = 2
INFO     repair          option ignore_infer_errors = False
INFO     repair          option synthesis_timeout = 30000
INFO     repair          option klee_timeout = None
INFO     repair          option localize_from_bottom = False
INFO     repair          option path_solving_timeout = 60000
INFO     repair          option localization = jaccard
INFO     repair          option ignore_trivial = False
INFO     repair          option initial_tests = 1
INFO     repair          option synthesis_levels = ['alternatives', 'integer-constants', 'boolean-constants']
INFO     repair          option klee_max_forks = None
INFO     repair          option klee_max_depth = None
INFO     repair          option test_timeout = None
INFO     repair          option instr_printf = None
INFO     repair          option suspicious = 20
INFO     repair          option all_tests = False
INFO     repair          option ignore_trans_errors = False
INFO     repair          option redundant_test = False
INFO     repair          option semfix = False
INFO     repair          option synthesis_used_vars = True
INFO     project         configuring validation source
INFO     project         building json compilation database from validation source
gcc -I. -c distance.c -o distance.o
gcc distance.o -o distance
INFO     testing         running test '1' of validation source
INFO     testing         running test '2' of validation source
INFO     testing         running test '3' of validation source
INFO     project         configuring frontend source
INFO     transformation  instrumenting repairable of frontend source
/home/gilbert/Documents/angelix/.angelix/frontend/distance.c:25:10: warning: 
      implicit declaration of function 'atoi' is invalid in C99
      [-Wimplicit-function-declaration]
    x1 = atoi(argv[1]);
         ^
9 9 9 14
x1 > x2
10 14 10 19
x1 - x2
12 14 12 19
x2 - x1
13 9 13 14
y1 > y2
14 14 14 19
y1 - y2
16 14 16 19
y1 - y2
17 9 17 14
dx > dy
1 warning generated.
INFO     project         building frontend source
angelix-compiler --test -I. -c distance.c -o distance.o
[angelix-compiler] gcc -include /home/gilbert/angelix/src/runtime/runtime.h '-I.' '-c' 'distance.c' '-o' 'distance.o' -L/home/gilbert/angelix/build/lib/test -langelix -L/home/gilbert/angelix/src/klee/Release+Asserts/lib -lkleeRuntest 
angelix-compiler --test distance.o -o distance
[angelix-compiler] gcc -include /home/gilbert/angelix/src/runtime/runtime.h 'distance.o' '-o' 'distance' -L/home/gilbert/angelix/build/lib/test -langelix -L/home/gilbert/angelix/src/klee/Release+Asserts/lib -lkleeRuntest 
INFO     repair          running positive tests for debugging
INFO     testing         running test '1' of frontend source
INFO     testing         running test '2' of frontend source
INFO     repair          running negative tests for debugging
INFO     testing         running test '3' of frontend source
INFO     repair          repair test suite: ['1', '2', '3']
INFO     repair          validation test suite: ['1', '2', '3']
INFO     localization    selected expressions [(13, 9, 13, 14), (16, 14, 16, 19)] with group score 1.3333 
INFO     localization    selected expressions [(9, 9, 9, 14), (10, 14, 10, 19)] with group score 0.83333 
INFO     localization    selected expressions [(17, 9, 17, 14)] with group score 0.33333 
INFO     repair          considering suspicious expressions [(13, 9, 13, 14), (16, 14, 16, 19)]
INFO     reduction       selected 1 tests
INFO     reduction       selected passing tests: []
INFO     reduction       selected failing tests: ['3']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
/home/gilbert/Documents/angelix/.angelix/backend/distance.c:25:10: warning: 
      implicit declaration of function 'atoi' is invalid in C99
      [-Wimplicit-function-declaration]
    x1 = atoi(argv[1]);
         ^
13 9 13 14
y1 > y2
16 14 16 19
y1 - y2
1 warning generated.
INFO     project         building backend source
angelix-compiler --klee -I. -c distance.c -o distance.o
[angelix-compiler] llvm-gcc -include /home/gilbert/angelix/src/runtime/runtime.h -emit-llvm -g -O0 -D ANGELIX_SYMBOLIC_RUNTIME '-I.' '-c' 'distance.c' '-o' 'distance.o' 
angelix-compiler --klee distance.o -o distance
[angelix-compiler] llvm-ld --disable-opt 'distance.o' '-o' 'distance' -L/home/gilbert/angelix/build/lib/klee -langelix 
INFO     inference       inferring specification for test '3'
INFO     testing         running test '3' of backend source with KLEE
mv: ‘klee.log’ and ‘/home/gilbert/Documents/angelix/.angelix/backend/klee.log’ are the same file
mv: ‘./klee-out-0’ and ‘/home/gilbert/Documents/angelix/.angelix/backend/klee-out-0’ are the same file
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       solving path .angelix/backend/klee-out-0/test000003.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       found 0 angelic paths for test '3'
INFO     repair          considering suspicious expressions [(9, 9, 9, 14), (10, 14, 10, 19)]
INFO     reduction       selected 1 tests
INFO     reduction       selected passing tests: []
INFO     reduction       selected failing tests: ['3']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
/home/gilbert/Documents/angelix/.angelix/backend/distance.c:25:10: warning: 
      implicit declaration of function 'atoi' is invalid in C99
      [-Wimplicit-function-declaration]
    x1 = atoi(argv[1]);
         ^
9 9 9 14
x1 > x2
10 14 10 19
x1 - x2
1 warning generated.
INFO     project         building backend source
angelix-compiler --klee -I. -c distance.c -o distance.o
[angelix-compiler] llvm-gcc -include /home/gilbert/angelix/src/runtime/runtime.h -emit-llvm -g -O0 -D ANGELIX_SYMBOLIC_RUNTIME '-I.' '-c' 'distance.c' '-o' 'distance.o' 
angelix-compiler --klee distance.o -o distance
[angelix-compiler] llvm-ld --disable-opt 'distance.o' '-o' 'distance' -L/home/gilbert/angelix/build/lib/klee -langelix 
INFO     inference       inferring specification for test '3'
INFO     testing         running test '3' of backend source with KLEE
mv: ‘klee.log’ and ‘/home/gilbert/Documents/angelix/.angelix/backend/klee.log’ are the same file
mv: ‘./klee-out-0’ and ‘/home/gilbert/Documents/angelix/.angelix/backend/klee-out-0’ are the same file
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       solving path .angelix/backend/klee-out-0/test000003.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       found 0 angelic paths for test '3'
INFO     repair          considering suspicious expressions [(17, 9, 17, 14)]
INFO     reduction       selected 1 tests
INFO     reduction       selected passing tests: []
INFO     reduction       selected failing tests: ['3']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
/home/gilbert/Documents/angelix/.angelix/backend/distance.c:25:10: warning: 
      implicit declaration of function 'atoi' is invalid in C99
      [-Wimplicit-function-declaration]
    x1 = atoi(argv[1]);
         ^
17 9 17 14
dx > dy
1 warning generated.
INFO     project         building backend source
angelix-compiler --klee -I. -c distance.c -o distance.o
[angelix-compiler] llvm-gcc -include /home/gilbert/angelix/src/runtime/runtime.h -emit-llvm -g -O0 -D ANGELIX_SYMBOLIC_RUNTIME '-I.' '-c' 'distance.c' '-o' 'distance.o' 
angelix-compiler --klee distance.o -o distance
[angelix-compiler] llvm-ld --disable-opt 'distance.o' '-o' 'distance' -L/home/gilbert/angelix/build/lib/klee -langelix 
INFO     inference       inferring specification for test '3'
INFO     testing         running test '3' of backend source with KLEE
mv: ‘klee.log’ and ‘/home/gilbert/Documents/angelix/.angelix/backend/klee.log’ are the same file
mv: ‘./klee-out-0’ and ‘/home/gilbert/Documents/angelix/.angelix/backend/klee-out-0’ are the same file
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       value 'stdout' executed 0 times while 1 required
INFO     inference       found 0 angelic paths for test '3'
INFO     repair          no patch generated in 9s
FAIL

I ran make test, but all tests pass. Here is my "angelix" folder with the tutorial files: angelix.tar.gz. There is probably something obvious I'm missing, but if you could take a look at this, I would really appreciate it. Thank you!

Update for the latest KLEE

There were a lot of improvements and bugfixes in KLEE since:

2.0.0 release https://github.com/klee/klee/releases/tag/v2.0
Newer changes: klee/klee@v2.0...master

Don't consider expression with 0 suspiciousness score, because they are not executed by failing tests

Angelix docker version failed test

There is a failing test on the docker version of Angelix

======================================================================
FAIL: test_deletebreak (__main__.TestAngelix)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "tests/tests.py", line 126, in test_deletebreak
    self.assertEqual(result, 'SUCCESS')
AssertionError: 'FAIL' != 'SUCCESS'
- FAIL
+ SUCCESS


----------------------------------------------------------------------
Ran 17 tests in 209.562s

Dockerfile doesn't build: Unsupported major.minor version 52.0

When in the RUN make stage of trying to build the docker image, I got the error java.lang.UnsupportedClassVersionError: scala/Option : Unsupported major.minor version 52.0. The Docker build, therefore, was unsuccessful.

Guards not add for certain type of statement

The "guards" defect class doesn't add guard for the following types of statement:

Break / Continue
E+=E1 / E-=E1 / E*=E1

For example, if the defect involves removing break statement. Angelix doesn't insert angelix_trace in the frontend instrumentation and hence, no fix is generated.

Use klee_prefer_cex for characters

Can't reproduce experimental results with docker image

I tried reproducing Angelix's experimental data locally using a docker image as described by the following Dockerfile:

FROM mechtaev/angelix:1.1
WORKDIR /src/

RUN apt-get install -y libffi-dev gtk-doc-tools libgtk2.0-dev libpcap-dev

COPY angelix-experiments/ .
RUN chmod +x ./repair ./repair-* ./fetch ./get-options

All experiments, other than heartbleed, could not be ran because the genprog benchmarks is unavailable. For example, running ./repair libtiff d13be72c-ccadf48a results in the following output:

--2021-06-15 11:00:44--  http://dijkstra.cs.virginia.edu/genprog/resources/genprog-icse2012-benchmarks/libtiff-bug-d13be72c-ccadf48a.tar.gz
Resolving dijkstra.cs.virginia.edu (dijkstra.cs.virginia.edu)... failed: Name or service not known.
wget: unable to resolve host address 'dijkstra.cs.virginia.edu'

As for heartbleed, running ./repair openssl 1.0.1-beta1 results in:

./repair-openssl: No such file or directory

Running ./repair-heartbleed `./get-options openssl 1.0.1-beta1` appears to do the trick, but Angelix is incapable of generating a fix. The contents of angelix.log are the following:

INFO     project         configuring validation source
INFO     project         building json compilation database from validation source
INFO     testing         running test '1' of validation source
INFO     testing         running test '4' of validation source
INFO     testing         running test '6' of validation source
INFO     testing         running test '7' of validation source
INFO     testing         running test '8' of validation source
INFO     project         configuring frontend source
INFO     transformation  instrumenting repairable of frontend source
INFO     project         building frontend source
INFO     repair          running positive tests for debugging
INFO     testing         running test '1' of frontend source
INFO     testing         running test '6' of frontend source
INFO     testing         running test '7' of frontend source
INFO     repair          running negative tests for debugging
INFO     testing         running test '4' of frontend source
INFO     testing         running test '8' of frontend source
INFO     repair          repair test suite: ['1', '4', '6', '7', '8']
INFO     repair          validation test suite: ['1', '4', '6', '7', '8']
INFO     localization    selected expressions [(2432, 8, 2432, 8)] with group score 0.5 
INFO     localization    selected expressions [(171, 15, 171, 26)] with group score 0.4 
INFO     localization    selected expressions [(2415, 7, 2415, 7)] with group score 0.4 
INFO     localization    selected expressions [(2417, 6, 2417, 9)] with group score 0.4 
INFO     localization    selected expressions [(2422, 6, 2422, 39)] with group score 0.4 
INFO     repair          considering suspicious expressions [(2432, 8, 2432, 8)]
INFO     reduction       selected 5 tests
INFO     reduction       selected passing tests: ['1', '6', '7']
INFO     reduction       selected failing tests: ['4', '8']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
INFO     project         building backend source
WARNING  project         compilation of .angelix/backend returned non-zero code
WARNING  project         failed to build .angelix/backend/apps/s_server.c
WARNING  project         failed to build .angelix/backend/apps/s_client.c
WARNING  project         failed to build .angelix/backend/apps/s_time.c
WARNING  project         failed to build .angelix/backend/apps/ocsp.c
WARNING  project         failed to build .angelix/backend/apps/openssl
INFO     inference       inferring specification for test '4'
INFO     testing         running test '4' of backend source with KLEE
INFO     inference       sleeping for 1 second...
WARNING  inference       No paths explored
INFO     repair          considering suspicious expressions [(171, 15, 171, 26)]
INFO     reduction       selected 5 tests
INFO     reduction       selected passing tests: ['1', '6', '7']
INFO     reduction       selected failing tests: ['4', '8']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
INFO     project         building backend source
WARNING  project         compilation of .angelix/backend returned non-zero code
WARNING  project         failed to build .angelix/backend/apps/s_server.c
WARNING  project         failed to build .angelix/backend/apps/s_client.c
WARNING  project         failed to build .angelix/backend/apps/s_time.c
WARNING  project         failed to build .angelix/backend/apps/ocsp.c
WARNING  project         failed to build .angelix/backend/apps/openssl
INFO     inference       inferring specification for test '4'
INFO     testing         running test '4' of backend source with KLEE
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000003.smt2
WARNING  inference       choice instance 0 for variable actual_payload_len is missing
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
WARNING  inference       choice instance 0 for variable actual_payload_len is missing
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
WARNING  inference       choice instance 0 for variable actual_payload_len is missing
INFO     inference       found 0 angelic paths for test '4'
INFO     repair          considering suspicious expressions [(2415, 7, 2415, 7)]
INFO     reduction       selected 5 tests
INFO     reduction       selected passing tests: ['1', '6', '7']
INFO     reduction       selected failing tests: ['4', '8']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
INFO     project         building backend source
WARNING  project         compilation of .angelix/backend returned non-zero code
WARNING  project         failed to build .angelix/backend/apps/s_server.c
WARNING  project         failed to build .angelix/backend/apps/s_client.c
WARNING  project         failed to build .angelix/backend/apps/s_time.c
WARNING  project         failed to build .angelix/backend/apps/ocsp.c
WARNING  project         failed to build .angelix/backend/apps/openssl
INFO     inference       inferring specification for test '4'
INFO     testing         running test '4' of backend source with KLEE
INFO     inference       sleeping for 1 second...
WARNING  inference       No paths explored
INFO     repair          considering suspicious expressions [(2417, 6, 2417, 9)]
INFO     reduction       selected 5 tests
INFO     reduction       selected passing tests: ['1', '6', '7']
INFO     reduction       selected failing tests: ['4', '8']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
INFO     project         building backend source
WARNING  project         compilation of .angelix/backend returned non-zero code
WARNING  project         failed to build .angelix/backend/apps/s_server.c
WARNING  project         failed to build .angelix/backend/apps/s_client.c
WARNING  project         failed to build .angelix/backend/apps/s_time.c
WARNING  project         failed to build .angelix/backend/apps/ocsp.c
WARNING  project         failed to build .angelix/backend/apps/openssl
INFO     inference       inferring specification for test '4'
INFO     testing         running test '4' of backend source with KLEE
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       UNSAT
INFO     inference       found 0 angelic paths for test '4'
INFO     repair          considering suspicious expressions [(2422, 6, 2422, 39)]
INFO     reduction       selected 5 tests
INFO     reduction       selected passing tests: ['1', '6', '7']
INFO     reduction       selected failing tests: ['4', '8']
INFO     project         configuring backend source
INFO     transformation  instrumenting suspicious of backend source
INFO     project         building backend source
WARNING  project         compilation of .angelix/backend returned non-zero code
WARNING  project         failed to build .angelix/backend/apps/s_server.c
WARNING  project         failed to build .angelix/backend/apps/s_client.c
WARNING  project         failed to build .angelix/backend/apps/s_time.c
WARNING  project         failed to build .angelix/backend/apps/ocsp.c
WARNING  project         failed to build .angelix/backend/apps/openssl
INFO     inference       inferring specification for test '4'
INFO     testing         running test '4' of backend source with KLEE
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       expression (2422, 6, 2422, 39)[0]: angelic = False
INFO     testing         running test '4' of frontend source
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       UNSAT
INFO     inference       found 1 angelic paths for test '4'
INFO     inference       inferring specification for test '8'
INFO     testing         running test '8' of backend source with KLEE
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       expression (2422, 6, 2422, 39)[0]: angelic = False
INFO     testing         running test '8' of frontend source
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       UNSAT
INFO     inference       found 1 angelic paths for test '8'
INFO     inference       inferring specification for test '1'
INFO     testing         running test '1' of backend source with KLEE
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       UNSAT
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       expression (2422, 6, 2422, 39)[0]: angelic = True
INFO     testing         running test '1' of frontend source
INFO     inference       spurious angelic path
INFO     inference       found 0 angelic paths for test '1'
WARNING  repair          angelic forest for positive test 1 not found
INFO     inference       inferring specification for test '7'
INFO     testing         running test '7' of backend source with KLEE
INFO     inference       sleeping for 1 second...
INFO     inference       solving path .angelix/backend/klee-out-0/test000001.smt2
INFO     inference       expression (2422, 6, 2422, 39)[0]: angelic = False
INFO     testing         running test '7' of frontend source
INFO     inference       spurious angelic path
INFO     inference       solving path .angelix/backend/klee-out-0/test000002.smt2
INFO     inference       UNSAT
INFO     inference       found 0 angelic paths for test '7'
WARNING  repair          angelic forest for positive test 7 not found
INFO     synthesis       synthesizing patch with component level 'extended-arithmetic'
INFO     synthesis       fixing expression (2422, 6, 2422, 39): ((hbtype == 1) && (0 < 1)) ---> ((hbtype == 1) && (1025 < 1))
INFO     repair          candidate fix synthesized
INFO     transformation  applying patch to validation source
INFO     project         building validation source
INFO     testing         running test '1' of validation source
INFO     testing         running test '4' of validation source
INFO     testing         running test '6' of validation source
INFO     testing         running test '7' of validation source
INFO     testing         running test '8' of validation source
WARNING  repair          generated invalid fix (tests ['6'] not repaired)
INFO     repair          no patch generated in 3h 9m 9s

compiling failed

Installed all dependencies:

after make default obtained several compilation errors (attached is a log file)

some of these errors include

/home/stein/Desktop/Projects/angelix/build/llvm-2.9/include/llvm/Operator.h:209:7: error: deleted function ‘virtual llvm::GEPOperator::~GEPOperator()’ overriding non-deleted function 209 | class GEPOperator | ^~~~~~~~~~~

compilation.log

Support augmented assignments

Problem of reproducing the angelix test

Sorry for disturbing you with this question. I download the source code of Angelix and configure it as indicated by the README.md. However, I failed to reproduce all tests of Angelix and Semfix ( I configured Semfix also, with make semfix command). For example, the output of running make test-semfix is as follow:

dehengyang@dehengyang:~/Semifix/angelix-master$ . activate 
dehengyang@dehengyang:~/Semifix/angelix-master$ make test-semfix
python3 tests/semfix-tests.py
FF
====================================================================
FAIL: test_semfix (__main__.TestAngelix)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "tests/semfix-tests.py", line 36, in test_semfix
    self.assertEqual(result, 'SUCCESS')
AssertionError: 'FAIL' != 'SUCCESS'
- FAIL
+ SUCCESS


====================================================================
FAIL: test_semfix_synthesis (__main__.TestAngelix)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "tests/semfix-tests.py", line 42, in test_semfix_synthesis
    self.assertEqual(result, 'SUCCESS')
AssertionError: 'FAIL' != 'SUCCESS'
- FAIL
+ SUCCESS

----------------------------------------------------------------------
Ran 2 tests in 0.860s

FAILED (failures=2)
make: *** [test-semfix] Error 1

Then, I tried to explore the reasons why this failed. I reproduced the whole folder of distance.c according to the Tutorial.md. I run the command

. activate
bugs=distance
bugDir=/home/dehengyang/Semifix/angelix-master/tests/$bugs
cd $bugDir
angelix src distance.c oracle 1 2 3 --assert assert.json

However, angelix still failed to repair this bug. The output is:

INFO project configuring validation source
INFO project building json compilation database from validation source
INFO testing running test '1' of validation source
INFO testing running test '2' of validation source
INFO testing running test '3' of validation source
INFO project configuring frontend source
INFO transformation instrumenting repairable of frontend source
INFO project building frontend source
INFO repair running positive tests for debugging
INFO testing running test '1' of frontend source
INFO testing running test '2' of frontend source
INFO repair running negative tests for debugging
INFO testing running test '3' of frontend source
INFO localization selected expressions [(12, 14, 12, 19)] with group score 1.0
INFO localization selected expressions [(6, 14, 6, 19)] with group score 0.5
INFO localization selected expressions [(5, 9, 5, 14)] with group score 0.33333
INFO localization selected expressions [(9, 9, 9, 14)] with group score 0.33333
INFO localization selected expressions [(13, 9, 13, 14)] with group score 0.33333
INFO repair considering suspicious expressions [(12, 14, 12, 19)]
INFO reduction selected 1 tests
INFO reduction selected passing tests: []
INFO reduction selected failing tests: ['3']
INFO project configuring backend source
INFO transformation instrumenting suspicious of backend source
INFO project building backend source
INFO inference inferring specification for test '3'
INFO testing running test '3' of backend source with KLEE
INFO inference sleeping for 1 second...
WARNING inference No paths explored
INFO repair considering suspicious expressions [(6, 14, 6, 19)]
INFO reduction selected 1 tests
INFO reduction selected passing tests: []
INFO reduction selected failing tests: ['3']
INFO project configuring backend source
INFO transformation instrumenting suspicious of backend source
INFO project building backend source
INFO inference inferring specification for test '3'
INFO testing running test '3' of backend source with KLEE
INFO inference sleeping for 1 second...
WARNING inference No paths explored
INFO repair considering suspicious expressions [(5, 9, 5, 14)]
INFO reduction selected 1 tests
INFO reduction selected passing tests: []
INFO reduction selected failing tests: ['3']
INFO project configuring backend source
INFO transformation instrumenting suspicious of backend source
INFO project building backend source
INFO inference inferring specification for test '3'
INFO testing running test '3' of backend source with KLEE
INFO inference sleeping for 1 second...
WARNING inference No paths explored
INFO repair considering suspicious expressions [(9, 9, 9, 14)]
INFO reduction selected 1 tests
INFO reduction selected passing tests: []
INFO reduction selected failing tests: ['3']
INFO project configuring backend source
INFO transformation instrumenting suspicious of backend source
INFO project building backend source
INFO inference inferring specification for test '3'
INFO testing running test '3' of backend source with KLEE
INFO inference sleeping for 1 second...
WARNING inference No paths explored
INFO repair considering suspicious expressions [(13, 9, 13, 14)]
INFO reduction selected 1 tests
INFO reduction selected passing tests: []
INFO reduction selected failing tests: ['3']
INFO project configuring backend source
INFO transformation instrumenting suspicious of backend source
INFO project building backend source
INFO inference inferring specification for test '3'
INFO testing running test '3' of backend source with KLEE
INFO inference sleeping for 1 second...
WARNING inference No paths explored
INFO repair no patch generated in 5s
FAIL
(I am sorry that due to the problem of uploading the file, I copy the whole text of the output rather than upload a file.)
This output is quite different from the expected output given by Tutorial.md.

Much appreciated if any help is provided.

Empty trace files

I configured Angelix to run on sort.c of CoreUtils. Angelix runs through instrumentation, validation process, but after that it does not find any suspicious lines. I inspected the trace folder, which contains all the trace files, and I saw that all the trace files are totally empty. This seems strange because the trace files should not be empty. I would love to hear what could be the problem here?

Attached is the log file, and the instrumented input source code c file.

angelix-experiments.zip

Problem of generating the patch for tutorial folder

I have encountered a issue that angelix still fails to repair the bug even though I reproduced the whole folder of distance.c with four files in it by following the tutorial section. I am trying to find the reason why it fails.

Angelix could pass all tests by running "make test".

According to the tutorial, I reproduced four files and "distance.c","Makefile" are in the src folder.

The running command I use is "angelix src distance.c oracle 1 2 3 --assert assert.json". However, it fails to generate the expected patch.

Much appreciated if any help is provided. Thanks!

Error: make default

Dear Sir,
When I run ''make default'', I got the follwing message:

(base) root@iZbp179omj4oyxhfll6amcZ:/test/angelix# make default
cd build && wget --retry-connrefused --waitretry=1 --read-timeout=20 --timeout=15 --tries=5 --continue http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
/bin/sh: 1: cd: can't cd to build
Makefile:74: recipe for target 'build/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2' failed
make: *** [build/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2] Error 2
(base) root@iZbp179omj4oyxhfll6amcZ:/test/angelix#

make with multi-threaded fail

Hi Sergey,

After using the Dockerfile to build and enter the docker, run activate.
When I run make default, it failed with:

...
[ 95%] Building CXX object tools/clang/tools/libclang/CMakeFiles/libclang.dir/Indexing.cpp.o
[ 95%] Building CXX object tools/clang/tools/libclang/CMakeFiles/libclang.dir/IndexingContext.cpp.o
Linking CXX shared library ../../../../lib/libclang.so
collect2: error: ld terminated with signal 9 [Killed]
make[3]: *** [lib/libclang.so.3.7] Error 1
make[3]: Leaving directory /angelix/build/llvm-3.7.0.src/build' make[2]: *** [tools/clang/tools/libclang/CMakeFiles/libclang.dir/all] Error 2 make[2]: Leaving directory /angelix/build/llvm-3.7.0.src/build'
make[1]: *** [all] Error 2
make[1]: Leaving directory `/angelix/build/llvm-3.7.0.src/build'
make: *** [clang] Error 2

I run several times, but they failed not in the same position but all in 95%.

I delete the multi-threaded content in makefile

klee-uclibc: $(KLEE_UCLIBC_DIR)
	cd $(KLEE_UCLIBC_DIR) && ./configure --make-llvm-lib && make -j2

klee-uclibc: $(KLEE_UCLIBC_DIR)
	cd $(KLEE_UCLIBC_DIR) && ./configure --make-llvm-lib && make

It passed finally.
The similar issue came when I build the docker image, again failed at about 95%, so I have to delete the multi-threaded -j.
I don't know why multi-threaded make infects the results.

Support null-terminated strings for ANGELIX_OUTPUT

Downloading dependencies during docker build fails due to Java certificates

Use this answer: https://stackoverflow.com/a/50103533

What should I write in assert.json if the output includes string?

I saw all the example in tests. I find the results of all are numeric. What should I write if the result is not numeric?

Calling Angelix from the source directory causes crash

Angelix example from `Tutorial.md` fails to find a repair with `--instr-printf distance.c`

I'm currently working on this commit 01396ac20e1e973834d0fd4eccbc7e24216d37d0 [currently origin/master HEAD]
Angelix was successfully able to find a repair using the distance.c example from Manual.md, which contains some instrumentation.
When I stripped distance.c of the Angelix instrumentation and applied --instr-printf distance.c to the Angelix command line, Angelix was unable to find a repair.

Here is some preliminary debug info:
Looking at the differences between runs and Angelix log output, I'm seeing this in the --instr-printf angelix.log:
INFO inference value 'stdout' executed 0 times while 1 required

while diff'ing the backend/distance.c between the baseline (<) and instr-print (>), this difference is the culprit of the logfile's inference note:

1,3d0
< #include <stdio.h>
< #include <stdlib.h>
<
7a5,8
> #include <stdio.h>
> #include <stdlib.h>
>
>
17c18
<         dy = ANGELIX_CHOOSE(int, y1 - y2, 17, 14, 17, 19, ((char*[]){"y1", "y2"}), ((int[]){y1, y2}), 2);
---
>         dy = y1 - y2;
30c31
<     printf("%d\n", ANGELIX_OUTPUT(int, distance(x1, y1, x2, y2), "stdout"));
---
>     ({ if (ANGELIX_CHOOSE(bool, 1, 31, 12, 31, 12, ((char*[]){"y1", "x1", "x2", "y2"}), ((int[]){y1, x1, x2, y2}), 4)) printf("%d\n", ANGELIX_OUTPUT(int, distance(x1, y1, x2, y2), "angelixVar11")); });

https://git.llvm.org/git/clang-tools-extra not accessible

https://git.llvm.org/git/clang-tools-extra is no more accessible.

In Makefile, CLANG_TOOLS_EXTRA_URL should be changed to the following:

CLANG_TOOLS_EXTRA_URL=https://github.com/llvm-mirror/clang-tools-extra.git

Can't pass the tutorial test

Hi Sergey,

After I setting up the oracle, assert.json, src/distance.c, src/Makefile from the tutorial, I run angelix /angelix/test/src distance.c oracle 1 2 3 --assert assert.json --verbose
and it shows:

root@9f2c2b97a49e:/angelix/test# angelix /angelix/test/src distance.c oracle 1 2 3 --assert assert.json --verbose
INFO repair option group_by_score = False
INFO repair option klee_max_depth = None
INFO repair option path_solving_timeout = 60000
INFO repair option synthesis_ptr_vars = False
INFO repair option redundant_test = False
INFO repair option ignore_infer_errors = False
INFO repair option instr_printf = None
INFO repair option defect = ['if-conditions', 'assignments']
INFO repair option synthesis_bool_only = False
INFO repair option synthesis_func_params = False
INFO repair option mute_test_message = False
INFO repair option max_z3_trials = 2
INFO repair option localize_from_bottom = False
INFO repair option initial_tests = 1
INFO repair option synthesis_timeout = 30000
INFO repair option mute_warning = False
INFO repair option semfix = False
INFO repair option klee_timeout = None
INFO repair option ignore_trans_errors = False
INFO repair option build_before_instr = False
INFO repair option max_angelic_paths = None
INFO repair option invalid_localization = False
INFO repair option synthesis_used_vars = True
INFO repair option group_size = 1
INFO repair option init_uninit_vars = False
INFO repair option synthesis_global_vars = False
INFO repair option all_tests = False
INFO repair option localization = jaccard
INFO repair option klee_ignore_errors = False
INFO repair option mute_build_message = False
INFO repair option ignore_trivial = False
INFO repair option klee_max_forks = None
INFO repair option klee_solver_timeout = None
INFO repair option verbose = True
INFO repair option klee_debug = False
INFO repair option test_timeout = None
INFO repair option use_nsynth = False
INFO repair option localize_only = False
INFO repair option synthesis_levels = ['alternatives', 'integer-constants', 'boolean-constants']
INFO repair option suspicious = 20
INFO repair option generate_all = False
INFO repair option klee_search = None
INFO repair option use_semfix_syn = False
INFO project configuring validation source
INFO project building json compilation database from validation source
make: distance' is up to date. INFO testing running test '1' of validation source INFO testing running test '2' of validation source INFO testing running test '3' of validation source INFO project configuring frontend source INFO transformation instrumenting repairable of frontend source Skipping /angelix/test/.angelix/frontend/distance.c. Compile command not found. INFO project building frontend source make: distance' is up to date.
INFO repair running positive tests for debugging
INFO testing running test '1' of frontend source
INFO testing running test '2' of frontend source
INFO repair running negative tests for debugging
INFO testing running test '3' of frontend source
INFO repair repair test suite: ['1', '2', '3']
INFO repair validation test suite: ['1', '2', '3']
WARNING repair no suspicious expressions localized
INFO repair no patch generated in 0s
FAIL

No idea where gets wrong.

Boyang

pku-msv-lab / angelix Goto Github PK

angelix's Introduction

Angelix

Installation

Option 1: VirtualBox image

Option 2: Build from source

Documentation

Changelog

1.1 (2017-Mar-20)

1.0 (2016-Jul-8)

icse16 (2016-Feb-19)

Publications

Contributors

angelix's People

Contributors

Stargazers

Watchers

Forkers

angelix's Issues

Recommend Projects

Recommend Topics

Recommend Org