jburnim / crest Goto Github PK

CREST is a concolic test generation tool for C.

Home Page: http://jburnim.github.io/crest/

License: BSD 2-Clause "Simplified" License

C 51.34% Shell 0.84% C++ 1.91% Awk 0.21% Perl 0.60% IDL 0.12% OCaml 24.94% Makefile 2.19% Batchfile 0.01% DIGITAL Command Language 0.01% XS 0.16% Prolog 0.61% GDB 0.01% M4 0.09% Standard ML 0.17% Roff 0.88% Vim Script 15.92%

crest's Introduction

CREST

CREST is a concolic test generation tool for C.

Thanks for downloading and trying out CREST.

You can get the latest version of CREST, as well as news and announcements at CREST's homepage: https://burn.im/crest .

If you want to cite CREST, please refer to the (short) paper: Burnim, Sen, "Heuristics for Dynamic Test Generation", Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2008.

You can find a list of papers using CREST at https://burn.im/crest/#publications .

NOTE: CREST is no longer being actively developed, but questions are still answered on the CREST-users mailing list -- [email protected] and https://groups.google.com/forum/#!forum/crest-users .

Preparing a Program for CREST

To use CREST on a C program, use functions CREST_int, CREST_char, etc., declared in "crest.h", to generate symbolic inputs for your program. For examples, see the programs in test/.

For simple, single-file programs, you can use the build script "bin/crestc" to instrument and compile your test program.

CREST can be used to instrument multi-file programs, too -- instructions may be added later. In the meantime, you can take a look at an example, instrumented form of grep-2.2, available at https://github.com/jburnim/crest/tree/master/benchmarks/grep-2.2 . For further information, please see this post on the CREST-users mailing list.

Running Crest

CREST is run on an instrumented program as:

bin/run_crest PROGRAM NUM_ITERATIONS -STRATEGY

Possibly strategies include: dfs, cfg, random, uniform_random, random_input. Some strategies take optional parameters.

Example commands to test the "test/uniform_test.c" program:

cd test
../bin/crestc uniform_test.c
../bin/run_crest ./uniform_test 10 -dfs

This should produce output roughly like:

... [GARBAGE] ...
Read 8 branches.
Read 13 nodes.
Wrote 6 branch edges.

Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 1 branches [1 reach funs, 8 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 8 reach branches].
Iteration 3 (0s): covered 5 branches [1 reach funs, 8 reach branches].
Iteration 4 (0s): covered 7 branches [1 reach funs, 8 reach branches].
GOAL!
Iteration 5 (0s): covered 8 branches [1 reach funs, 8 reach branches].

NOTE: run_crest and crestc currently leave a lot of files lying around, some of which are temporary and some of which must be kept. In particular, "cfg_branches" and "branches" are output by the instrumentation process and are needed to run run_crest, and run_crest produces "coverage", a list of the ID's of all covered branches.

Setup

CREST depends on Yices 1, an SMT solver tool and library available at http://yices.csl.sri.com/old/download-yices1.shtml. To build and run CREST, you must download and install Yices version 1 and change YICES_DIR in src/Makefile to point to Yices location.

CREST uses CIL to instrument C programs for testing. A modified distribution of CIL is included in directory cil/. To build CIL, simply run "configure" and "make" in the cil/ directory.

Finally, CREST can be built by running "make" in the src/ directory.

License

CREST is distributed under the revised BSD license. See LICENSE for details.

This distribution includes a modified version of CIL, a tool for parsing, analyzing, and transforming C programs. CIL is written by George Necula, Scott McPeak, Wes Weimer, Ben Liblit, and Matt Harren. It is also distributed under the revised BSD license. See cil/LICENSE for details.

crest's People

Contributors

Stargazers

Watchers

Forkers

jusmarge cherry-wb zlqhem ramymibrahim yongbol haowai31 imu2008 ssthappy terry2012 linearregression scoutzhang anirudh-kabde faith1985rjy kren1 leima-hit naloboud lembergerth jeremyku99 posticarus fuzzamos masterhung0112 kariosm kkomdal sosy-lab hansolchoe arise-handong pcshark ck624 archerplus ewenwan imtiazkarimik23 jkunlin ganeshsankaran princeb3n yijiangtian yongwoo36 varshasuresh91 canliture ruddhowl lancherba repchain-group xiaozhouqi git45016683 linuer dimied h-mole

crest's Issues

Question about kMinValue array

Hello, I have been modified yicies_solver for my term project.

I found that kMinValue[0](Minimum value of U_CHAR) does not give me correct value(0)

for(size_t i = 0 ; i < 1 ; ++i)
{
    fprintf(stdout, "\tkMinValue[%u, %s]: %lld\n", i, type_names[i], kMinValue[i]);
    fprintf(stdout, "\tkMaxValue[%u, %s]: %lld\n", i, type_names[i], kMaxValue[i]);
}

from above codes,
I saw the result live below
I know that kMaxValue is initialized at basic_types.cc as numeric_limits::min()
but I wonder why I got the wrong result.

kMinValue[0, U_CHAR]: 154468404
kMaxValue[0, U_CHAR]: 255

Thanks.

return struct crestc error

Compiling

struct a {
  char const b;
} g_1782;
struct a c() {
  for (;;)
    return g_1782;
}
int main() {  }

With crestc gives me

test7.c: In function ‘c’:
test7.c:6:15: error: assignment of read-only variable ‘__retres1’
     return g_1782;

Is this some sort of instrumentation bug?

Stuck during compilation

Hi,
I am trying to run an example from the repo but I'm getting stuck during the first compilation step:

../bin/crestc uniform_test.c
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/ruraj/src/opensource/crest/cil/bin/cilly.native --out ./uniform_test.cil.c --doCrestInstrument ./uniform_test.i

I've left it running for hours with no results. Any ideas?

Error while compiling CREST : base/basic_types.cc

Hello,
I'am starting using CREST but as subject, I have a problem of "narrowing conversion" as follow

vagrant@vagrant:~/vagrant_data/tools/jburnim-crest-f5ff7fc/src$ make
g++ -I. -I../../yices-1.0.40/include -Wall -O2 -c -o base/basic_types.o base/basic_types.cc
base/basic_types.cc:96:1: error: narrowing conversion of '18446744073709551615u' from 'long unsigned int' to 'crest::value_t {aka long long int}' inside { } [-Wnarrowing]
};
^
base/basic_types.cc:96:1: error: narrowing conversion of '18446744073709551615ull' from 'long long unsigned int' to 'crest::value_t {aka long long int}' inside { } [-Wnarrowing]
: recipe for target 'base/basic_types.o' failed
make: *** [base/basic_types.o] Error 1

How is it? Does anyone have same problem?

I'm using Lubuntu 16.10, running on VM.

Thank you for your help.
uwevil

How to use CREST with muti-files program?How to build the executable program?

/home/yzb/Downloads/crest-master/benchmarks/grep-2.2/src/grep.c:112: undefined reference to __CrestChar' /home/yzb/Downloads/crest-master/benchmarks/grep-2.2/src/grep.c:112: undefined reference to __CrestChar'
grep_comb.o: In function main': /home/yzb/Downloads/crest-master/benchmarks/grep-2.2/src/grep.c:957: undefined reference to __CrestChar'
collect2: error: ld returned 1 exit status
make: *** [grep] Error 1
Could anyone tell me how to fix this problem?I can get the grep_comb.c，but failed to make the executable grep.
@jburnim

Make doesn't work at src/

How can I solve it?

structs with non 32bit width

I think I found another issue with crest when dealing with bit fields.

Given a program like:

struct {
  unsigned a : 16;
} b = {1};
int d;

int main() {
  if (b.a < -1) {
    d = 9;
  }
  printf("d: %d\n",d);
}

Crest outputs d: 9, while the correct output should clearly be d: 0. Interestingly if the width of a is changed to 32, the bug disappears. Any other width but 32, shows the error.

big integer in condition bug

If I compile and run

#include <crest.h>
unsigned int a;
int main() {
    __CrestUInt(&a);
    printf("a: %d\n",a);
    if( a < 4294967295) {
        exit(0);
    }
}

with something like crestc example.c && run_crest ./example 1000 -dfs

I get

Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
a: 1058183384
Iteration 1 (0s): covered 1 branches [1 reach funs, 2 reach branches].
a: 0
Iteration 2 (0s): covered 1 branches [1 reach funs, 2 reach branches].
Prediction failed!

So what I assume is happening is that in iteration 1 a path that skips the if is meant to be taken, but a gets set to 0 for some reason, so the path with the if is taken again which causes the prediction failed. This behaviour can be observed for quite a while, for example it happens if the constant is 2294967295 and disappears by the time it is 1294967295.

Is this a real bug or some known limitation?

Exploring the same branch twice

Given this program:

unsigned int a, b;

int main() {
  __CrestUInt(&a);
  if( a < 1 || a > 1) {
    exit(0);
  }
  (-1 > a ) || b;

  printf("g_4: %d\n", a);
}

I would expect crest to explore 3 branches, printing "g_4: 1" once, however I get:

Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 2 branches [1 reach funs, 8 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 3 (0s): covered 5 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 4 (0s): covered 5 branches [1 reach funs, 8 reach branches].
Prediction failed!

Error when trying to run test: uniform_test.c

Hi,
So I'm trying to run the test program just to make sure crest is functioning and keep getting the error:
uniform_test.c:12:19: error: crest.h: No such file or directory
Where is crest.h supposed to be located?
and also will this program work with bam, fasta, sam, or fastq files at all?
Thanks in advance,
Ram Ayyala

Question about running example uniform.c

Hi, I just tried to run crest with uniform.c example, it successfully read branches and write branches, but it just stopped without iteration, and also no error message showed. The output message is shown below:

yh570:~/crest/test$ ../bin/crestc uniform_test.c
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/yh570/crest/cil/bin/cilly.native --out ./uniform_test.cil.c --doCrestInstrument ./uniform_test.i
gcc -D_GNUCC -E -I../bin/../include ./uniform_test.cil.c -o ./uniform_test.cil.i
gcc -D_GNUCC -c -I../bin/../include -o ./uniform_test.o ./uniform_test.cil.i
uniform_test.c:16:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   16 |   int a, b, c, d;
      | ^ ~~~~
uniform_test.c:17:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   17 |   CREST_int(a);
      | ^ ~~~~
uniform_test.c:18:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   18 |   CREST_int(b);
      | ^ ~~~~
uniform_test.c:19:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   19 |   CREST_int(c);
      | ^ ~~~~
uniform_test.c:20:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   20 |   CREST_int(d);
      | ^ ~~~~
uniform_test.c:21:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   21 | 
      | ^     
uniform_test.c:22:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   22 |   if (a == 5) {
      | ^ ~~~~
uniform_test.c:23:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   23 |     if (b == 19) {
      | ^   ~~
uniform_test.c:24:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   24 |       if (c == 7) {
      | ^     
uniform_test.c:25:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
   25 |         if (d == 4) {
      | ^     
../bin/../include/crest.h:202:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
  202 | EXTERN void __CrestInt(int* x) __SKIP;
      | ^~~~~~
gcc -D_GNUCC -o uniform_test -I../bin/../include ./uniform_test.o -L../bin/../lib -lcrest -lstdc++
Read 8 branches.
Read 13 nodes.
Wrote 6 branch edges.
yh570:~/crest/test$

Would you please help me solve this issue? Thank you.

Error while installing CREST (yices_c.h: No such file or directory)

Brief description: Fatal error message is displayed while installing CREST

Steps to reproduce:

Download and install Yices 2.2.2
Change YICES_DIR in src/Makefile to point to Yices location
Build CIL by running "configure" and "make" in the cil/ directory
Try to build CREST by running "make" in the src/ directory

Expected results:

CREST should be properly build after step #4.

Actual result:

A fatal error message is displayed stating that yices_c.h cannot be found (fatal error: yices_c.h: No such file or directory)
This is the complete error message:

g++ -I. -I/home/user/Downloads/yices-2.2.2/include -Wall -O2   -c -o base/yices_solver.o base/yices_solver.cc
base/yices_solver.cc:17:21: fatal error: yices_c.h: No such file or directory
 #include <yices_c.h>
                     ^
compilation terminated.
make: *** [base/yices_solver.o] Error 1

Environment information:

Ubuntu 14.04 (64-bit)
Crest 0.1.2
Yices 2.2.2

Additional information:

It seems that this issue has been already reported at google code page for the CREST project (Issue 22) since May, 2014.

CREST isn't detecting GCC.

I was trying to run ../bin/crestc uniform_test.c and it shows this error

Cannot find GNUCC version

bits/libc-header-start.h

/usr/include/stdio.h:27:10: fatal error: bits/libc-header-start.h: No such file or directory
#include <bits/libc-header-start.h>
^~~~~~~~~~~~~~~~~~~~~~~~~~

on Ubuntu 18 64 bits

I had to install 32 bit compatibility library.

Unable to build CIL due to unbound module Big_int

Running

cd cil
./configure
make

fails with

make[1]: Leaving directory '/home/sam/Downloads/test2/test/crest/cil'
+ ocamlc.opt -c -I src -I ocamlutil -I src/frontc -I src/ext -I src/ext/pta -o src/cilint.cmi src/cilint.mli
+ ocamlc.opt -c -I src -I ocamlutil -I src/frontc -I src/ext -I src/ext/pta -o src/cilint.cmi src/cilint.mli
File "src/cilint.mli", line 6, characters 36-51:
6 | type cilint = Small of int | Big of Big_int.big_int
                                        ^^^^^^^^^^^^^^^
Error: Unbound module Big_int
Command exited with code 2.
make: *** [Makefile:79: _build/src/cil.cma] Error 10

Note, I am using OCaml version 4.12.1.

Prediction failed #2

I've encountered another prediction failed issue, it looks very different from the other one to me. Running:

unsigned short a = 0;
unsigned char b = 1;

void main() {
  __CrestUShort(&a);
  __CrestUChar(&b);
  int ak = --b;
  a && 0;
  ak >= 2 || 0;
}

with the latest crest(3e5ecec) gives me:

Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 2 branches [1 reach funs, 4 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 4 reach branches].
Iteration 3 (0s): covered 3 branches [1 reach funs, 4 reach branches].
Prediction failed!
Iteration 4 (0s): covered 3 branches [1 reach funs, 4 reach branches].
Prediction failed!

Any insight into this bug would be greatly appreciated.