extracted/costCheck.ml

   1 open Preamble
   2
   3 open BitVectorTrie
   4
   5 open Graphs
   6
   7 open Order
   8
   9 open Registers
  10
  11 open FrontEndVal
  12
  13 open Hide
  14
  15 open ByteValues
  16
  17 open GenMem
  18
  19 open FrontEndMem
  20
  21 open Division
  22
  23 open Z
  24
  25 open BitVectorZ
  26
  27 open Pointers
  28
  29 open Coqlib
  30
  31 open Values
  32
  33 open FrontEndOps
  34
  35 open CostLabel
  36
  37 open Proper
  38
  39 open PositiveMap
  40
  41 open Deqsets
  42
  43 open ErrorMessages
  44
  45 open PreIdentifiers
  46
  47 open Errors
  48
  49 open Extralib
  50
  51 open Lists
  52
  53 open Positive
  54
  55 open Identifiers
  56
  57 open Exp
  58
  59 open Arithmetic
  60
  61 open Vector
  62
  63 open Div_and_mod
  64
  65 open Util
  66
  67 open FoldStuff
  68
  69 open BitVector
  70
  71 open Jmeq
  72
  73 open Russell
  74
  75 open List
  76
  77 open Setoids
  78
  79 open Monad
  80
  81 open Option
  82
  83 open Extranat
  84
  85 open Bool
  86
  87 open Relations
  88
  89 open Nat
  90
  91 open Integers
  92
  93 open Types
  94
  95 open AST
  96
  97 open Hints_declaration
  98
  99 open Core_notation
 100
 101 open Pts
 102
 103 open Logic
 104
 105 open RTLabs_syntax
 106
 107 open CostSpec
 108
 109 open Extra_bool
 110
 111 open Sets
 112
 113 open Listb
 114
 115 open Listb_extra
 116
 117 open CostMisc
 118
 119 (** val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool **)
 120 let check_well_cost_fn f =
 121   Bool.andb
 122     (Identifiers.idmap_all PreIdentifiers.LabelTag f.RTLabs_syntax.f_graph
 123       (fun l s _ ->
 124       CostSpec.well_cost_labelled_statement f.RTLabs_syntax.f_graph s))
 125     (CostSpec.is_cost_label
 126       (Identifiers.lookup_present PreIdentifiers.LabelTag
 127         f.RTLabs_syntax.f_graph (Types.pi1 f.RTLabs_syntax.f_entry)))
 128
 129 open Deqsets_extra
 130
 131 (** val check_label_bounded :
 132     RTLabs_syntax.statement Graphs.graph -> Graphs.label -> Graphs.label
 133     List.list -> Identifiers.identifier_set -> Nat.nat ->
 134     Identifiers.identifier_set Types.option **)
 135 let rec check_label_bounded g checking checking_tail to_check term_check =
 136   let stop_now = Types.Some to_check in
 137   (match term_check with
 138    | Nat.O -> (fun _ -> assert false (* absurd case *))
 139    | Nat.S term_check' ->
 140      (fun _ ->
 141        let st = Identifiers.lookup_present PreIdentifiers.LabelTag g checking
 142        in
 143        let succs = CostSpec.successors st in
 144        (match succs with
 145         | List.Nil -> (fun _ -> stop_now)
 146         | List.Cons (h, t) ->
 147           (match t with
 148            | List.Nil ->
 149              (fun _ ->
 150                let st' =
 151                  Identifiers.lookup_present PreIdentifiers.LabelTag g h
 152                in
 153                (match CostSpec.is_cost_label st' with
 154                 | Bool.True -> stop_now
 155                 | Bool.False ->
 156                   (match Identifiers.try_remove PreIdentifiers.LabelTag
 157                            to_check h with
 158                    | Types.None ->
 159                      (fun _ ->
 160                        match Bool.orb
 161                                (Deqsets.eqb
 162                                  (Identifiers.deq_identifier
 163                                    PreIdentifiers.LabelTag) (Obj.magic h)
 164                                  (Obj.magic checking))
 165                                (Listb.memb
 166                                  (Identifiers.deq_identifier
 167                                    PreIdentifiers.LabelTag) (Obj.magic h)
 168                                  (Obj.magic checking_tail)) with
 169                        | Bool.True -> Types.None
 170                        | Bool.False -> stop_now)
 171                    | Types.Some to_check' ->
 172                      (fun _ ->
 173                        check_label_bounded g h (List.Cons (checking,
 174                          checking_tail)) to_check'.Types.snd term_check')) __))
 175            | List.Cons (x, x0) -> (fun _ -> stop_now))) __)) __
 176
 177 (** val check_graph_bounded :
 178     RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set ->
 179     Graphs.label -> Nat.nat -> Bool.bool **)
 180 let rec check_graph_bounded g to_check start term_check =
 181   (match term_check with
 182    | Nat.O -> (fun _ -> assert false (* absurd case *))
 183    | Nat.S term_check' ->
 184      (fun _ ->
 185        (match check_label_bounded g start List.Nil to_check
 186                 (Identifiers.id_map_size PreIdentifiers.LabelTag g) with
 187         | Types.None -> (fun _ -> Bool.False)
 188         | Types.Some to_check' ->
 189           (fun _ ->
 190             (match Identifiers.choose PreIdentifiers.LabelTag to_check' with
 191              | Types.None -> (fun _ _ _ -> Bool.True)
 192              | Types.Some l_to_check'' ->
 193                (fun _ _ _ ->
 194                  check_graph_bounded g l_to_check''.Types.snd
 195                    l_to_check''.Types.fst.Types.fst term_check')) __ __ __))
 196          __)) __
 197
 198 (** val check_sound_cost_fn :
 199     RTLabs_syntax.internal_function -> Bool.bool **)
 200 let check_sound_cost_fn fn =
 201   (match Identifiers.try_remove PreIdentifiers.LabelTag
 202            (Identifiers.id_set_of_map PreIdentifiers.LabelTag
 203              fn.RTLabs_syntax.f_graph) (Types.pi1 fn.RTLabs_syntax.f_entry) with
 204    | Types.None -> (fun _ -> assert false (* absurd case *))
 205    | Types.Some to_check ->
 206      (fun _ _ _ ->
 207        check_graph_bounded fn.RTLabs_syntax.f_graph to_check.Types.snd
 208          (Types.pi1 fn.RTLabs_syntax.f_entry)
 209          (Identifiers.id_map_size PreIdentifiers.LabelTag
 210            fn.RTLabs_syntax.f_graph))) __ __ __
 211
 212 (** val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool **)
 213 let check_cost_program p =
 214   Lists.all (fun fn ->
 215     match fn.Types.snd with
 216     | AST.Internal fn0 ->
 217       Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0)
 218     | AST.External x -> Bool.True) p.AST.prog_funct
 219
 220 (** val check_cost_program_prf :
 221     RTLabs_syntax.rTLabs_program -> __ Errors.res **)
 222 let check_cost_program_prf p =
 223   (match check_cost_program p with
 224    | Bool.True -> (fun _ -> Errors.OK __)
 225    | Bool.False ->
 226      (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __
 227