mattulbrich / llreve Goto Github PK

Shouldn't reve be able to handle endless loops?

The horn clauses for the following programs are sat, which should not be the case.

extern int __mark(int i);

int foo(){
    int i = 0;
    int a = 0;
    while (__mark(1) & (i < 4)) {
        a++;
        i++;
    }
    return a;
}

extern int __mark(int i);

int foo(){
    int i = 0;
    int a = 0;
    while (__mark(1) & (i < 4)) {
        a++;
    }
    return a;
}

Input C file contents-
#include <stdio.h> int main(){ printf("hello"); return 0; }
and
#include <stdio.h> int main(){ printf("bye"); return 0; }

./llreve -I /usr/lib/gcc/x86_64-linux-gnu/7/include/ " + "./"+file+ " ./teacher_solution.c -o reve.smt2
Output-
(set-logic HORN) (define-fun .str$1 () Int (- 5)) (define-fun .str$2 () Int (- 5)) (define-fun INV_REC_printf^printf ((_$1_0 Int) (_$2_0 Int) (result$1 Int) (result$2 Int)) Bool (=> (= _$1_0 _$2_0) (= result$1 result$2))) (define-fun INV_REC_printf__1 ((_$1_0 Int) (result$1 Int)) Bool true) (define-fun INV_REC_printf__2 ((_$2_0 Int) (result$2 Int)) Bool true) (define-fun IN_INV () Bool true) (define-fun OUT_INV ((result$1 Int) (result$2 Int)) Bool (= result$1 result$2)) (assert (forall ((call$1_0 Int) (call$2_0 Int)) (=> (INV_REC_printf^printf (+ .str$1 (* 4 0) 0) (+ .str$2 (* 6 0) 0) call$1_0 call$2_0) (let ((result$1 0) (result$2 0)) (OUT_INV result$1 result$2))))) (check-sat) (get-model)

./z3 fixedpoint.engine=duality -T:300 reve.smt2
Output-
sat (model (define-fun @Fail!0 () Bool false) )

@steohan, consider this program. After running the SyntacticSlicePass and the SlicingPass the program looks this way:

define i32 @foo(i32 %a) #0 !dbg !4 {
%1 = add nsw i32 0, 1, !dbg !11, !sliced !12
%2 = icmp eq i32 %a, 0, !dbg !13, !sliced !12
br i1 %2, label %3, label %5, !dbg !15, !sliced !12

; (label):3 ; preds = %0
%4 = add nsw i32 %1, 2, !dbg !16, !sliced !12
br label %7, !dbg !18, !sliced !12

; (label):5 ; preds = %0
%6 = add nsw i32 %1, 3, !dbg !19, !sliced !12
br label %7, !sliced !12

; (label):7 ; preds = %5, %3
%i.0 = phi i32 [ %4, %3 ], [ %6, %5 ], !sliced !12
%8 = add nsw i32 %i.0, 4, !dbg !21, !sliced !12
%9 = add nsw i32 %8, 5, !dbg !22, !sliced !12
%10 = icmp eq i32 %a, -1, !dbg !23
br i1 %10, label %11, label %13, !dbg !25

; (label):11 ; preds = %7
%12 = sub nsw i32 %a, 0, !dbg !26
br label %15, !dbg !28

; (label):13 ; preds = %7
%14 = sub nsw i32 %a, -2, !dbg !29
br label %15

; (label):15 ; preds = %13, %11
%.0 = phi i32 [ %12, %11 ], [ %14, %13 ]
ret i32 %.0, !dbg !31
}

So there are still instructions left, that should be sliced, but the SlicingPass didn't remove them. Only the immediate predecessor of the return instruction has been removed. Is there any reason for this bevavior?

Z3 returns sat here while we would expect unsat. Not yet sure what’s going on here. The generated SMT looks correct.

http://formal.iti.kit.edu/llreve

If -init-pred is used as command-line parameter, the program produces illegal SMT2 code which has nested assert commands.

(assert
   (assert
      (forall
         ((n$1_0 Int)
          (n$2_0 Int))
         (=>
            (IN_INV n$1_0 n$2_0)
            (INIT n$1_0 n$2_0)))))

@cocreature I've merged the master branch into the slicing branch to get INIT predicate changes. Now I get errors when executing CMake. The variable Z3_LIBRARIES (ADVANCED) is set to NOTFOUND. I have currently no Z3 implementation in the Rêve folder. Do I need one or should I use the CMake files from an older version?

@steohan I get an assertion failure when using programs with pointers:

int foo(int x) {
int* a = &x;
return x;
}

The failure is:
slicing: /usr/local/include/llvm/Support/Casting.h:95: static bool llvm::isa_impl_cl<llvm::Instruction, const llvm::Value *>::doit(const From *) [To = llvm::Instruction, From = const llvm::Value *]: Assertion 'Val && "isa<> used on a null pointer"' failed.

Any ideas, what causes the problem? It's probably one of the preprocessing passes because Rêve works on this program. When assigning the null pointer to 'a' everything works just fine.

Stephan wrote:

Bei dem Beispiel beschwert sich Z3 über die syntax
(invalid function application, arguments missing)

int f() {
    int x = 0;
    return x;
}

(Issue added to prove the issue tracker alive. ...)

Could Reve support marks without loops? At the moment the following example causes a malformed smt file:

extern int __mark(int);

int foo(int result) {
    result += 1;
    __mark(1);
    result += 2;
    return result;
}

Current workaround is

    while (__mark(1) & 0){};

Some source files include the header file 'unistd.h' which is only available on UNIX systems. Is this file really necessary for rêve to work?

The generation of the smt file is not working properly for the attached source, compared with it self:

./reve test.c test.c > test.smt2; eld test.smt2

Results in the error Symbol -1 not declared. Removing any line does not result in the error.

test.c:

extern int foo();

int
main (int argc, char **argv)
{
  int a = 0;
  int nproc, ignore = 0;
      int c = foo();
      if (c == -1)
        return 1;
      if (c == 12)
        ignore = 42;

  nproc = ignore;
  return 0;
}

Extern functions include implications. This results in non-Horn clauses being output which Z3 does not handle correctly.

@cocreature I've tested the option -init-pred directly in command line and it works. However, when invoking Rêve via the API the option seems to be ignored. I added the option the following way:

SMTGenerationOpts &smtOpts = SMTGenerationOpts::getInstance();
smtOpts.PerfectSync = true;
smtOpts.InitPredicate = true;

Am I missing anything? When running the slicing program, there is no INIT predicate in the resulting SMT file.

@cocreature while adding our project, I also did some changes to include libreve without add_subdirectory, as this may cause trubles. Have a look at llreve/slicing/src/CMakeLists.txt

This is only for including from a build path.

Hej,

I tried to use the llreve-dyamic tool on the following example:

extern int __mark(int);

void send(int *to, int *from, int count)
{
    do {                          /* count > 0 assumed */
        *to = *from++;
    } while(__mark(1) & (--count > 0));
}
extern int __mark(int);

and

void send(int *to, int *from, int count)
{
    int n = (count + 7) / 8;
    switch (count % 8) {
    case 0: do { *to = *from++;
    case 7:      *to = *from++;
    case 6:      *to = *from++;
    case 5:      *to = *from++;
    case 4:      *to = *from++;
    case 3:      *to = *from++;
    case 2:      *to = *from++;
    case 1:      *to = *from++;
            } while (__mark(1) & (--n > 0));
    }
}

which are duff1.c and duff2.c. Invoking llreve-dynamic gives a seg fault.

$ ./llreve-dynamic -patterns ../../patterns/looppatterns ~/duff1.c ~/duff2.c 
Found 4 patterns
(_ ≥ _)
(_ > _)
(_ < 0)
(_ ≥ 0)
MAIN: 1
startMark: -1
endMark: 0
function 1: send
function 2: send
---
Found counterexample:
starting at mark -1
ending at mark 0
 5
 5
HEAP$1_old
background: 0
HEAP$2_old
background: 0
llreve-dynamic: /home/ubuntu/src/llreve/reve/dynamic/llreve-dynamic/include/llreve/dynamic/Integer.h:69: Integer &Integer::operator+=(const Integer &): Assertion `type == other.type' failed.
Aborted (core dumped)

Some headers are usually only available as builtin includes (p.a. stddef.h, limits.h). And may not be found during the execution of reve. This prevents the analysis of real world programs.

A possible but bad solution would be to hard code the resource directory. See 742c868.

The following example does not produce a result in reasonable time using eldarica. The smt file locks fine to me (please double check), so it is probably a bug in eldarica. (Z3 returns unknown)

The example:

int foo(int a, int b){
    return 0;
}

int foo(int a, int b){
    return a * b;
}

The produced SMT:

(set-logic HORN)
(define-fun
   IN_INV
   ((a$1_0 Int)
    (b$1_0 Int)
    (a$2_0 Int)
    (b$2_0 Int))
   Bool
   (and
      (= a$1_0 a$2_0)
      (= b$1_0 b$2_0)))
(define-fun
   OUT_INV
   ((result$1 Int)
    (result$2 Int))
   Bool
   (= result$1 result$2))
(assert
   (forall
      ((a$1_0_old Int)
       (b$1_0_old Int)
       (a$2_0_old Int)
       (b$2_0_old Int))
      (=>
         (IN_INV a$1_0_old b$1_0_old a$2_0_old b$2_0_old)
         (let
            ((a$1_0 a$1_0_old)
             (b$1_0 b$1_0_old)
             (result$1 1)
             (a$2_0 a$2_0_old)
             (b$2_0 b$2_0_old))
            (let
               ((_$2_0 (* a$2_0 b$2_0)))
               (let
                  ((result$2 _$2_0))
                  (OUT_INV result$1 result$2)))))))
(check-sat)

Trace example fails on https://formal.kastel.kit.edu/projects/improve/reve/?ex=redis%2Ftrace with missing header:

/tmp/prog110123-1566.c:1:10: fatal error: 'lua.h' file not found
#include <lua.h>
         ^~~~~~~
1 error generated.
ERROR: Couldn’t execute action

@steohan I applied CGS to the benchmark example 'requires_path_sensitivity.c' and as there is a criterion at an intermediate location I think the return statement shouldn't be part of the slice. The control flow doesn't change when removing the return statement. IAA keeps the statement and CGS wants to remove it, but the slice candidate validation doesn't consider it a valid slice and CGS crashes because it gets a new counterexample that doesn't add more statements to the slice and thus doesn't generate a new candidate.

I talked today with Mattias and Vladimir about open sourcing llrêve/this repo and we considered the BSD3 license and the University of Illinois/NCSA Open Source License (used by LLVM). They seem to be identical (even the wording is identical in the three clauses) and since BSD3 is wider known (at least in my filterbubble) I would go with that.

@steohan and @Lein4d need to either agree to the BSD3 license or we make it clear that your code is not licensed under an open source license.

Once that is done I’ll add the license to the repo. @mattulbrich also needs to pull the trigger to make it public which can happen either before or after a license is added.

And in case anyone is wondering, we are linking against LLVM, Z3 and the tools for my bachelorthesis are linking against libgmp and include https://github.com/nlohmann/json. None of this contradicts a BSD3 license.