Merge branch 'master' into stats_on_texpr

src/analyses/apron/relationAnalysis.apron.ml

@@ -256,8 +256,9 @@ struct
             if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
             if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
             let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
-            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
-            r
+            let r' = assert_type_bounds ask r v in
+            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r';
+            r'
           )
       )
     in

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
+      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
+          let lenOf t =
+            match Cil.unrollType t with
             | TArray (_, l, _) -> (try Some (lenOfArray l) with LenOfArray -> None)
             | _ -> None
           in
@@ -1563,7 +1564,7 @@ struct
               let lval = Addr.Mval.to_cil mval in
               (try `Lifted (Bytes.to_string (Hashtbl.find char_array lval))
                with Not_found -> Queries.Result.top q)
-            | _ -> (* what about ISChar and IUChar? *)
+            | _ -> (* TODO: what about ISChar and IUChar? what about TEnum? *)
               (* ignore @@ printf "Type %a\n" d_plaintype t; *)
               Queries.Result.top q
           end
@@ -2030,10 +2031,8 @@ struct
       match exp with
       | None -> nst
       | Some exp ->
-        let t_override = match Cilfacade.fundec_return_type fundec with
-          | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false
-          | ret -> ret
-        in
+        let t_override = Cilfacade.fundec_return_type fundec in
+        assert (not (Cil.isVoidType t_override)); (* Returning a value from a void function, CIL removes the Return expression for us anyway. *)
         let rv = eval_rv ~man man.local exp in
         let st' = set ~man ~t_override nst (return_var ()) t_override rv in
         match ThreadId.get_current ask with
@@ -2284,7 +2283,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
@@ -2301,7 +2300,7 @@ struct
         let pts_elems_to_sizes (addr: Queries.AD.elt) =
           begin match addr with
             | Addr (v, _) ->
-              begin match v.vtype with
+              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/baseInvariant.ml

@@ -112,14 +112,18 @@ struct
         r
       )
     | Mem (Lval lv), off ->
-      let lvals = eval_lv ~man st (Mem (Lval lv), off) in
-      let res = AD.fold (fun a acc ->
+      (* Underlying lvals (may have offsets themselves), e.g., for struct members NOT including any offset appended to outer Mem *)
+      let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in
+      (* Additional offset of value being refined in Addr Offset type *)
+      let original_offset = convert_offset ~man st off in
+      let res = AD.fold (fun base_a acc ->
           Option.bind acc (fun acc ->
-              match a with
-              | Addr (base, _) as orig ->
-                let (a:VD.t) = Address (AD.singleton (AD.Addr.of_var base)) in
-                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty a;
-                let st = set' lv a st in
+              match base_a with
+              | Addr _ ->
+                let (lval_a:VD.t) = Address (AD.singleton base_a) in
+                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a;
+                let st = set' lv lval_a st in
+                let orig = AD.Addr.add_offset base_a original_offset in
                 let old_val = get ~man st (AD.singleton orig) None in
                 let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *)
                 (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
@@ -237,7 +241,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 (t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
         begin match eval_rv ~man st (Lval x) with
           | Int v ->
             if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
@@ -246,7 +250,7 @@ struct
               `NotUnderstood
           | _ -> `NotUnderstood
         end
-      | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) ->
+      | BinOp(op, rval, CastE (ti, Lval x), typ) when Cil.isIntegralType ti ->
         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). *)
@@ -611,8 +615,8 @@ struct
       else
         match exp, c_typed with
         | UnOp (LNot, e, _), Int c ->
-          (match Cilfacade.typeOf e with
-           | TInt  _ | TPtr _ ->
+          (match Cil.unrollType (Cilfacade.typeOf e) with
+           | TInt  _ | TEnum _ | TPtr _ ->
              let ikind = Cilfacade.get_ikind_exp e in
              let c' =
                match ID.to_bool (unop_ID LNot c) with

src/analyses/extractPthread.ml

@@ -359,7 +359,7 @@ end
 module Variable = struct
   type t = varinfo
 
-  let is_integral v = match v.vtype with TInt _ -> true | _ -> false
+  let is_integral v = isIntegralType v.vtype
 
   let is_global v = v.vglob
 

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
+              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/mutexAnalysis.ml

@@ -337,11 +337,7 @@ struct
             | ts when Queries.TS.is_top ts ->
               ()
             | ts ->
-              let f = function
-                | TComp (_, _) -> true
-                | _ -> false
-              in
-              if Queries.TS.exists f ts then
+              if Queries.TS.exists Cilfacade.isStructOrUnionType ts then
                 old_access None
           end;
           on_ad ad

src/analyses/raceAnalysis.ml

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

src/analyses/tutorials/constants.ml

@@ -18,13 +18,8 @@ struct
   (* No contexts *)
   include Analyses.IdentityUnitContextsSpec
 
-  let is_integer_var (v: varinfo) =
-    match v.vtype with
-      | TInt _ -> true
-      | _ -> false
-
   let get_local = function
-    | Var v, NoOffset when is_integer_var v && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
+    | Var v, NoOffset when isIntegralType v.vtype && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
     | _, _ -> None
 
   (** Evaluates expressions *)

src/autoTune.ml

@@ -311,6 +311,7 @@ class addTypeAttributeVisitor = object
 
   (*Set arrays with important types for thread analysis to unroll*)
   method! vtype typ =
+    (* TODO: reuse predicates in Access module (also handles TNamed correctly) *)
     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
@@ -375,7 +376,7 @@ class octagonVariableVisitor(varMap, globals) = object
 
   method! vexpr = function
     (*an expression of type +/- a +/- b where a,b are either variables or constants*)
-    | BinOp (op, e1,e2, (TInt _)) when isComparison op -> (
+    | BinOp (op, e1,e2, _) when isComparison op -> (
         List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e1);
         List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e2);
         DoChildren

src/autoTune0.ml

@@ -91,6 +91,11 @@ let collectFactors visitAction visitedObject =
   ignore (visitAction visitor visitedObject);
   factors
 
-let is_large_array = function
-  | TArray (_,Some (Const (CInt (i,_,_))),_) -> i > Z.of_int @@ 10 * get_int "ana.base.arrays.unrolling-factor"
+let is_large_array t =
+  match Cil.unrollType t with
+  | TArray (_, e, _) ->
+    begin match Cil.lenOfArray e with (* TODO: Cil.lenOfArray but with Z.t? *)
+      | i -> i > 10 * get_int "ana.base.arrays.unrolling-factor"
+      | exception Cil.LenOfArray -> false
+    end
   | _ -> false