Merge pull request #27 from ManuelLerchner/fixingBase

Fixing base analysis

src/analyses/base.ml

@@ -624,6 +624,8 @@ struct
 
   let drop_intervalSet = CPA.map (function Int x -> Int (ID.no_intervalSet x) | x -> x )
 
+  let drop_bitfield = CPA.map (function Int x -> Int (ID.no_bitfield x) | x -> x )
+
   let context man (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
@@ -634,6 +636,7 @@ struct
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.int" ~removeAttr:"base.no-int" ~keepAttr:"base.int" fd) drop_ints
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval" ~removeAttr:"base.no-interval" ~keepAttr:"base.interval" fd) drop_interval
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval_set" ~removeAttr:"base.no-interval_set" ~keepAttr:"base.interval_set" fd) drop_intervalSet
+    %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.bitfield" ~removeAttr:"base.no-bitfield" ~keepAttr:"base.bitfield" fd) drop_bitfield
 
 
   let reachable_top_pointers_types man (ps: AD.t) : Queries.TS.t =

src/cdomain/value/cdomains/int/bitfieldDomain.ml

@@ -239,9 +239,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
       else if should_wrap ik then
         (new_bitfield, overflow_info)
       else if should_ignore_overflow ik then 
-        (M.warn ~category:M.Category.Integer.overflow "Bitfield: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Top";
+        (* (M.warn ~category:M.Category.Integer.overflow "Bitfield: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Top"; *)
          (* (bot (), overflow_info)) *)
-         (top_of ik, overflow_info))
+         (top_of ik, overflow_info)
       else 
         (top_of ik, overflow_info)
 
@@ -368,8 +368,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
                                           || BArith.is_invalid a
 
   let is_undefined_shift_operation ik a b =
-    let some_negatives = BArith.min ik b < Z.zero in
-    let b_is_geq_precision = Z.to_int @@ BArith.min ik b >= precision ik in
+    let minVal = BArith.min ik b in 
+    let some_negatives = minVal < Z.zero in
+    let b_is_geq_precision = (if Z.fits_int minVal then Z.to_int @@ minVal >= precision ik else true) in
     (isSigned ik) && (some_negatives || b_is_geq_precision) && not (a = BArith.zero)
 
   let shift_right ik a b = 
@@ -479,7 +480,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     norm ik (!z3, !o3)
 
   let div ?no_ov ik (z1, o1) (z2, o2) =
-    let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = o1 /: o2 in (!:tmp, tmp)) 
+    if o2 = Ints_t.zero then (top_of ik, {underflow=false; overflow=false}) else
+    let res = 
+      if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = o1 /: o2 in (!:tmp, tmp)) 
       else if BArith.is_const (z2, o2) && is_power_of_two o2 then (z1 >>: (Ints_t.to_int o2), o1 >>: (Ints_t.to_int o2))
       else top_of ik in
     norm ik res
@@ -541,10 +544,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     match bf, cong with
     | (z,o), Some (c, m) when m = Ints_t.zero -> norm ik (!: c, c) |> fst
     | (z,o), Some (c, m) when is_power_of_two m && m <> Ints_t.one ->
-      let congruenceMask = !:m in
-      let newz = (!:congruenceMask &: z) |: (congruenceMask &: !:c) in
-      let newo = (!:congruenceMask &: o) |: (congruenceMask &: c) in
-      norm ik (newz, newo) |> fst
+      let congruenceMask = !: (m -: Ints_t.one) in
+      let congZ = congruenceMask |: !:c in 
+      let congO = congruenceMask |: c in 
+      meet ik (congZ, congO) bf
     | _ -> norm ik bf |> fst
 
   let refine_with_interval ik t itv = 

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -31,6 +31,7 @@ module IntDomTupleImpl = struct
   (* The Interval domain can lead to too many contexts for recursive functions (top is [min,max]), but we don't want to drop all ints as with `ana.base.context.int`. TODO better solution? *)
   let no_interval = GobTuple.Tuple6.map2 (const None)
   let no_intervalSet = GobTuple.Tuple6.map5 (const None)
+  let no_bitfield = GobTuple.Tuple6.map6 (const None)
 
   type 'a m = (module SOverflow with type t = 'a)
   type 'a m2 = (module SOverflow with type t = 'a and type int_t = int_t )
@@ -63,7 +64,7 @@ module IntDomTupleImpl = struct
     | Some(_, {underflow; overflow}) -> not (underflow || overflow)
     | _ -> false
 
-  let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf =
+  let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf = 
     let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) || (no_overflow ik bf) in
     if not no_ov && not suppress_ovwarn && ( BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then (
       let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in
@@ -75,7 +76,7 @@ module IntDomTupleImpl = struct
     );
     no_ov
 
-  let create2_ovc ik r x ((p1, p2, p3, p4, p5,p6): int_precision) =
+  let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
     let f b g = if b then Some (g x) else None in
     let map x = Option.map fst x in
     let intv =  f p2 @@ r.fi2_ovc (module I2) in
@@ -286,8 +287,8 @@ module IntDomTupleImpl = struct
      (fun (a, b, c, d, e, f) -> maybe refine_with_congruence ik (a, b, c, d, e, f) d);
      (fun (a, b, c, d, e, f) -> maybe refine_with_bitfield ik (a, b, c, d, e, f) f)]
 
-  let refine ik ((a, b, c, d, e,f) : t ) : t =
-    let dt = ref (a, b, c, d, e,f) in
+  let refine ik ((a, b, c, d, e, f) : t ) : t =
+    let dt = ref (a, b, c, d, e, f) in
     (match get_refinement () with
      | "never" -> ()
      | "once" ->
@@ -559,6 +560,8 @@ struct
   let no_interval (x: I.t) = {x with v = IntDomTupleImpl.no_interval x.v}
 
   let no_intervalSet (x: I.t) = {x with v = IntDomTupleImpl.no_intervalSet x.v}
+
+  let no_bitfield (x: I.t) = {x with v = IntDomTupleImpl.no_bitfield x.v}
 end
 
 let of_const (i, ik, str) = IntDomTuple.of_int ik i

src/cdomain/value/cdomains/intDomain.mli

@@ -361,6 +361,7 @@ module IntDomTuple : sig
   include Z
   val no_interval: t -> t
   val no_intervalSet: t -> t
+  val no_bitfield: t -> t
   val ikind: t -> ikind
 end
 

src/config/options.schema.json

@@ -1714,7 +1714,7 @@
             "type": "array",
             "items": {
               "type": "string",
-              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set","base.interval", "base.interval_set","relation.no-context", "relation.context", "no-widen", "widen"]
+              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen"]
             },
             "default": []
           }