/chc-ldv-LIA-NonLin-Arrays

Linux Device Driver verification problems from SV-COMP

These is a set of medium hardness benchmarks generated by SeaHorn from Linux Device Drivers (LDV) examples at SV-COMP19. For the same benchmark different encodings of memory are available:

  • (1) -a.smt2: traditional encoding modeling memory with arrays. Disjoint memory regions are modeled with different array variables.
  • (2) -fm1.smt2: encoding modeling memory with a scalar if possible, otherwise, the same as (1).
  • (3) -fm2-2.smt2: encoding modeling memory that has at most 2 memory cells with scalars (and ite terms), otherwise the same as (2).

The following options were used in seahorn to generate these benchmarks:

To generate bitcode:

sea -O2 --step=large --track=mem --horn-global-constraints=true --horn-stats --enable-nondet-init --strip-extern --externalize-addr-taken-functions --horn-singleton-aliases=true --horn-pdr-contexts=600 --devirt-functions --horn-ignore-calloc=false --enable-indvar --enable-loop-idiom --symbolize-constant-loop-bounds --unfold-loops-for-dsa --simplify-pointer-loops --horn-shadow-mem-optimize=false --horn-iuc=1 --horn-iuc-arith=1 --dsa-stats --dsa=sea-cs -m64

To generate CHCs:

--horn-nondet-undef --keep-shadows=true --sea-dsa-type-aware --sea-dsa=cs -horn-inter-proc -horn-sem-lvl=mem --horn-step=large --horn-global-constraints=true --horn-stats --horn-ignore-calloc=true --horn-ignore-memset=true --horn-shadow-mem-optimize=false --horn-use-mbqi=true --horn-vcgen-use-ite --horn-array-global-constraints --horn-use-write=false --horn-skip-constraints=true --lower-gv-init-struct=false --horn-solver-local-ctx=true --horn-solve=false

Additionally, for encoding (2): --horn-inter-proc-mem-fmaps=true --horn-fmap-max-keys=1 --horn-fmap-max-alias=1

For encoding (3): --horn-inter-proc-mem-fmaps=true --horn-fmap-max-keys=2 --horn-fmap-max-alias=2

The original final name is encoded inside the SMT2 file.

The files are in the Z3 rules-format for CHC and are compressed by gzip.

To run using Z3, use the following command line:

$ zcat data/FILE.smt2.gz | z3 -in OPTIONS

Contributors

Created by Isabel Garcia-Contreras, Arie Gurfinkel, and Jorge A. Navas with the help of SeaHorn and Spacer teams.