Merge pull request #1823 from goblint/bitfield-z-overflow

Fix `IntervalDomain.top_of` `Z.Overflow` for 63-bit bitfields

Author: sim642

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

@@ -11,7 +11,7 @@ struct
 
   let top_of ?bitfield ik =
     match bitfield with
-    | Some b when b <= Ints_t.to_int (range ik |> snd) ->
+    | Some b when b <= Z.numbits (Size.range ik |> snd) ->
       let signed_lower_bound = Ints_t.neg @@ Ints_t.shift_left Ints_t.one (b - 1) in
       let unsigned_upper_bound = Ints_t.sub (Ints_t.shift_left Ints_t.one b) Ints_t.one in
       if GoblintCil.isSigned ik then

src/framework/constraints.ml

@@ -9,6 +9,15 @@ open Goblint_constraint.ConstrSys
 open GobConfig
 
 
+type Goblint_backtrace.mark += TfLocation of location
+
+let () = Goblint_backtrace.register_mark_printer (function
+    | TfLocation loc ->
+      Some ("transfer function at " ^ CilType.Location.show loc)
+    | _ -> None (* for other marks *)
+  )
+
+
 module type Increment =
 sig
   val increment: increment_data option
@@ -343,14 +352,6 @@ struct
       | Skip           -> tf_skip var edge prev_node
     end getl sidel demandl getg sideg d
 
-  type Goblint_backtrace.mark += TfLocation of location
-
-  let () = Goblint_backtrace.register_mark_printer (function
-      | TfLocation loc ->
-        Some ("transfer function at " ^ CilType.Location.show loc)
-      | _ -> None (* for other marks *)
-    )
-
   let tf var getl sidel demandl getg sideg prev_node (_,edge) d (f,t) =
     let old_loc  = !Goblint_tracing.current_loc in
     let old_loc2 = !Goblint_tracing.next_loc in

src/framework/control.ml

@@ -321,7 +321,6 @@ struct
         if M.tracing then M.trace "con" "Initializer %a" CilType.Location.pretty loc;
         (*incr count;
           if (get_bool "dbg.verbose")&& (!count mod 1000 = 0)  then Printf.printf "%d %!" !count;    *)
-        Goblint_tracing.current_loc := loc;
         match edge with
         | MyCFG.Entry func        ->
           if M.tracing then M.trace "global_inits" "Entry %a" d_lval (var func.svar);
@@ -341,11 +340,19 @@ struct
           res'
         | _                       -> failwith "Unsupported global initializer edge"
       in
+      let transfer_func st (loc, edge) =
+        let old_loc = !Goblint_tracing.current_loc in
+        Goblint_tracing.current_loc := loc;
+        (* TODO: next_loc? *)
+        Goblint_backtrace.protect ~mark:(fun () -> Constraints.TfLocation loc) ~finally:(fun () ->
+            Goblint_tracing.current_loc := old_loc;
+          ) (fun () ->
+            transfer_func st (loc, edge)
+          )
+      in
       let with_externs = do_extern_inits man file in
       (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges);    *)
-      let old_loc = !Goblint_tracing.current_loc in
       let result : Spec.D.t = List.fold_left transfer_func with_externs edges in
-      Goblint_tracing.current_loc := old_loc;
       if M.tracing then M.trace "global_inits" "startstate: %a" Spec.D.pretty result;
       result, !funs
     in

tests/regression/98-bitwise-operations/07-bitfield63-interval.c

@@ -0,0 +1,14 @@
+// PARAM: --enable ana.int.interval
+#include <stdint.h>
+
+// NOCRASH: global initializer for 63-bit bitfield used to crash with Z.Overflow in interval domain
+// From: sv-benchmarks/c/intel-tdx-module/tdg_vp_vmcall__requirement__invalid_input_bitmap_havoc_memory.i
+struct
+{
+  uint64_t notify_ept_faults : 1;
+  uint64_t reserved_63_1 : 63;
+} g;
+
+int main() {
+  return 0;
+}