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

let dkey = Wp_parameters.register_category "rte"

module type Option = sig (* hides elements from Parameter_sig.Bool *)
  val get : unit -> bool
  val is_default : unit -> bool
  val name : string
end

type t = {
  name : string ;
  cint : bool ; (* whether the option is impacted by the int arithmetic model *)
  option : (module Option) ;
  status : (module RteGen.Generator.S) ;
}

let configure ~update ~generate kf cint rte =
  let module Option = (val rte.option) in
  let module Generator = (val rte.status) in
  if rte.cint && not @@ Option.get () && generate then
    match cint with
    | Cint.Natural -> (* The option is necessary because of the model *)
      Wp_parameters.warning ~once:true ~current:false
        "-wp-rte and model nat require kernel to warn against %s" rte.name
    | Cint.Machine -> ()
  else
  if not @@ Generator.is_computed kf then
    if Option.get () then begin
      let msg = if generate then "generate" else "missing" in
      Wp_parameters.debug ~dkey "function %a: %s rte for %s"
        Kernel_function.pretty kf msg rte.name ;
      update := true
    end else if not @@ Option.is_default () then begin
      Wp_parameters.warning ~once:true ~current:false
        "-wp-rte can annotate %s because %s is not set"
        rte.name Option.name ;
      (* we want to globally warn on "just-check" mode *)
      update := !update || not generate
    end

module WrapFiniteFloat = struct
  include Kernel.SpecialFloat
  let get () = get () <> "none"
end

let generator =
  [ (* Note: -warn-unaligned-pointer and -rte-pointer-call are not listed here,
       so that we do not warn for missing RTE guards for them. *)
    { name = "memory access" ; cint = false ;
      option = (module RteGen.Options.DoMemAccess) ;
      status = (module RteGen.Generator.Mem_access) } ;
    { name = "division by zero" ; cint = false ;
      option = (module RteGen.Options.DoDivMod) ;
      status = (module RteGen.Generator.Div_mod) } ;
    { name = "signed overflow" ; cint = true ;
      option = (module Kernel.SignedOverflow) ;
      status = (module RteGen.Generator.Signed_overflow) } ;
    { name = "unsigned overflow" ; cint = true ;
      option = (module Kernel.UnsignedOverflow) ;
      status = (module RteGen.Generator.Unsigned_overflow) } ;
    { name = "signed downcast" ; cint = true ;
      option = (module Kernel.SignedDowncast) ;
      status = (module RteGen.Generator.Signed_downcast) } ;
    { name = "unsigned downcast" ; cint = true ;
      option = (module Kernel.UnsignedDowncast) ;
      status = (module RteGen.Generator.Unsigned_downcast) } ;
    { name = "shift" ; cint = true ;
      option = (module RteGen.Options.DoShift) ;
      status = (module RteGen.Generator.Shift) } ;
    { name = "left shift on negative" ; cint = true ;
      option = (module Kernel.LeftShiftNegative) ;
      status = (module RteGen.Generator.Left_shift_negative) } ;
    { name = "right shift on negative" ; cint = false ;
      option = (module Kernel.RightShiftNegative) ;
      status = (module RteGen.Generator.Right_shift_negative) } ;
    { name = "invalid bool value" ; cint = false ;
      option = (module Kernel.InvalidBool) ;
      status = (module RteGen.Generator.Bool_value) } ;
    { name = "pointer downcast" ; cint = false ;
      option = (module Kernel.PointerDowncast) ;
      status = (module RteGen.Generator.Pointer_downcast) } ;
    { name = "invalid pointer" ; cint = false ;
      option = (module Kernel.InvalidPointer) ;
      status = (module RteGen.Generator.Pointer_value) } ;
    { name = "float to int" ; cint = false ;
      option = (module RteGen.Options.DoFloatToInt) ;
      status = (module RteGen.Generator.Float_to_int) } ;
    { name = "special float" ; cint = false ;
      option = (module WrapFiniteFloat) ;
      status = (module RteGen.Generator.Float_to_int) } ;
  ]

(* Initialized is a specific case: it is associated to a set of functions *)

let configure_initialized ~update ~generate kf =
  let module Option = RteGen.Options.DoInitialized in
  (* Note: we do not warn when the function is not mem of the set since there
     are two possibilities for the Option:
     - it is the default: no reason to warn,
     - it is explicitly positioned: we expect that the user correctly set it
  *)
  if Option.mem kf then begin
    let generated = RteGen.Generator.Initialized.is_computed kf in
    if not generated then begin
      let msg = if generate then "generate" else "missing" in
      Wp_parameters.debug ~dkey "function %a: %s rte for initialization"
        Kernel_function.pretty kf msg ;
    end ;
    update := !update || not generated
  end

let print_unsupported ~asked message =
  if asked then
    Wp_parameters.warning ~once:true ~current:false
      "Skipped RTE guards: %s" message

let generate model kf =
  let update = ref false in
  let cint = WpContext.on_context (model,WpContext.Kf kf) Cint.current () in
  List.iter (configure ~update ~generate:true kf cint) generator ;
  configure_initialized ~update ~generate:true kf ;
  if !update then begin
    print_unsupported ~asked:(Kernel.UnalignedPointer.get ())
      "unaligned pointers (\\aligned not supported)" ;
    print_unsupported ~asked:(RteGen.Options.DoPointerCall.get ())
      "invalid function pointer calls (\\valid_function not supported)" ;
    let flags =
      { (RteGen.Flags.default ()) with (* we do not support: *)
        pointer_alignment = false ;    (* - \aligned *)
        pointer_call = false ;         (* - \valid_function *)
      }
    in
    RteGen.Visit.annotate ~flags kf
  end

let generate_all model =
  Wp_parameters.iter_kf (generate model)

let missing_guards model kf =
  let update = ref false in
  let cint = WpContext.on_context (model,WpContext.Kf kf) Cint.current () in
  List.iter (configure ~update ~generate:false kf cint) generator ;
  configure_initialized ~update ~generate:false kf ;
  !update

(* -------------------------------------------------------------------------- *)