package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file overflow_checks.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

module Log = Tracelog.Make(struct let category = "Domains.Overflow_checks" end);;
module In_bits = Units.In_bits
open Operator.Alarm

let increase_size = Codex_config.extend_size_for_additive_operations

module Make
  (Sub : Sig.BASE_WITH_INTEGER) =
struct
  include Sub

  (* TODO: Ideally, we would emit alarms here otherwise some assumptions could go unnoticed. This requires
     that every new pointer is assumed to be in the correct range, which we don't do for now.         *)
  let should_emit_alarm = false
  let emit_unsigned_signed_alarms = false

  module Binary_Forward = struct
    include Sub.Binary_Forward

    (* TODO: Should be provided in the domain signature; assume true
       is a workaround. *)
    let clone dom =
      let dom' = match Sub.assume dom (Sub.Boolean_Forward.true_ dom) with
        | Some x -> x
        | None -> assert false in
      dom'

    (* Evaluate a condition in a copy of dom (to not pollute it with
       new terms), that is removed if the condition is
       valid. Otherwise, calls [emit_alarm] then refine dom assuming
       that the condition is true.

       "valid" means that the condition does not return false if [id_or_not] is id,
       and does not return true if it is Quadrivalent.not. *)
    let check_cond  mkcond emit_alarm dom =
      let dom' = clone dom in
      let cond = mkcond dom' in
      match query_boolean dom' cond with
      | Lattices.Quadrivalent.True -> ()
      | Lattices.Quadrivalent.Bottom ->
        Log.fatal (fun p -> p "Evaluation of an overflow condition returned a bottom. \
This is probably an analyzer error that should not have happened \
(the bottom should have been catched earlier).  Please report.")
      | Lattices.Quadrivalent.(False | Top) ->
        emit_alarm ();
        begin
          match assume dom' cond (* Further refine the error. *) with
          | None -> raise Sig.Bottom
          | Some dom'' -> Sub.Context.assign dom dom''
        end


    (** [check_overflow ~signed ~small_size ~wide_size value]
        Adds assertion ensuring that [value], a binary value of size [~wide_size]
        bits, can correctly fit on [~small_size] bits without over/underflow.
        - If [~signed], this means [-2^{small_size-1} <=s value <=s 2^{small_size-1} - 1]
        - If not [~signed], this means [0 <=u value <=u 2^small_size - 1] *)
    let check_overflow ~signed ~(small_size:In_bits.t) ~wide_size operation value dom =
      let compare = (if signed then bisle else biule) in
      let two_pow_size = Z.shift_left Z.one (if signed then (small_size:>int)-1 else (small_size:>int)) in
      (* Upper bound *)
      let upper_bound = Z.sub two_pow_size Z.one in
      let mkcond dom =
        let upper_bound_val = biconst ~size:wide_size upper_bound dom in
        compare ~size:wide_size dom value upper_bound_val in
      let emit_alarm () =
        if should_emit_alarm then
          let size = small_size in
          let overflow_type = if signed then Signed else Unsigned in
          Emit_alarm.emit_alarm  (Integer_overflow{size;operation;overflow_type})
      in
      check_cond mkcond emit_alarm dom;
      (* lower bound *)
      if signed then
        let lower_bound = Z.neg two_pow_size in
        let mkcond dom =
          let lower_bound_val = biconst ~size:wide_size lower_bound dom in
          compare ~size:wide_size dom lower_bound_val value in
        let emit_alarm () =
          if should_emit_alarm then begin
            let size = small_size in
            let overflow_type = Signed in
            Emit_alarm.emit_alarm (Integer_underflow {size;operation;overflow_type})
          end in
        check_cond mkcond emit_alarm dom

    (** [term_builder ~signed dom ~small_size ~wide_size binop v1 v2 r]
        extends [v1], [v2] from [~small_size] to [~wide_size], computes the
        [binop] on [~wide_size], then assumes there are no overflows. *)
    let term_builder ~signed dom ~small_size ~wide_size binop op v1 v2 =
      let dom = clone dom in
      let extend = if signed then bsext else buext in
      let v1_wide = extend ~size:wide_size ~oldsize:small_size dom v1 in
      let v2_wide = extend ~size:wide_size ~oldsize:small_size dom v2 in
      let res = binop ~size:wide_size dom v1_wide v2_wide in
      check_overflow ~signed ~small_size ~wide_size op res dom

    (** Variant of [term_builder] (with inlined [check_overflow])
        for the [~nusw] case (adding an unsigned (pointer) and a signed [offset])
        result must fit on [unsigned] without overflow or underflow. *)
    let check_nusw orig_dom ~small_size ~wide_size binop operation v1 v2 =
      let dom = clone orig_dom in
      let overflow_type = Operator.Alarm.Unsigned_signed in
      let v1_wide = buext ~size:wide_size ~oldsize:small_size dom v1 in
      let v2_wide = bsext ~size:wide_size ~oldsize:small_size dom v2 in
      let res = binop ~size:wide_size dom v1_wide v2_wide in
      let two_pow_size = Z.shift_left Z.one (small_size:>int) in

      (* Upper bound *)
      let mkcond dom =
        let upper_bound = Z.sub two_pow_size Z.one in
        let upper_bound_val = biconst ~size:wide_size upper_bound dom in
        bisle ~size:wide_size dom res upper_bound_val in
      let emit_alarm() =
        let size = small_size in
        if emit_unsigned_signed_alarms then
          Emit_alarm.emit_alarm (Integer_overflow { overflow_type; size; operation })
      in
      check_cond mkcond emit_alarm dom;

      (* lower bound *)
      let mkcond dom =
        let lower_bound_val = biconst ~size:wide_size Z.zero dom in
        bisle ~size:wide_size dom lower_bound_val res in
      let emit_alarm() =
        let size = small_size in
        if emit_unsigned_signed_alarms then
          Emit_alarm.emit_alarm (Integer_underflow {overflow_type; size; operation });
      in
      check_cond mkcond emit_alarm dom



    (** [binop_with_overflow_guard ~small_size ~wide_size binop_func v1 v2]
        returns [binop_func ~size:small_size v1 v2], but first it ensures that no
        overflow occurs by computing [binop_func ~size:wide_size v1 v2] and checking
        that it fits on [~small_size] bits.

        @param ~small_size should be the size of terms [v1] and [v2]
        @param ~wide_size should be large enough to ensure that
               [binop_func ~size:wide_size v1 v2] does not overflow *)
    let binop_with_overflow_guard ~nsw ~nuw ~nusw dom ~small_size ~wide_size binop op v1 v2 =
      if nsw then term_builder ~signed:true dom ~small_size ~wide_size binop op v1 v2;
      if nuw then term_builder ~signed:false dom ~small_size ~wide_size binop op v1 v2;
      if nusw (* We need size+1 here to be able to sign compare unsigned values *)
      then check_nusw dom ~small_size ~wide_size:(increase_size wide_size) binop op v1 v2;
      binop ~size:small_size dom v1 v2

    let biadd ~size ~flags dom a b =
      let Operator.Flags.Biadd.{nsw;nuw;nusw} = Operator.Flags.Biadd.unpack flags in
      (* if nsw || nuw || nusw then
        Emit_alarm.feedback "OverflowAddition size:%d nsw:%b nuw:%b nusw:%b (%a + %a = %a)"
          size nsw nuw nusw
          Terms.pretty a Terms.pretty b Terms.pretty res; *)
      binop_with_overflow_guard ~nsw ~nuw ~nusw dom
        ~small_size:size ~wide_size:(increase_size size) (* No overflow on n+1 bits *)
        (Binary_Forward.biadd ~flags) Biadd
        a b

    let bisub ~size ~flags dom a b =
      let Operator.Flags.Bisub.{nsw;nuw;nusw} = Operator.Flags.Bisub.unpack flags in
      (* if nsw || nuw || nusw then
        Emit_alarm.feedback "OverflowSubtraction size:%d nsw:%b nuw:%b nusw:%b (%a + %a = %a)"
          size nsw nuw nusw
          Terms.pretty a Terms.pretty b Terms.pretty res; *)
      binop_with_overflow_guard ~nsw ~nuw ~nusw dom
        ~small_size:size ~wide_size:(increase_size size) (* No overflow on n+1 bits *)
        (Binary_Forward.bisub ~flags) Bisub
        a b

    let bimul ~size ~flags dom a b = (* Binary_Forward.bimul ~size ~nsw ~nuw dom a b *)
      let Operator.Flags.Bimul.{nsw;nuw} = Operator.Flags.Bimul.unpack flags in
      binop_with_overflow_guard ~nsw ~nuw ~nusw:false dom
        ~small_size:size ~wide_size:In_bits.(double size) (* No overflow on 2n bits *)
        (Binary_Forward.bimul ~flags) Bimul
        a b

    (* There is only one case whe div overflows: MIN_INT / -1 *)
    let bisdiv ~size dom a b =
      let mkcond dom =
        let minus_one = biconst ~size Z.minus_one dom in
        let div_is_neg_one = beq ~size dom b minus_one in
        let min_int = biconst ~size (Z.neg (Z.shift_left Z.one ((size:>int)-1))) dom in
        let num_is_min_int = beq ~size dom a min_int in
        let cond = Boolean_Forward.(&&) dom div_is_neg_one num_is_min_int in
        Boolean_Forward.not dom cond in
      let emit_alarm () =
        if should_emit_alarm then begin
          let overflow_type = Signed in
          let alarm = Integer_overflow { overflow_type; size; operation = Bisdiv } in
          Emit_alarm.emit_alarm alarm
        end in
      check_cond mkcond emit_alarm dom;
      bisdiv ~size dom a b
    ;;
  end
end