wp-interpolation on single dimension arrays

[rasoolmaghareh]

@xuanlinhha, let's uncomment our old code on wp-interpolant on arrays.

This is a sample test program. If we had sum += v * x; then the wp-interpolant works correctly. But when having sum += v * weight[x]; the wp-interpolant is not generated. Can you kindly start working on this and let me know if you face any issues:

#include <klee/klee.h>

#define N 10
#define BOUND 66
int sum = 0;
int weight[] = {0,1,2,3,4,5,6,7,8,9,10};
int GOAL = 0;

int choice(int z, int flip) {
    if (z != 1) z=0; 
    else z = 1;                                                                       
    return z;
}

int main() {
       int x = 0;
       for (x = 1; x<=N; x++) { // can choose in another order
           int v;
           klee_make_symbolic(&v, sizeof(unsigned), "v");
           v = choice(v, 0); 
           sum += v * weight[x];
           klee_assert(sum<=BOUND);
       }
}

[rasoolmaghareh]

Output without array:

KLEE: done: total instructions = 943
KLEE: done: completed paths = 20, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 10
KLEE: done:     average branching depth of subsumed paths = 6
KLEE: done:     average instructions of completed paths = 471.5
KLEE: done:     average instructions of subsumed paths = 251.5
KLEE: done:     subsumed paths = 18
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2

Output with array:

KLEE: done: total instructions = 12143
KLEE: done: completed paths = 260, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 10
KLEE: done:     average branching depth of subsumed paths = 8.5
KLEE: done:     average instructions of completed paths = 375.087
KLEE: done:     average instructions of subsumed paths = 294
KLEE: done:     subsumed paths = 168
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 92

[xuanlinhha]

on which branch do you run this example? is it master?

[rasoolmaghareh]

no the wp-interpolant branch.

[xuanlinhha]

@rasoolmaghareh I don't remember the old code on wp-interpolant on arrays you mentioned. Could you show me where it is?

[xuanlinhha]

I see this function generateExprFromOperand cannot generate WPExpr for load instruction with GPE:

%13 = load i32* %12, align 4, !dbg !144
%12 = getelementptr inbounds [11 x i32]* @weight, i32 0, i64 %11, !dbg !144

The result of this: std::pair<ref<Expr>, ref<Expr> > pair = getPointer(parentGEP); is a pair of null values.

assembly.txt

[rasoolmaghareh]

I had intentionally stopped those codes. Please remove these lines to activate the previous codes:

In TxWeakestPreCondition::getConstantExpr:

  // klee_warning("PUSHUP1");
  return result;

In TxWeakestPreCondition::getPointer:

  // klee_warning("PUSHUP3");
  return pair;

In TxWeakestPreCondition::getLoadGep:

  // klee_warning("PUSHUP4");
  return result;

In TxWeakestPreCondition::getGepInst please uncomment these codes:

  gep->dump();
  if (gep->getNumOperands() == 2){
          gep->getOperand(0)->dump();
          gep->getOperand(1)->dump();
          ref<Expr> offset = this->generateExprFromOperand(gep->getOperand(1));
          offset->dump();
          result = this->generateExprFromOperand(gep->getOperand(0));
  }*/
  // klee_warning("PUSHUP5");
  return result;

[xuanlinhha]

When we call this function instantiateWPatSubsumption to create WP from dependency (Sel < (WPVar weight)> [ (SExt w64 (WPVar w32 (x)))] ) The (WPVar w32 (x)) is 10 but there are only 9 elements in the dependency, the weight has 11 elements, it losts 2 elements. So when running to this function: TxStore::find(ref<TxAllocationContext> alc, ref<Expr> offset) the returned entry is null and we have error So why we have only 9 elements

[rasoolmaghareh]

Can you post the state of the path just before this subsumption check. You can use -debug-state=3

[xuanlinhha]

(Sel < (WPVar weight)> [ (SExt w64 (WPVar w32 (x)))] )
kids[0] = (WPVar weight)
kids[1] = 10
offset = 40
path condition = [
        (Eq 1
     (ReadLSB w32 0 v_9)),
        (Eq 1
     (ReadLSB w32 0 v_1)),
        (Eq 1
     (ReadLSB w32 0 v_2)),
        (Eq 1
     (ReadLSB w32 0 v_6)),
        (Eq 1
     (ReadLSB w32 0 v_7)),
        (Eq 1
     (ReadLSB w32 0 v_5)),
        (Eq 1
     (ReadLSB w32 0 v_4)),
        (Eq 1
     (ReadLSB w32 0 v_3)),
        (Eq false
     (Eq 1
         (ReadLSB w32 0 v_8))),
        (Eq 1
     (ReadLSB w32 0 v))]

When I declare array weight as local in main, the printed info like this:

(Sel < (WPVar weight)> [ (SExt w64 (Add w32 1 (WPVar w32 (x))))] )
kids[0] = (WPVar weight)
kids[1] = 11
offset = 44
path condition = [
        (Eq 1
     (ReadLSB w32 0 v_9)),
        (Eq 1
     (ReadLSB w32 0 v_1)),
        (Eq 1
     (ReadLSB w32 0 v_2)),
        (Eq 1
     (ReadLSB w32 0 v_6)),
        (Eq 1
     (ReadLSB w32 0 v_7)),
        (Eq 1
     (ReadLSB w32 0 v_5)),
        (Eq 1
     (ReadLSB w32 0 v_4)),
        (Eq 1
     (ReadLSB w32 0 v_3)),
        (Eq false
     (Eq 1
         (ReadLSB w32 0 v_8))),
        (Eq 1
     (ReadLSB w32 0 v))]

[xuanlinhha]

@rasoolmaghareh I think there are something wrong with data of dependency in funtion ref<TxStoreEntry> TxStore::find(ref<TxAllocationContext> alc, ref<Expr> offset) const This is the source code I used to print:

llvm::errs() << "-----111----\n";
    for (LowerStateStore::const_iterator it = array.concreteBegin(),
                                             ie = array.concreteEnd();
             it != ie; ++it) {
          ref<TxStoreEntry> tmp = (*it).second;
          tmp->getIndex()->dump();
          llvm::errs() << "------------\n";
          tmp->getContent()->getExpression()->dump();
          llvm::errs() << "************\n";
        }
    llvm::errs() << "-----222----\n";

And the result I got is like this:

-----111----
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 0
------------
237684487579686500932345921536
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 4
------------
1
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 8
------------
2
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 12
------------
3
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 16
------------
4
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 20
------------
5
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 24
------------
6
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 28
------------
7
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 32
------------
8
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 33
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 34
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 35
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 36
------------
9
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 37
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 38
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 39
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 40
------------
10
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 41
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 42
------------
0
************
function/value: main/  %weight = alloca [11 x i32], align 16
stack: (empty)
offset: 43
------------
0
************
-----222----

Why do we have offset values like 42,43 here, I don't know if this is a bug or it has other usages

[rasoolmaghareh]

@xuanlinhha My understanding is that everything is fine here.

1- Regarding having 9 elements in the dependency the point is that at that point only 9 out of 11 elements in the array are initialized. The null value returned is correct and we should fail subsumption at that point.

2- Regarding Why do we have offset values like 42,43 here the array has 11 elements of 4 bytes. As a result, the offset can range from 0 to 43. Since the first 8 elements are initialized to 4-byte integers it prints them in 4 bytes offsets. The remainder of the array is not initialized and it prints them byte by byte.

I think the main issue over here is why the correct WP formula is not generated when the array is global. Let's focus back on this.

[xuanlinhha]

I uncommented your code and update to like this: if there is no ref<TxAllocationContext> or no ref<TxStoreEntry> when initiating WPVar, I return a null instance of WPVar Is that ok?

[rasoolmaghareh]

yes.

[xuanlinhha]

But how about this:

ref<Expr> TxWeakestPreCondition::getLoadGep(llvm::LoadInst *p) {
  ref<Expr> result;
  // klee_warning("PUSHUP4");
  return result;
}

[xuanlinhha]

And I run with this program: https://github.com/tracer-x/klee/pull/361#issuecomment-630497018 I got this warning also: klee_warning("TxWeakestPreCondition::getLoad: Not implemented yet!");

[rasoolmaghareh]

@xuanlinhha: I have checked the output and the first issue seems to be from the partitioning. Have a look at the stored interpolant:

KLEE: ------------ Subsumption Table Entry ------------
Program point = 37604936
interpolant = (empty)
concretely-addressed store = [
        address:
                function/value: main/  %a = alloca [5 x i32], align 16
                stack: (empty)
                offset: 0
        content:
                function/value: choice/  %1 = load i32* %arrayidx, align 4, !dbg !132
                1
                reason(s) for storage:
                        branch infeasibility [main: Line 10]
]
symbolically-addressed store = []
concretely-addressed historical store = [
        address:
                function/value: choice/  %a.addr = alloca i32*, align 8
                stack:
                          %call = call i32 @choice(i32* %arraydecay), !dbg !135
                offset: 0
        content:
                function/value: i32* %a
                OFFSETS:
                [[base: 8792603361960, size: 20]=={0}]
                reason(s) for storage:
                        branch infeasibility [main: Line 10]
                        pointer use [choice: Line 21]
                        pointer use [choice: Line 23]
                        pointer use [choice: Line 24]
]
symbolically-addressed historical store = []
existentials = []
wp interpolant = [(And (And (Sle (Add w32 (WPVar w32 (sum))
                         N0:(Sel w32 (WPVar w32 (a.addr)) 0))
                9000)
           (Eq 1 (WPVar w32 (count))))
      (Not (Eq 4294967295 N0)))]

Hear a.addr is shared between the WP interpolant formula and the deletion interpolant. This should not happen. Also, if a.addr is in the wp-interpolant, it should change to a at the call point. As a result, here the DELETION part of the interpolant should have been empty.

[xuanlinhha]

In choice function,

define i32 @choice(i32* %a) #0 {
  %1 = alloca i32, align 4
  %2 = alloca i32*, align 8

I think we can link %2 with %a but how we can link with array a in main function? In order to link we need to use the list of actually executed instructions but currently, we only see the CFG. Different paths it may link to different passed parameters, %2 may be linked to another name not a in main

[rasoolmaghareh]

Hi Linh,

If you look at the last instruction before %1 = alloca i32, align 4 in reverseInstructionList, it would be the call instruction to this function. The call instruction would have a sequence of arguments, where those arguments can be matched with %a here.

For example, in this program we have:

%arraydecay = getelementptr inbounds [5 x i32]* %a, i32 0, i32 0, !dbg !135
%call = call i32 @choice(i32* %arraydecay), !dbg !135

Here, %arraydecay can be matched with %a.

[xuanlinhha]

Currently, there are 2 places we get the name of llvm::AllocaInst instruction which is used to store function parameters 1 is when generating WP 1 is in function updateSubsumptionTableEntry Do you think we need to change in both 2 places or just in updateSubsumptionTableEntry?

[rasoolmaghareh]

I am not sure if I understood your question completely. But I think it is needed at least when generating WP.

[xuanlinhha]

When we create WP for alloca with no variable name, we look for the call instruction to match variable but when I see the list of inversedInstructionList in the current node, there is not call instruction but is in the parent node, do you know why? And how do we know the exact list of executed instructions?

TxWeakestPreCondition::getLoad 
NO NAME ---
  %1 = alloca i32, align 4
function name=choice
// current node
  %20 = load i32** %2, align 8, !dbg !138
  %21 = getelementptr inbounds i32* %20, i64 0, !dbg !138
  %22 = load i32* %21, align 4, !dbg !138
  %23 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([11 x i8]* @.str6, i32 0, i32 0), i32 %22), !dbg !138
  %24 = load i32** %2, align 8, !dbg !138
  %25 = getelementptr inbounds i32* %24, i64 0, !dbg !138
  %26 = load i32* %25, align 4, !dbg !138
  store i32 %26, i32* %1, !dbg !138
  br label %27, !dbg !138
  %28 = load i32* %1, !dbg !140
  ret i32 %28, !dbg !140
  store i32 %10, i32* %c, align 4, !dbg !135
  %11 = load i32* %c, align 4, !dbg !137
  %12 = icmp eq i32 %11, -1, !dbg !137
  br i1 %12, label %13, label %14, !dbg !137
  %15 = load i32* %c, align 4, !dbg !139
  %16 = load i32* %sum, align 4, !dbg !139
  %17 = add nsw i32 %16, %15, !dbg !139
  store i32 %17, i32* %sum, align 4, !dbg !139
  %18 = load i32* %c, align 4, !dbg !140
  %19 = load i32* %sum, align 4, !dbg !140
  %20 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([18 x i8]* @.str, i32 0, i32 0), i32 %18, i32 %19), !dbg !140
  br label %4, !dbg !141
  %5 = load i32* %count, align 4, !dbg !134
  %6 = add nsw i32 %5, -1, !dbg !134
  store i32 %6, i32* %count, align 4, !dbg !134
  %7 = icmp ne i32 %5, 0, !dbg !134
  br i1 %7, label %8, label %21, !dbg !134
  %22 = load i32* %sum, align 4, !dbg !142
  %23 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([14 x i8]* @.str1, i32 0, i32 0), i32 %22), !dbg !142
  %24 = load i32* %sum, align 4, !dbg !143
  %25 = icmp sle i32 %24, 9000, !dbg !143
  br i1 %25, label %26, label %27, !dbg !143
  br label %29, !dbg !143
  %30 = load i32* %1, !dbg !144
  ret i32 %30, !dbg !144
===============
// parent node
  %20 = load i32** %2, align 8, !dbg !138
  %21 = getelementptr inbounds i32* %20, i64 0, !dbg !138
  %22 = load i32* %21, align 4, !dbg !138
  %23 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([11 x i8]* @.str6, i32 0, i32 0), i32 %22), !dbg !138
  %24 = load i32** %2, align 8, !dbg !138
  %25 = getelementptr inbounds i32* %24, i64 0, !dbg !138
  %26 = load i32* %25, align 4, !dbg !138
  store i32 %26, i32* %1, !dbg !138
  br label %27, !dbg !138
  %28 = load i32* %1, !dbg !140
  ret i32 %28, !dbg !140
  store i32 %10, i32* %c, align 4, !dbg !135
  %11 = load i32* %c, align 4, !dbg !137
  %12 = icmp eq i32 %11, -1, !dbg !137
  br i1 %12, label %13, label %14, !dbg !137
  %15 = load i32* %c, align 4, !dbg !139
  %16 = load i32* %sum, align 4, !dbg !139
  %17 = add nsw i32 %16, %15, !dbg !139
  store i32 %17, i32* %sum, align 4, !dbg !139
  %18 = load i32* %c, align 4, !dbg !140
  %19 = load i32* %sum, align 4, !dbg !140
  %20 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([18 x i8]* @.str, i32 0, i32 0), i32 %18, i32 %19), !dbg !140
  br label %4, !dbg !141
  %5 = load i32* %count, align 4, !dbg !134
  %6 = add nsw i32 %5, -1, !dbg !134
  store i32 %6, i32* %count, align 4, !dbg !134
  %7 = icmp ne i32 %5, 0, !dbg !134
  br i1 %7, label %8, label %21, !dbg !134
  %9 = getelementptr inbounds [5 x i32]* %a, i32 0, i32 0, !dbg !135
  %10 = call i32 @choice(i32* %9), !dbg !135
  %1 = alloca i32, align 4
  %2 = alloca i32*, align 8
  %c = alloca i32, align 4
  store i32* %a, i32** %2, align 8
  %3 = load i32** %2, align 8, !dbg !132
  %4 = getelementptr inbounds i32* %3, i64 0, !dbg !132
  %5 = load i32* %4, align 4, !dbg !132
  %6 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([21 x i8]* @.str4, i32 0, i32 0), i32 %5), !dbg !132
  %7 = bitcast i32* %c to i8*, !dbg !133
  call void @klee_make_symbolic(i8* %7, i64 4, i8* getelementptr inbounds ([2 x i8]* @.str5, i32 0, i32 0)), !dbg !133
  %8 = load i32** %2, align 8, !dbg !134
  %9 = load i32* %8, align 4, !dbg !134
  %10 = icmp eq i32 %9, -1, !dbg !134
  br i1 %10, label %11, label %12, !dbg !134
  %13 = load i32* %c, align 4, !dbg !136
  %14 = icmp ne i32 %13, 0, !dbg !136
  br i1 %14, label %15, label %19, !dbg !136

[rasoolmaghareh]

@xuanlinhha: I think the easier way is to look at the previous instruction in the reverseInstructionList. If you look at the parent node, the instruction before Alloca is the Call instruction. In case, a function has two or more arguments, we would have a sequence of Alloca instructions and one call instruction before them.

[xuanlinhha]

In the TxWeakestPreCondition::getLoad, I can access the TxTreeNode corresponding to that TxWeakestPreCondition and reverseInstructionList inside that node, but there is no alloca and call instruction. You see I printed here https://github.com/tracer-x/klee/issues/368#issuecomment-631964417 When we generate WP for other cases, we only based on the CGF by recursion, and when reaching to alloca for function parameters, that instruction may not be executed in the current node

[rasoolmaghareh]

I think we might require to look at the parent node while they are in the same function. The reason is that if there are two if-stmt between the current instruction and the top of the function, the alloca would be in the grandparent node.

[xuanlinhha]

@rasoolmaghareh 1 thing I found is that when we see %10 = call i32 @choice(i32* %9), !dbg !135, use the function TxWeakestPreCondition::getCallInst , it finds the return instruction of choice which is %28 = load i32* %1, !dbg !140, then apply TxWeakestPreCondition::getLoad on %1 and because %1 is alloca instruction then the WP is WPVar("%1"), in your format is WPVar("retvalue") This is not correct right? How to deal with this case?

[rasoolmaghareh]

@xuanlinhha I think WPVar("%1") would be good enough. Later on, when there is a store into %1, the wp formula is updated naturally.

[xuanlinhha]

So with the format on your machine, alloca instruction for return value will have name as retvalue and for params will end with .addr If the format is %1, %2, %3 do you know how to differentiate them which is for return which is for params?

[rasoolmaghareh]

I suggest we discuss this more in an online meeting.

[rasoolmaghareh]

@xuanlinhha, with respect to our discussion, there are three things that should be checked:

1- Return instruction 2- Call instruction 3- Bug in the partitioning algorithm

I will first start with the third case. After fixing this we will go to case 2 and case 1.

Consider this program:

#include <klee/klee.h>

int sum = 0;
int a[5] = {1, 10, 100, 1000, -1};

int main() {
    int c;
    c = choice(a);
    if (c == -1) exit(0);
    sum += c;
    klee_assert(sum <= 9000);
}

int choice(int *a) {
    int c;
    klee_make_symbolic(&c, sizeof(unsigned), "c");
    if (*a == -1) return -1;
    if (c) return choice(a + 1); else { return a[0]; }
}

Attached please find the output of my run. out.txt

Here you can see that the partitioning is not working correctly and the same variable appears on the both sides of the Interpolant:

KLEE: ------------ Subsumption Table Entry ------------
Program point = 36330680
interpolant = (empty)
concretely-addressed store = [
        address:
                function/value: @a = global [5 x i32] [i32 1, i32 10, i32 100, i32 1000, i32 -1], align 16
                stack: (empty)
                offset: 0
        content:
                function/value: choice/  %2 = load i32* %1, align 4, !dbg !140
                1
                reason(s) for storage:
                        branch infeasibility [main: Line 10]
]
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
wp interpolant = [(And (Sle (Add w32 (WPVar w32 (sum))
                    N0:(Sel w32 (WPVar w32 (a.addr)) 0))
           9000)
      (Not (Eq 4294967295 N0)))]

Issues: 1- a and a.addr appear in both side of the interpolant. a should have been removed from concretely-addressed store. 2- On your version probably you would see %2 instead of a.addr.

Please fix this issue and we will continue with the other two issues. The ourput interpolant should be like this:

KLEE: ------------ Subsumption Table Entry ------------
Program point = 36330680
interpolant = (empty)
concretely-addressed store = []
symbolically-addressed store = []
concretely-addressed historical store = []
symbolically-addressed historical store = []
existentials = []
wp interpolant = [(And (Sle (Add w32 (WPVar w32 (sum))
                    N0:(Sel w32 (WPVar w32 (a.addr)) 0))
           9000)
      (Not (Eq 4294967295 N0)))]

[xuanlinhha]

@rasoolmaghareh: I think these issues are related each other. If we solve issue 1 and 2, the issue 3 will be solved. The current implementation is that, for alloca instruction without name we get the name %1, %2. Now we will replace with the name of variables in the call instruction in main function, something like a ... If the name is correct, the row of varible a in the concrete-address store will be removed. In order to map, we first map %1, %2 to arguments a of function choice then we map arguments a of choice to varible a in main function. What do you think?

[xuanlinhha]

The problem now is that we don't know how to map %1, %2 to function arguments

[rasoolmaghareh]

Consider this function:

int sum (int a, int b, int c)
{
   ....
}

If you compile this function to LLVM, you will have 4 alloca instructions on the top:

%1 is always the return value. %2 is the first argument (%a) %3 is the first argument (%b) %4 is the first argument (%c)

[xuanlinhha]

But for this function, there is not alloca for return, based on what to know that?

define i32 @choice(i32 %z, i32 %flip) #0 {
  %1 = alloca i32, align 4
  %2 = alloca i32, align 4
  store i32 %z, i32* %1, align 4
  store i32 %flip, i32* %2, align 4
  %3 = load i32* %1, align 4, !dbg !138
  %4 = icmp ne i32 %3, 1, !dbg !138
  br i1 %4, label %5, label %6, !dbg !138

; <label>:5                                       ; preds = %0
  store i32 0, i32* %1, align 4, !dbg !138
  br label %7, !dbg !138

; <label>:6                                       ; preds = %0
  store i32 1, i32* %1, align 4, !dbg !140
  br label %7

; <label>:7                                       ; preds = %6, %5
  %8 = load i32* %1, align 4, !dbg !141
  ret i32 %8, !dbg !141
}

[rasoolmaghareh]

can you post the C function, probably it has no return value (void).

[xuanlinhha]

It has but it returns the param:

int choice(int z, int flip) {
  if (z != 1) z=0; 
  else z = 1;                                                                       
  return z;
}

[rasoolmaghareh]

Ok, I think we can agree that LLVM is not acting consistently in every place. The best way to detect the arguments seems to be the first instructions after the alloca instructions:

store i32 %z, i32* %1, align 4 store i32 %flip, i32* %2, align 4

Here, z is linked to %1 and flip is linked to %2.

[xuanlinhha]

But I found this case in main function:

define i32 @main() #0 {
  %1 = alloca i32, align 4
  %count = alloca i32, align 4
  %sum = alloca i32, align 4
  %a = alloca [5 x i32], align 16
  %c = alloca i32, align 4
  store i32 0, i32* %1
  store i32 2, i32* %count, align 4, !dbg !132
  store i32 0, i32* %sum, align 4, !dbg !132
  %2 = bitcast [5 x i32]* %a to i8*, !dbg !133
  %3 = call i8* @memcpy(i8* %2, i8* bitcast ([5 x i32]* @main.a to i8*), i64 20)
  br label %4, !dbg !134

it stores to %1 which is not an argument, I think in some other functions it would have the same situation

[rasoolmaghareh]

In such a case %1 is the return value. If you compile this on my version %1 is %retval

[xuanlinhha]

so how to differentiate between the return value and parameter? on your version we can use names but on my machine, they have no name.

[rasoolmaghareh]

The algorithm would be like this:

1- %1 is return value if first the function return is not void and there is no store instruction after the alloca instructions on the top of the function which links %1 to any argument.
2- The store instruction on the top helps us to match %1... to the function arguments.

[xuanlinhha]

I updated the code like this: If alloca is for function paramenters then generate WP of passed argument in caller function But this has 2 issues:

%9 = getelementptr inbounds [5 x i32]* %a, i32 0, i32 0, !dbg !135
  %10 = call i32 @choice(i32* %9), !dbg !135

The passed argument is a GE, it will produce a SelectWP but the thing we want is a normal WPVar(a), so what I did is to check if passed argument is a GEP then I just generate WP of the first operand => this need to be discuss again

Another issue is that in the concrete address store we can remove row containing a but cannot remove the rows containing %2

[rasoolmaghareh]

I think we need to remember the information that %2 and %9 are linked and replace %2 with %9 in the wp formula. Then naturally %9 is converted to a

[xuanlinhha]

If we keep WP(%2, the WP formula is like this:

(And (And (Sle (Add w32 (WPVar w32 (sum))
                         N0:(Sel w32 (WPVar w32 (%2)) 0))
                9000)
           (Eq 1 (WPVar w32 (count))))
      (Not (Eq 4294967295 N0)))

And the entry is like this:

concretely-addressed store = [
        address:
                function/value: main/  %count = alloca i32, align 4
                stack: (empty)
                offset: 0
        content:
                function/value: main/  %6 = add nsw i32 %5, -1, !dbg !134
                0
                reason(s) for storage:
                        branch infeasibility [main: Line 6]
        ------------------------------------------
        address:
                function/value: main/  %sum = alloca i32, align 4
                stack: (empty)
                offset: 0
        content:
                function/value: main/  %17 = add nsw i32 %16, %15, !dbg !139
                1
                reason(s) for storage:
                        branch infeasibility [main: Line 14]
        ------------------------------------------
        address:
                function/value: main/  %a = alloca [5 x i32], align 16
                stack: (empty)
                offset: 0
        content:
                function/value: choice/  %5 = load i32* %4, align 4, !dbg !132
                1
                reason(s) for storage:
                        branch infeasibility [main: Line 9]
        ------------------------------------------
        address:
                function/value: choice/  %2 = alloca i32*, align 8
                stack:
                          %10 = call i32 @choice(i32* %9), !dbg !135
                offset: 0
        content:
                function/value: i32* %a
                OFFSETS:
                [[base: 34692704, size: 20]=={0}]
                reason(s) for storage:
                        branch infeasibility [main: Line 9]
                        pointer use [choice: Line 20]
                        pointer use [choice: Line 22]
                        pointer use [choice: Line 28]
]
symbolically-addressed store = []
concretely-addressed historical store = [
        address:
                function/value: choice/  %2 = alloca i32*, align 8
                stack:
                          %10 = call i32 @choice(i32* %9), !dbg !135
                offset: 0
        content:
                function/value: i32* %a
                OFFSETS:
                [[base: 34692704, size: 20]=={0}]
                reason(s) for storage:
                        branch infeasibility [main: Line 9]
                        pointer use [choice: Line 20]
                        pointer use [choice: Line 22]
                        pointer use [choice: Line 28]
]

And the list of instructions in the current node is:

%20 = load i32** %2, align 8, !dbg !142
  %21 = getelementptr inbounds i32* %20, i64 0, !dbg !142
  %22 = load i32* %21, align 4, !dbg !142
  %23 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([11 x i8]* @.str6, i32 0, i32 0), i32 %22), !dbg !142
  %24 = load i32** %2, align 8, !dbg !142
  %25 = getelementptr inbounds i32* %24, i64 0, !dbg !142
  %26 = load i32* %25, align 4, !dbg !142
  store i32 %26, i32* %1, !dbg !142
  br label %27, !dbg !142
  %28 = load i32* %1, !dbg !144
  ret i32 %28, !dbg !144
  store i32 %10, i32* %c, align 4, !dbg !135
  %11 = load i32* %c, align 4, !dbg !137
  %12 = icmp eq i32 %11, -1, !dbg !137
  br i1 %12, label %13, label %14, !dbg !137
  %15 = load i32* %c, align 4, !dbg !139
  %16 = load i32* %sum, align 4, !dbg !139
  %17 = add nsw i32 %16, %15, !dbg !139
  store i32 %17, i32* %sum, align 4, !dbg !139
  %18 = load i32* %c, align 4, !dbg !140
  %19 = load i32* %sum, align 4, !dbg !140
  %20 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([18 x i8]* @.str, i32 0, i32 0), i32 %18, i32 %19), !dbg !140
  br label %4, !dbg !141
  %5 = load i32* %count, align 4, !dbg !134
  %6 = add nsw i32 %5, -1, !dbg !134
  store i32 %6, i32* %count, align 4, !dbg !134
  %7 = icmp ne i32 %5, 0, !dbg !134
  br i1 %7, label %8, label %21, !dbg !134
  %22 = load i32* %sum, align 4, !dbg !142
  %23 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([14 x i8]* @.str1, i32 0, i32 0), i32 %22), !dbg !142
  %24 = load i32* %sum, align 4, !dbg !143
  %25 = icmp sle i32 %24, 9000, !dbg !143
  br i1 %25, label %26, label %27, !dbg !143
  br label %29, !dbg !143
  %30 = load i32* %1, !dbg !144
  ret i32 %30, !dbg !144

I don't know when we replace %2 by %9. From the code, I think %9 is replaced by a when pushing up the call instruction %10 = call i32 @choice(i32* %9), !dbg !135. But that instruction is in the parrent node, I don't know how we can do that in the current node.

[xuanlinhha]

If we just replace %2 in WP by the name of parameters of choice function: define i32 @choice(i32* %a), then how can we delete the row %2 and row %a = alloca [5 x i32], align 16 in the concrete address store, this is global variable a not parameter a of choice function

[rasoolmaghareh]

I see your point, I think we might need to design a new approach for the call instruction. My suggestion is that you continue with the approach which you think is best to implement. Then I will check on a few examples and if there was an issue, we will address it in a special form. It requires a small redesign.

[rasoolmaghareh]

@xuanlinhha and I have fixed this issue halfway, I will close this issue now. I have created 3 new issues for 3 crashes.