Suspected false positive in saber

[tianxinghe]

I automatically generate some test cases and attempt to use them to test Saber. I suspect I have found a false positive issue. I try to minimize it to still reflect the observed issue and below is the test case.

The free function is called three times: free1: entry - block5 - block4 - block6 free2: entry - block5 - (block4) - block3 - (block7) - block2 - block1 free3: entry - block5 - (block4) - block3 - (block7) - block2 - block So there is no double free in the function. I guess it's possible because the same basic block is entered multiple times, or there is a bug in the code related to bool. I am trying to modify the code, can you help me confirm if it is a bug or if I just make a mistake？

  #include<stdlib.h>
  
  int main(int argc, char ** argv) {
    int a1 = 1;
    unsigned char a2;
    int a3;
    int** a4;
    int a5;
    unsigned char a6;
    
    a3 = 346239900;
    a4 = (int **)malloc(8);
    goto block5;
  
  block:
    free(a4);
    goto exit;
  
  block1:
    free(a4);
    goto exit;
  
  block2:
    a2 = 0 & 1;
    if (a2) {
      goto block;
    } else {
      goto block1;
    }
  
  block3:
    if (a3 < 211626231) {
      goto block7;
    } else {
      goto block2; 
    }
  
  block4:
    a5 = a1;
    if (205254149 == a5) {
      goto block6;
    } else {
      goto block3;
    }
  
  block5:
    a6 = (0 & 1);
    if (a6) {
      goto block3;
    } else {
      goto block4;
    }
  
  block6:
    free(a4);
    goto exit;
    
  block7:
    a3 = 3;
    goto block2;
  
  exit:
    return 0;
  }

[tianxinghe]

Calling the simplify function here does not effectively reduce the size of expr. When there are multiple paths to the same basic block, the size of expr can quickly exceed the 30 limit. for example:

    if (a2) { // c0
      goto block; // s1
    } else {
      goto block1;
    }

constraints for s1: (let ((a!1 (and (or c3 (and (not c3) (not c2))) (not c1))) (a!2 (and (or c3 (and (not c3) (not c2))) c1))) (and (or (and c3 c1) a!1 (and c3 (not c1)) a!2) c0))

c0 = c1 = c2 = c3 = false The result above is (and (or c3 (and (not c3) (not c2)) c0) = false

which are merged from four paths: path1: entry - block5 - block4 - block3 - block7 - block2 - block path2: entry - block5 - block4 - block3 - block2 - block path3: entry - block5 - block3 - block7 - block2 - block path4: entry - block5 - block3 - block2 - block

After checking, the code in the figure believes that the constraint is not unset.

1. the input for check is constraints for s1 . The solver may believes that c0 ,c1, c2, c3 are symbolic values while c0, c1, c2, c3 are all constants.
2. the constraints are too long so that saber thinks the constraints at goto block; and goto block1; are both true. Actually, getVFCond(goto block;) is (and (or c3 (and (not c3) (not c2)) c0) = false, getVFCond(goto block1;) is (and (or c3 (and (not c3) (not c2)) (not c0)) = true

This results in the false positive.

Simplify function fails to simplify the constraints, and it seems that there are some issues with the constant values.

May I ask if it is possible to rewrite the solver? Thank you for taking the trouble to check this issue! @yuleisui

[tianxinghe]

This is the SExpr I have implemented in other projects, which can record path constraints and simplify constraints based on it. I think maybe this would be better.

[yuleisui]

@jumormt I think the issue makes sense. Could you take a look at it?

[jumormt]

Hello @tianxinghe,

Thanks for reporting this, and sorry for the late reply.

Your observation is correct. The false positive is caused by the limitation of the SMT solver. We conservatively evaluate the path constraint as a true value if the z3 expr size exceeds a maximum limit. We do this to sacrifice precision for scalability.

Regarding rewriting the solver, you are welcome to write another solver. However, I don't know whether it is good to replace z3 with your solver. Can you try running Saber on some medium-sized open source to see whether it becomes slower? You can find some bc here.

Best Regards, Xiao

[tianxinghe]

Hello @tianxinghe,

Thanks for reporting this, and sorry for the late reply.

Your observation is correct. The false positive is caused by the limitation of the SMT solver. We conservatively evaluate the path constraint as a true value if the z3 expr size exceeds a maximum limit. We do this to sacrifice precision for scalability.

Regarding rewriting the solver, you are welcome to write another solver. However, I don't know whether it is good to replace z3 with your solver. Can you try running Saber on some medium-sized open source to see whether it becomes slower? You can find some bc here.

Best Regards, Xiao

I plan to make an attempt: record the local constraints and implement the simplify function (to simplify logical operations), which may result in fewer checks using z3. And you seem to have not distinguished between symbolic values and constants？Since c0, c1, c2, c3 is constants (true or false) and the getSolver.check() in the figure should return unsat, but it does not. That‘s why getVFCond(goto block;) and getVFCond(goto block1;) are both true.

(let ((a!1 (and (or c3 (and (not c3) (not c2))) (not c1))) (a!2 (and (or c3 (and (not c3) (not c2))) c1))) (and (or (and c3 c1) a!1 (and c3 (not c1)) a!2) c0)) = (and (or c3 (and (not c3) (not c2)) c0) = false

I will try to do this job in two months and apologize for it!

[tianxinghe]

    #include <stdlib.h>
    
    int main(int argc, char ** argv) {
      int a = 1;
      int b = 2;
      int** a1;
    
      a1 = (int **)malloc(8);
      if (a == b) {
      } else{
        free(a1);
      }
    
      return 0;
    }

When using Saber to check for memory leaks, it is easy to generate false positives. I think it might need to add some information to help Saber do a check. @yuleisui @jumormt

[tianxinghe]

#include <stdlib.h>

int main(int argc, char ** argv) {
  int a = 1;
  int b = 2;
  int** a1;

  a1 = (int **)malloc(8);
  if (a == b) { // c0
  } else{
    free(a1);
  }

  return 0;
}

I may have misunderstood, but what I mean is that saber does not distinguish between symbolic values and constants, so that the solver thinks that the c0 is a variable and the res (Condition::getSolver().check()) of (not c0) is not unsat.

I think this is similar to determining whether a dynamic memory allocation has been freed at each dominance frontier（or on each path), so I think it's better to distinguish between constants and variables? Thank you! @yuleisui @jumormt