Consider IS_ERR in ldv_malloc

Created by: tautschnig

The Linux kernel uses addresses near (unsigned long)-1 to indicate errors. ldv_is_err and IS_ERR catch this, and calls to malloc must not interfere with this.

The changes were done using the following command:

for f in c/ldv-*/*.[ci] c/ldv-*/model/*.[ci]
do
grep -q -w '= IS_ERR' $f || continue
export is_err_type=$(grep -w IS_ERR -m 1 $f | cut -f3 -d" ")
perl -i -e \
  '$s = 0; $e = 0; $p = "";
   while(<>) {
     if(/^long ldv_is_err\(void const \*ptr \) ;\s*$/) {
       $e = 1;
     }
     elsif(/^__inline static (long|bool) IS_ERR\(void( const)? \*ptr \)( ;)?\s*$/) {
       $e = 2;
     }
     elsif(/^static inline long IS_ERR\(const void \*ptr\)\s*$/) {
       $e = 2;
     }
     elsif(/^void \*ldv_(x)?[cmz]alloc\(size_t size \)\s*$/) {
       $p = $_;
       $s = 1;
       next;
     }
     elsif($s == 1) {
       if(/ldv_is_err/ || /IS_ERR/ || /tmp = ldv_calloc/) {
         $p .= $_;
         print $p;
         $p = "";
         $s = 0;
       }
       elsif(/^  return malloc\(size\);$/) {
         if($e == 0) {
           print "__inline static $ENV{is_err_type} IS_ERR(void const *ptr ) ;\n";
           $e = 2;
         }
         print $p;
         $p = "";
         print "  void *p = malloc(size);\n";
         if($e == 1) {
           print "  __VERIFIER_assume(ldv_is_err(p) == 0);\n";
         }
         else {
           print "  __VERIFIER_assume(IS_ERR(p) == 0);\n";
         }
         print "  return p;\n";
         $s = 0;
       }
       elsif(/^    return \(p\);$/) {
         if($e == 0) {
           print "__inline static $ENV{is_err_type} IS_ERR(void const *ptr ) ;\n";
           $e = 2;
         }
         print $p;
         $p = "";
         if($e == 1) {
           print "    __VERIFIER_assume(ldv_is_err(p) == 0);\n";
         }
         else {
           print "    __VERIFIER_assume(IS_ERR(p) == 0);\n";
         }
         print "    return (p);\n";
         $s = 0;
       }
       elsif(/^  return calloc\(1UL, size\);$/) {
         if($e == 0) {
           print "__inline static $ENV{is_err_type} IS_ERR(void const *ptr ) ;\n";
           $e = 2;
         }
         print $p;
         $p = "";
         print "  void *p = calloc(1UL, size);\n";
         if($e == 1) {
           print "  __VERIFIER_assume(ldv_is_err(p) == 0);\n";
         }
         else {
           print "  __VERIFIER_assume(IS_ERR(p) == 0);\n";
         }
         print "  return p;\n";
         $s = 0;
       }
       elsif(/^\}/) {
         print "e=$e\n";
         $p = "";
         $s = 0;
       }
       else {
         $p .= $_;
       }
       next;
     }
     print;
   }' \
  $f
done

This PR includes the commits from #1037, #1038, #1055 and those should thus be merged first. The above comment only is the last commit, which is the only change unique to this PR here.