package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file domain.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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)



(* Reduced product interaction modes. *)
type interaction_modes =
  | Only_Reduce_Absolute_Using_Relative
  | Only_Reduce_Relative_Using_Absolute
  | Complete_Reduced_Product
  | No_Reduced_Product

(* Retrieving the interaction mode from parameters. *)
let get_interaction_mode () =
  match Parameters.Numerors_Mode.get () with
  | "relative" -> Only_Reduce_Relative_Using_Absolute
  | "absolute" -> Only_Reduce_Absolute_Using_Relative
  | "both" -> Complete_Reduced_Product
  | "none" -> No_Reduced_Product
  | _ -> assert false

(* Identity effect with unit context. *)
module Identity = struct
  include Identity
  type context = unit
  let resolve () x = x
end

(* Interval abstraction over rationals. *)
module Abstraction = Field_interval.Make (Rational) (Identity)



(* Numerors model based on rational intervals and without context. *)
module Model = struct

  module Scalar = Rational
  type scalar = Rational.t

  module Context = Unit_context
  module Computation = Identity
  type 'a computation = 'a Computation.t

  module Additive       = Abstraction
  module Multiplicative = Abstraction

  module Exact    = Abstraction
  module Absolute = Abstraction
  module Relative = Abstraction

  type exact    = Abstraction.t
  type absolute = Abstraction.t
  type relative = Abstraction.t

  let name = "Numerors.Value"

  let between lower upper =
    let lower = Abstraction.singleton lower in
    let upper = Abstraction.singleton upper in
    Abstraction.join lower upper

  let new_absolute_elementary_error _ bound =
    let upper = Scalar.abs bound in
    let lower = Scalar.neg upper in
    between lower upper

  let new_relative_elementary_error _ bound =
    let upper = Scalar.abs bound in
    let lower = Scalar.neg upper in
    between lower upper

  let do_reduce_absolute_with_relative () =
    match get_interaction_mode () with
    | Only_Reduce_Absolute_Using_Relative | Complete_Reduced_Product -> true
    | Only_Reduce_Relative_Using_Absolute | No_Reduced_Product -> false

  let do_reduce_relative_with_absolute () =
    match get_interaction_mode () with
    | Only_Reduce_Relative_Using_Absolute | Complete_Reduced_Product -> true
    | Only_Reduce_Absolute_Using_Relative | No_Reduced_Product -> false

  let recompute_absolute ~(exact : exact) ~(relative : relative) =
    Abstraction.(exact * relative)

  let recompute_relative ~(exact : exact) ~(absolute : absolute) =
    Abstraction.(absolute / exact)

  let a_x_plus_b_y_over_x_plus_y ~a ~x ~b ~y =
    let bounds s = let b = Abstraction.bounds s in [ b.lower ; b.upper ] in
    let permutations l r = List.(map (fun l -> map (fun r -> l, r) r) l |> flatten) in
    let compute ((a, x), (b, y)) = Scalar.((a * x + b * y) / (x + y)) in
    let ax_permutations = permutations (bounds a) (bounds x) in
    let by_permutations = permutations (bounds b) (bounds y) in
    let values = List.map compute (permutations ax_permutations by_permutations) in
    let lower = List.fold_left Scalar.min Scalar.pos_inf values in
    let upper = List.fold_left Scalar.max Scalar.neg_inf values in
    between lower upper

end



(* Instantiate the value using the model. *)
module Value = struct
  include Value.Make (Model)
  let contextualize (name, builtin) = (name, builtin ())
  let builtins = List.map contextualize builtins
end



(* Reduced product with Cvalues. *)
module Reduce_Cast (Abstract : Abstractions.S) : Abstractions.S = struct

  include Abstract

  let project_ival cvalue =
    try Cvalue.V.project_ival cvalue
    with Cvalue.V.Not_based_on_null -> Ival.top

  let cast get_cvalue set_numerors context ~src_type ~dst_type value =
    let open Eval.Bottom.Operators in
    let+ result = Val.forward_cast context ~src_type ~dst_type value in
    match src_type, dst_type with
    | Eval_typ.(TSInt _, TSFloat fkind) ->
      let ival = get_cvalue value |> project_ival in
      let lower, upper = Ival.min_and_max ival in
      let to_neg_inf v = Option.value v ~default:Rational.neg_inf in
      let to_pos_inf v = Option.value v ~default:Rational.pos_inf in
      let lower = Option.(map Q.of_bigint lower |> to_neg_inf) in
      let upper = Option.(map Q.of_bigint upper |> to_pos_inf) in
      let numerors = Value.of_scalars fkind lower upper in
      set_numerors numerors result
    | _ -> result

  module Val = struct
    include Val
    let forward_cast =
      match get Main_values.CVal.key, mem Value.key with
      | None, _ | _, false -> forward_cast
      | Some get_cvalue, true -> cast get_cvalue (set Value.key)
  end

end



(* Public description of the Numerors abstract domain. *)
let descr =
  "Infers ranges for the absolute and relative errors \
   in floating-point computations."

(* Registration of the Numerors abstract domain and its reduced product. *)
let registered =
  let name = "numerors" and experimental = true in
  let module Name = (struct let name = name end) in
  let module Domain = Simple_memory.Make_Domain (Name) (Value) in
  Abstractions.Hooks.register (fun (module A) -> (module Reduce_Cast (A))) ;
  Abstractions.Domain.register ~name ~experimental ~descr (module Domain)