TrustInSoft / tis-interpreter

An interpreter for finding subtle bugs in programs written in standard C
565 stars 28 forks source link

How to catch issues when using tis-interpreter.sh #143

Open sijohans opened 6 years ago

sijohans commented 6 years ago

Hello,

I have a parser and a lot of generated test cases. Every test case have it's own main entry point. How do i catch issues/errors from tis-interpreter.sh?

I have a script similar to:

#!/bin/sh

for file in $(find generated_test_cases -type f -name '*.c');
do
    echo "tis-interpreter analyzing file: $file"
    if ! output=$(/home/developer/tis-interpreter/tis-interpreter.sh my_parser.c $file --cc "-I."); then
        echo "File $file had some problems:"
        echo $output
        exit 1
    fi
done

exit 0

However, the tis-interpreter.sh script always returns 0 even if i add a bug in the code. Are there any other ways of catching this?

pascal-cuoq commented 6 years ago

Hello,

it should already be the case that the tis-interpreter.sh script returns 2 when it finds an undefined behavior. Here is what I get when I test it:

~ $ cat t.c
int main(void) {
  int x = 1;
  x--;
  x = 100 / x;
  x++;
  return 0;
}
~ $ cat t_ok.c
int main(void) {
  int x = 2;
  x--;
  x = 100 / x;
  x++;
  return 0;
}
~ $ tis-interpreter.sh t_ok.c ; echo Return code: $?
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] done for function main
Return code: 0
~ $ tis-interpreter.sh t.c ; echo Return code: $?
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
t.c:4:[kernel] warning: division by zero: assert x ≢ 0;
                  stack: main
[value] Stopping at nth alarm
Return code: 2
~ $ 

Do you get the same behavior as above? What kind of bug are you adding to a C file in order to test your script?

sijohans commented 5 years ago

It seemed to be a warning that was harmless. However, i tested adding:

    int x = 1;
    x--;
    x = 100 / x;
    x++;

To one of my test cases, it doesn't stop on that one. I get the same output from your instructions, but it won't return 2. I also realize i used the 2016-05 linux binary snapshot: http://trust-in-soft.com/tis-interpreter-2016-05.linux-x86_64.tar.gz

Perhaps this feature was added later, in that case this issue should be closed and i'll have to build a fresh one.

sijohans commented 5 years ago

The return code of the snapshot is not 0 when crashes/problems are found. Are there any plans on making a new snapshot from the current sources?

(I had problem building it on my arch linux machine)