Add some type unrolling

Author: sim642

src/analyses/base.ml

@@ -928,7 +928,7 @@ struct
     (* | Lval (Mem e, ofs) -> get ~man st (eval_lv ~man (Mem e, ofs)) *)
     | (Mem e, ofs) ->
       (*if M.tracing then M.tracel "cast" "Deref: lval: %a" d_plainlval lv;*)
-      let rec contains_vla (t:typ) = match t with (* TODO: unrolltype? *)
+      let rec contains_vla (t:typ) = match Cil.unrollType t with
         | TPtr (t, _) -> contains_vla t
         | TArray(t, None, args) -> true
         | TArray(t, Some exp, args) when isConstant exp -> contains_vla t
@@ -1452,7 +1452,8 @@ struct
         match eval_rv_address ~man man.local e with
         | Address a ->
           let slen = Seq.map String.length (List.to_seq (AD.to_string a)) in
-          let lenOf = function (* TODO: unrolltype? *)
+          let lenOf t =
+            match Cil.unrollType t with
             | TArray (_, l, _) -> (try Some (lenOfArray l) with LenOfArray -> None)
             | _ -> None
           in
@@ -2285,7 +2286,7 @@ struct
         ) a
     | _ -> false
 
-  let get_size_of_ptr_target man ptr =
+  let get_size_of_ptr_target man ptr = (* TODO: deduplicate with memOutOfBounds *)
     let intdom_of_int x =
       ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
     in
@@ -2302,7 +2303,7 @@ struct
         let pts_elems_to_sizes (addr: Queries.AD.elt) =
           begin match addr with
             | Addr (v, _) ->
-              begin match v.vtype with (* TODO: unrolltype? *)
+              begin match Cil.unrollType v.vtype with
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with

src/analyses/memOutOfBounds.ml

@@ -77,7 +77,7 @@ struct
         ) a
     | _ -> false
 
-  let get_size_of_ptr_target man ptr =
+  let get_size_of_ptr_target man ptr = (* TODO: deduplicate with base *)
     if points_to_alloc_only man ptr then
       (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
       man.ask (Queries.BlobSize {exp = ptr; base_address = true})
@@ -92,7 +92,7 @@ struct
                 set_mem_safety_flag InvalidDeref;
                 M.warn "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v
               );
-              begin match v.vtype with (* TODO: unrolltype? *)
+              begin match Cil.unrollType v.vtype with
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with

src/analyses/raceAnalysis.ml

@@ -351,7 +351,8 @@ struct
             | ts ->
               if not (Queries.TS.is_empty ts) then
                 includes_uk := true;
-              let f = function (* TODO: unrolltype? *)
+              let f t =
+                match Cil.unrollType t with
                 | TComp (ci, _) ->
                   add_access_struct (conf - 50) ci
                 | _ -> ()

src/cdomain/value/cdomains/structDomain.ml

@@ -269,15 +269,15 @@ struct
         match rem_fields with
         | [] -> second_choice
         | h::t -> begin
-            match (h.ftype, get_bool "ana.base.structs.key.prefer-ptrs", get_bool "ana.base.structs.key.avoid-ints") with (* TODO: unrolltype? *)
+            match Cil.unrollType h.ftype, get_bool "ana.base.structs.key.prefer-ptrs", get_bool "ana.base.structs.key.avoid-ints" with (* TODO: generalize to TEnum with Cil.isIntegralType? *)
             | (TPtr (_, _), _, _) -> h
             | (TInt (_, _), true, _)
             | (TInt (_, _), _, true) -> first_appropriate_key t second_choice
             | (TInt (_, _), _, _) -> h
             | (_, false, _) -> h
             | (_, _, false) -> first_appropriate_key t second_choice
             | (_, _, _) ->
-              let second = match second_choice.ftype with (* TODO: unrolltype? *)
+              let second = match Cil.unrollType second_choice.ftype with (* TODO: generalize to TEnum with Cil.isIntegralType? *)
                 | TInt (_,_) -> h
                 | _ -> second_choice
               in first_appropriate_key t second

src/cdomain/value/cdomains/valueDomain.ml

@@ -372,7 +372,7 @@ struct
     if is_statically_safe_cast t2 t1 then
       true
     else
-      match t2, t1, v with (* TODO: unrolltype? *)
+      match Cil.unrollType t2, Cil.unrollType t1, v with
       | (TInt (ik2,_) | TEnum ({ekind=ik2; _},_)) , (TInt (ik1,_) | TEnum ({ekind=ik1; _},_)), Int v ->
         let cl, cu = IntDomain.Size.range ik2 in
         let l, u = ID.minimal v, ID.maximal v in

src/framework/constraints.ml

@@ -259,7 +259,7 @@ struct
         Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
     let one_function f =
-      match f.vtype with (* TODO: unrolltype? *)
+      match Cil.unrollType f.vtype with
       | TFun (_, params, var_arg, _)  ->
         let arg_length = List.length args in
         let p_length = Option.map_default List.length 0 params in