Add TODOs about unrollType (issue #1600)

src/analyses/base.ml

@@ -925,7 +925,7 @@ struct
     (* | Lval (Mem e, ofs) -> get ~ctx st (eval_lv ~ctx (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
+      let rec contains_vla (t:typ) = match t with (* TODO: unrolltype? *)
         | TPtr (t, _) -> contains_vla t
         | TArray(t, None, args) -> true
         | TArray(t, Some exp, args) when isConstant exp -> contains_vla t
@@ -1417,7 +1417,7 @@ struct
         match eval_rv_address ~ctx ctx.local e with
         | Address a ->
           let slen = Seq.map String.length (List.to_seq (AD.to_string a)) in
-          let lenOf = function
+          let lenOf = function (* TODO: unrolltype? *)
             | TArray (_, l, _) -> (try Some (lenOfArray l) with LenOfArray -> None)
             | _ -> None
           in
@@ -1995,7 +1995,7 @@ struct
       match exp with
       | None -> nst
       | Some exp ->
-        let t_override = match Cilfacade.fundec_return_type fundec with
+        let t_override = match Cilfacade.fundec_return_type fundec with (* TODO: unrolltype? *)
           | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false
           | ret -> ret
         in
@@ -2267,7 +2267,7 @@ struct
         let pts_elems_to_sizes (addr: Queries.AD.elt) =
           begin match addr with
             | Addr (v, _) ->
-              begin match v.vtype with
+              begin match v.vtype with (* TODO: unrolltype? *)
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match ctx.ask (Queries.EvalLength ptr) with

src/analyses/baseInvariant.ml

@@ -207,7 +207,7 @@ struct
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
       | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
-      | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) ->
+      | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) -> (* TODO: unrolltype? *)
         begin match eval_rv ~ctx st (Lval x) with
           | Int v ->
             if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
@@ -216,7 +216,7 @@ struct
               `NotUnderstood
           | _ -> `NotUnderstood
         end
-      | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) ->
+      | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) -> (* TODO: unrolltype? *)
         derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv
       | BinOp(op, (Const _ | AddrOf _), rval, typ) ->
         (* This is last such that we never reach here with rval being Lval (it is swapped around). *)
@@ -562,7 +562,7 @@ struct
       else
         match exp, c_typed with
         | UnOp (LNot, e, _), Int c ->
-          (match Cilfacade.typeOf e with
+          (match Cilfacade.typeOf e with (* TODO: unrolltype? *)
            | TInt  _ | TPtr _ ->
              let ikind = Cilfacade.get_ikind_exp e in
              let c' =
@@ -777,7 +777,7 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE ((TFloat (_, _)), e), Float c ->
+        | CastE ((TFloat (_, _)), e), Float c -> (* TODO: unrolltype? *)
           (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
            | TFloat (FLongDouble as fk, _), FFloat
            | TFloat (FDouble as fk, _), FFloat
@@ -786,7 +786,7 @@ struct
            | TFloat (FDouble as fk, _), FDouble
            | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
            | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
-        | CastE ((TInt (ik, _)) as t, e), Int c
+        | CastE ((TInt (ik, _)) as t, e), Int c (* TODO: unrolltype? *)
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
           (match eval e st with
            | Int i ->

src/analyses/memOutOfBounds.ml

@@ -93,7 +93,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
+              begin match v.vtype with (* TODO: unrolltype? *)
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match ctx.ask (Queries.EvalLength ptr) with
@@ -127,7 +127,7 @@ struct
          `Top)
 
   let get_ptr_deref_type ptr_typ =
-    match ptr_typ with
+    match ptr_typ with (* TODO: unrolltype? *)
     | TPtr (t, _) -> Some t
     | _ -> None
 

src/analyses/mutexAnalysis.ml

@@ -332,7 +332,7 @@ struct
             | ts when Queries.TS.is_top ts ->
               ()
             | ts ->
-              let f = function
+              let f = function (* TODO: unrolltype? *)
                 | TComp (_, _) -> true
                 | _ -> false
               in

src/analyses/raceAnalysis.ml

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

src/autoTune.ml

@@ -278,7 +278,7 @@ class addTypeAttributeVisitor = object
     let is_important_type (t: typ): bool = match t with
       | TNamed (info, attr) -> List.mem info.tname ["pthread_mutex_t"; "spinlock_t"; "pthread_t"]
       | TInt (IInt, attr) -> hasAttribute "mutex" attr
-      | _ -> false
+      | _ -> false (* TODO: unrolltype? *)
     in
     if is_important_type typ && not @@ hasAttribute "goblint_array_domain" (typeAttrs typ) then
       ChangeTo (typeAddAttributes [Attr ("goblint_array_domain", [AStr "unroll"])] typ)

src/autoTune0.ml

@@ -91,6 +91,6 @@ let collectFactors visitAction visitedObject =
   ignore (visitAction visitor visitedObject);
   factors
 
-let is_large_array = function
+let is_large_array = function (* TODO: unrolltype? *)
   | TArray (_,Some (Const (CInt (i,_,_))),_) -> i > Z.of_int @@ 10 * get_int "ana.base.arrays.unrolling-factor"
   | _ -> false

src/cdomain/value/cdomains/intDomain.ml

@@ -2906,7 +2906,7 @@ struct
         let (min_ikorg, max_ikorg) = range ikorg in
         ikorg = t || (max_t >=: max_ikorg && min_t <=: min_ikorg)
       in
-      match torg with
+      match torg with (* TODO: unrolltype? *)
       | Some (Cil.TInt (ikorg, _)) when p ikorg ->
         if M.tracing then M.trace "cong-cast" "some case";
         x

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
+            match (h.ftype, get_bool "ana.base.structs.key.prefer-ptrs", get_bool "ana.base.structs.key.avoid-ints") with (* TODO: unrolltype? *)
             | (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
+              let second = match second_choice.ftype with (* TODO: unrolltype? *)
                 | TInt (_,_) -> h
                 | _ -> second_choice
               in first_appropriate_key t second
@@ -503,8 +503,8 @@ struct
   let chosen_domain () = get_string "ana.base.structs.domain"
 
   let pick_combined setting (comp: compinfo) =
-    let all_bool () = List.for_all (fun f -> match f.ftype with TInt(IBool, _) -> true | _ -> false) comp.cfields in
-    let has_ptr () = List.exists (fun f -> match f.ftype with TPtr(_, _) -> true | _ -> false) comp.cfields in
+    let all_bool () = List.for_all (fun f -> match f.ftype with TInt(IBool, _) -> true | _ -> false) comp.cfields in (* TODO: unrolltype? *)
+    let has_ptr () = List.exists (fun f -> match f.ftype with TPtr(_, _) -> true | _ -> false) comp.cfields in (* TODO: unrolltype? *)
     match setting with
     | "combined-sk" -> if has_ptr () then "keyed" else "simple"
     | "combined-all" ->

src/cdomain/value/cdomains/valueDomain.ml

@@ -349,7 +349,7 @@ struct
    ************************************************************)
 
   (* is a cast t1 to t2 invertible, i.e., content-preserving in general? *)
-  let is_statically_safe_cast t2 t1 = match t2, t1 with
+  let is_statically_safe_cast t2 t1 = match t2, t1 with (* TODO: unrolltype? *)
     (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType
       | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*)
     | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true
@@ -372,7 +372,7 @@ struct
     if is_statically_safe_cast t2 t1 then
       true
     else
-      match t2, t1, v with
+      match t2, t1, v with (* TODO: unrolltype? *)
       | (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
@@ -392,7 +392,7 @@ struct
     | a, b -> a = b
 
   let cast_addr t a =
-    let rec stripVarLenArr = function
+    let rec stripVarLenArr = function (* TODO: unrolltype? *)
       | TPtr(t, args) -> TPtr(stripVarLenArr t, args)
       | TArray(t, None, args) -> TArray(stripVarLenArr t, None, args)
       | TArray(t, Some exp, args) when isConstant exp -> TArray(stripVarLenArr t, Some exp, args)
@@ -418,7 +418,7 @@ struct
       | _ -> (* cast to smaller/inner type *)
         if M.tracing then M.tracel "casta" "cast to smaller size";
         if d = Some true then err "Ptr-cast to type of incompatible size!" else
-          begin match ta, t with
+          begin match ta, t with (* TODO: unrolltype? *)
             (* struct to its first field *)
             | TComp ({cfields = fi::_; _}, _), _ ->
               if M.tracing then M.tracel "casta" "cast struct to its first field";
@@ -432,7 +432,7 @@ struct
             | _ -> err @@ Format.sprintf "Cast to neither array index nor struct field. is_zero_offset: %b" (Addr.Offs.cmp_zero_offset o = `MustZero)
           end
     in
-    let one_addr = let open Addr in function
+    let one_addr = let open Addr in function (* TODO: unrolltype? *)
         (* only allow conversion of float pointers if source and target type are the same *)
         | Addr ({ vtype = TFloat(fkind, _); _}, _) as x when (match t with TFloat (fkind', _) when fkind = fkind' -> true | _ -> false) -> x
         (* do not allow conversion from/to float pointers*)
@@ -508,7 +508,7 @@ struct
               | Int x when ID.to_int x = Some Z.zero -> AD.null_ptr
               | Int x -> AD.top_ptr
               (* we ignore casts to void*! TODO report UB! *)
-              | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x)
+              | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x) (* TODO: unrolltype? *)
               (*| Address x -> x*)
               | _ -> log_top __POS__; AD.top_ptr
             )
@@ -925,7 +925,7 @@ struct
           | `Field (fld, offs) -> begin
               match x with
               | Union (`Lifted l_fld, value) ->
-                (match value, fld.ftype with
+                (match value, fld.ftype with (* TODO: unrolltype? *)
                  (* only return an actual value if we have a type and return actually the exact same type *)
                  | Float f_value, TFloat(fkind, _) when FD.get_fkind f_value = fkind -> Float f_value
                  | Float _, t -> top_value t
@@ -1091,7 +1091,7 @@ struct
                       | `NoOffset -> top (), offs
                       | `Index (idx, _) when Cil.isArrayType fld.ftype ->
                         begin
-                          match fld.ftype with
+                          match fld.ftype with (* TODO: unrolltype? *)
                           | TArray(_, l, _) ->
                             let len = try Cil.lenOfArray l
                               with Cil.LenOfArray -> 42 (* will not happen, VLA not allowed in union and struct *) in
@@ -1114,15 +1114,15 @@ struct
                 let l', o' = shift_one_over l o in
                 match x with
                 | Array x' ->
-                  let t = (match t with
+                  let t = (match t with (* TODO: unrolltype? *)
                       | TArray(t1 ,_,_) -> t1
                       | _ -> t) in (* This is necessary because t is not a TArray in case of calloc *)
                   let e = determine_offset ask l o exp (Some v) in
                   let new_value_at_index = do_update_offset ask (CArrays.get ask x' (e,idx)) offs value exp l' o' v t in
                   let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
                   Array new_array_value
                 | Bot ->
-                  let t,len = (match t with
+                  let t,len = (match t with (* TODO: unrolltype? *)
                       | TArray(t1 ,len,_) -> t1, len
                       | _ -> t, None) in (* This is necessary because t is not a TArray in case of calloc *)
                   let x' = CArrays.bot () in
@@ -1185,7 +1185,7 @@ struct
   (* Won't compile without the final :t annotation *)
   let rec update_array_lengths (eval_exp: exp -> t) (v:t) (typ:Cil.typ):t =
     match v, typ with
-    | Array(n), TArray(ti, e, _) ->
+    | Array(n), TArray(ti, e, _) -> (* TODO: unrolltype? *)
       begin
         let update_fun x = update_array_lengths eval_exp x ti in
         let n' = CArrays.map (update_fun) n in

src/cdomain/value/domains/invariantCil.ml

@@ -87,7 +87,7 @@ let exp_contains_tmp e =
 class exp_contains_anon_type_visitor = object
   inherit nopCilVisitor
   method! vtype (t: typ) =
-    match t with
+    match t with (* TODO: unrolltype? *)
     | TComp ({cname; _}, _) when String.starts_with ~prefix:"__anon" cname ->
       raise Stdlib.Exit
     | _ ->

src/cdomain/value/util/wideningThresholds.ml

@@ -11,7 +11,7 @@ let addThreshold t_ref z = t_ref := Thresholds.add z !t_ref
 class extractThresholdsFromConditionsVisitor(upper_thresholds,lower_thresholds, octagon_thresholds) = object
   inherit nopCilVisitor
 
-  method! vexpr = function
+  method! vexpr = function (* TODO: unrolltype? *)
     (* Comparisons of type: 10 <= expr, expr >= 10, expr < 10, 10 > expr *)
     | BinOp (Le, (Const (CInt(i,_,_))), _, (TInt _))
     | BinOp (Ge, _, (Const (CInt(i,_,_))), (TInt _))

src/cdomains/apron/sharedFunctions.apron.ml

@@ -165,7 +165,7 @@ struct
               | BinOp (Mod, e1, e2, _) -> bop_near Mod e1 e2
               | BinOp (Div, e1, e2, _) ->
                 Binop (Div, texpr1 e1, texpr1 e2, Int, Zero)
-              | CastE (TInt (t_ik, _) as t, e) ->
+              | CastE (TInt (t_ik, _) as t, e) -> (* TODO: unrolltype? *)
                 begin match  IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t with (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
                   | exception Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)
                   | true -> texpr1 e

src/common/framework/cfgTools.ml

@@ -701,7 +701,7 @@ let getGlobalInits (file: file) : edges  =
       else if not (Hashtbl.mem inits (assign (any_index lval))) then
         Hashtbl.add inits (assign (any_index lval)) ()
     | CompoundInit (typ, lst) ->
-      let ntyp = match typ, lst with
+      let ntyp = match typ, lst with (* TODO: unrolltype? *)
         | TArray(t, None, attr), [] -> TArray(t, Some zero, attr) (* set initializer type to t[0] for flexible array members of structs that are intialized with {} *)
         | _, _ -> typ
       in

src/common/util/cilfacade.ml

@@ -32,7 +32,7 @@ let isFloatType t =
   | TFloat _ -> true
   | _ -> false
 
-let rec isVLAType t =
+let rec isVLAType t = (* TODO: use in base? *)
   match Cil.unrollType t with
   | TArray (et, len, _) ->
     let variable_len = GobOption.exists (Fun.negate Cil.isConstant) len in
@@ -565,7 +565,7 @@ let countLoc fn =
 
 
 let fundec_return_type f =
-  match f.svar.vtype with
+  match f.svar.vtype with (* TODO: unrolltype? *)
   | TFun (return_type, _, _, _) -> return_type
   | _ -> failwith "fundec_return_type: not TFun"
 

src/domains/access.ml

@@ -256,7 +256,7 @@ let get_type fb e =
   (* printf "e = %a\n" d_plainexp e; *)
   let r = get_type fb e in
   (* printf "result = %a\n" d_acct r; *)
-  match r with
+  match r with (* TODO: unrolltype? *)
   | `Type (TPtr (t,a)) -> `Type t (* Why this special case? Almost always taken if not `Struct. *)
   | x -> x (* Mostly for `Struct, but also rare cases with non-pointer `Type. Should they happen at all? *)
 
@@ -309,7 +309,7 @@ let add ~side ~side_empty e voffs =
     | None -> (* unknown variable *)
       if M.tracing then M.traceli "access" "add type %a" CilType.Exp.pretty e;
       let ty = get_val_type e in (* extract old acc_typ from expression *)
-      let (t, o) = match ty with (* convert acc_typ to type-based Memo (components) *)
+      let (t, o) = match ty with (* convert acc_typ to type-based Memo (components) *) (* TODO: unrolltype? *)
         | `Struct (c, o) -> (TComp (c, []), o)
         | `Type t -> (t, `NoOffset)
       in

src/framework/constraints.ml

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

src/util/loopUnrolling.ml

@@ -260,7 +260,7 @@ let findLoopVarAndGoal loopStatement func (op, exp1, exp2) =
     end;
   | _ -> None
 
-let getLoopVar loopStatement func = function
+let getLoopVar loopStatement func = function (* TODO: unrolltype? *)
   | BinOp (op, exp1, exp2, TInt _) when isCompare op -> findLoopVarAndGoal loopStatement func (op, exp1, exp2)
   | _ -> None