Question about assertion checking?

seahorn / clam

Static Analyzer for LLVM bitcode based on Abstract Interpretation

Apache License 2.0

273 stars 37 forks source link

Question about assertion checking? #52

Closed yiyuaner closed 3 years ago

yiyuaner commented 3 years ago

Hi, I run clam with the following command:

clam test.bc --crab-dom=int --crab-heap-analysis=none --crab-check=assert

I have already instrumented test.bc with some __CRAB_assert checks. When the analysis finishes, clam outputs:

************** ANALYSIS RESULTS ****************
 92   Number of total safe checks
  0    Number of total error checks
128  Number of total warning checks
************** ANALYSIS RESULTS END*************

It seems that there should be 128+92=220 checking statements in test.bc. However, I find out there are more (around 700) inserted __CRAB_assert checks in test.bc. Why is this happening? Does clam skip the verification for some __CRAB_assert statements?

caballa commented 3 years ago

One possible explanation is that the rest of checks are not reachable (i.e., dead code) so that the checker never checks them. But it would be helpful if you can share the bitcode so I can double check.

yiyuaner commented 3 years ago

One possible explanation is that the rest of checks are not reachable (i.e., dead code) so that the checker never checks them. But it would be helpful if you can share the bitcode so I can double check.

Here is the bit code. The analysis takes approximately 3 hours to finish. The command I used is

clam git.pp.bc --crab-dom=int --crab-heap-analysis=none --crab-check=assert

git.pp.zip

yiyuaner commented 3 years ago

One possible explanation is that the rest of checks are not reachable (i.e., dead code) so that the checker never checks them. But it would be helpful if you can share the bitcode so I can double check.

You can use the bc below for a quick verification goaccess_transed.zip

Here is my result:

clam goaccess_transed.bc --crab-dom=int --crab-heap-analysis=none --crab-check=assert
-----------------------------------------------------------------------------------------
************** ANALYSIS RESULTS ****************
7  Number of total safe checks
0  Number of total error checks
9  Number of total warning checks
************** ANALYSIS RESULTS END*************
-----------------------------------------------------------------------------------------
cat goaccess_transed.ll | grep "call void @__CRAB_assert" | wc -l 
33

Thanks a lot.

caballa commented 3 years ago

cat goaccess_transed.ll | grep "call void @__CRAB_assert":

  call void @__CRAB_assert(i32 %0)
  call void @__CRAB_assert(i32 12)
  call void @__CRAB_assert(i32 %4)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 %3)
  call void @__CRAB_assert(i32 %8)
  call void @__CRAB_assert(i32 %4)
  call void @__CRAB_assert(i32 %41)
  call void @__CRAB_assert(i32 %3)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 %21)
  call void @__CRAB_assert(i32 %25)
  call void @__CRAB_assert(i32 %spec.select1101)
  call void @__CRAB_assert(i32 8)
  call void @__CRAB_assert(i32 %align_sz.0.i1084)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 %37)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 2)
  call void @__CRAB_assert(i32 %0)
  call void @__CRAB_assert(i32 %10)
  call void @__CRAB_assert(i32 %11)
  call void @__CRAB_assert(i32 %0)

There are 17 calls to @_CRAB_assert with a constant argument. The translation from LLVM IR to Crab IR ignores those (https://github.com/seahorn/clam/blob/master/lib/Clam/CfgBuilder.cc#L1403) because the constants are all positive numbers so the assertions trivially hold.

yiyuaner commented 3 years ago

Thanks. Closing then.