Undetected double free

[Henrich Lauko]

In current divine, we are not able to detect possible double free here.

  #include <stdlib.h>
  
  int main() {
      void *x = malloc(0x1000);
      free(x);
      void *y = malloc(0x1000);
      if (x == y)
          free(y);
      free(y);
  }

Is there a way we would be able to do that?

[mornfall]

This is pretty much a use-case for the pointer domain described in the medium-term roadmap, where objid's are symbolic in numeric contexts but explicit in pointer contexts. There would be some fiddling to do with lifetime overlaps, since we may need to maintain a number of constraints on such symbolic object identifiers (namely that they are distinct from each other if the object lifetimes overlap). This may be a little annoying, but i don't imagine it's a showstopper.

[mornfall]

Milestone renamed

[mornfall]

The comparison is now reported as an error by verify, so the program is not accidentally accepted. It's then possible to use refinement & symbolic pointers to deal with the comparison, in which case the double free is detected, as desired.

$ divine refine --output testcase.bc --refinement pointers test.c
compiling test.c
$ divine verify --lamp pointers --symbolic test.bc 
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 20.8333                                                        
state count: 5
mips: 0.33
symbolic: 1

error found: yes
error trace: |
  ASSUME (not (= var_1 #x00000000))
  ASSUME (and (not (= var_1 #x00000000)) (= #xbf959e0700000000 (concat var_1 #x00000000)))
  FAULT: invalid pointer passed to __vm_obj_free
  [0] FATAL: memory error in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/sys/fault.hpp:118
  - symbol: free
    location: /dios/libc/_PDCLIB/glue.c:49
  - symbol: main
    location: test.c:10
  - symbol: __dios_start
    location: /dios/libc/sys/start.cpp:91
a report was written to test.report