extracted/linearise.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 (** val graph_to_lin_statement :
 122     Joint.uns_params -> AST.ident List.list -> 'a1 Identifiers.identifier_map
 123     -> Joint.joint_statement -> Joint.joint_statement **)
 124 let graph_to_lin_statement p globals visited = function
 125 | Joint.Sequential (c, nxt) ->
 126   (match c with
 127    | Joint.COST_LABEL x -> Joint.Sequential (c, (Obj.magic Types.It))
 128    | Joint.CALL (x, x0, x1) -> Joint.Sequential (c, (Obj.magic Types.It))
 129    | Joint.COND (a, ltrue) ->
 130      (match Identifiers.member PreIdentifiers.LabelTag visited
 131               (Obj.magic nxt) with
 132       | Bool.True -> Joint.FCOND (a, ltrue, (Obj.magic nxt))
 133       | Bool.False -> Joint.Sequential (c, (Obj.magic Types.It)))
 134    | Joint.Step_seq x -> Joint.Sequential (c, (Obj.magic Types.It)))
 135 | Joint.Final c -> Joint.Final c
 136 | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
 137
 138 (** val chop :
 139     ('a1 -> Bool.bool) -> 'a1 List.list -> ('a1, 'a1 List.list) Types.prod
 140     Types.option **)
 141 let rec chop test = function
 142 | List.Nil -> Types.None
 143 | List.Cons (x, l') ->
 144   (match test x with
 145    | Bool.True -> chop test l'
 146    | Bool.False ->
 147      Obj.magic
 148        (Monad.m_return0 (Monad.max_def Option.option) { Types.fst = x;
 149          Types.snd = l' }))
 150
 151 type graph_visit_ret_type =
 152   ((Nat.nat Identifiers.identifier_map, Identifiers.identifier_set)
 153   Types.prod, __) Types.prod Types.sig0
 154
 155 (** val graph_visit :
 156     Joint.uns_params -> AST.ident List.list -> __ ->
 157     Identifiers.identifier_set -> Nat.nat Identifiers.identifier_map -> __ ->
 158     Graphs.label List.list -> Nat.nat -> Nat.nat -> Graphs.label ->
 159     graph_visit_ret_type **)
 160 let rec graph_visit p globals g required visited generated visiting gen_length n entry =
 161   (match chop (fun x -> Identifiers.member PreIdentifiers.LabelTag visited x)
 162            visiting with
 163    | Types.None ->
 164      (fun _ -> { Types.fst = { Types.fst = visited; Types.snd = required };
 165        Types.snd = generated })
 166    | Types.Some pr ->
 167      (fun _ ->
 168        let vis_hd = pr.Types.fst in
 169        let vis_tl = pr.Types.snd in
 170        (match n with
 171         | Nat.O -> (fun _ -> assert false (* absurd case *))
 172         | Nat.S n' ->
 173           (fun _ ->
 174             let visited' =
 175               Identifiers.add PreIdentifiers.LabelTag visited vis_hd
 176                 gen_length
 177             in
 178             let statement =
 179               Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g)
 180                 vis_hd
 181             in
 182             let translated_statement =
 183               graph_to_lin_statement p globals visited' statement
 184             in
 185             let generated' = List.Cons ({ Types.fst = (Types.Some vis_hd);
 186               Types.snd = translated_statement }, (Obj.magic generated))
 187             in
 188             let required' =
 189               Identifiers.union_set PreIdentifiers.LabelTag
 190                 (Identifiers.set_from_list PreIdentifiers.LabelTag
 191                   (Joint.stmt_explicit_labels (Joint.lp_to_p__o__stmt_pars p)
 192                     globals translated_statement)) required
 193             in
 194             let visiting' =
 195               List.append
 196                 (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars p);
 197                   Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
 198                   Joint.has_fcond = Bool.False } globals statement) vis_tl
 199             in
 200             let add_req_gen =
 201               match statement with
 202               | Joint.Sequential (s, nxt) ->
 203                 (match s with
 204                  | Joint.COST_LABEL x ->
 205                    (match Identifiers.member PreIdentifiers.LabelTag visited'
 206                             (Obj.magic nxt) with
 207                     | Bool.True ->
 208                       { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
 209                         (Identifiers.add_set PreIdentifiers.LabelTag
 210                           (Identifiers.empty_set PreIdentifiers.LabelTag)
 211                           (Obj.magic nxt)) }; Types.snd = (List.Cons
 212                         ({ Types.fst = Types.None; Types.snd =
 213                         (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
 214                         x0) }, List.Nil)) }
 215                     | Bool.False ->
 216                       { Types.fst = { Types.fst = Nat.O; Types.snd =
 217                         (Identifiers.empty_set PreIdentifiers.LabelTag) };
 218                         Types.snd = List.Nil })
 219                  | Joint.CALL (x, x0, x1) ->
 220                    (match Identifiers.member PreIdentifiers.LabelTag visited'
 221                             (Obj.magic nxt) with
 222                     | Bool.True ->
 223                       { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
 224                         (Identifiers.add_set PreIdentifiers.LabelTag
 225                           (Identifiers.empty_set PreIdentifiers.LabelTag)
 226                           (Obj.magic nxt)) }; Types.snd = (List.Cons
 227                         ({ Types.fst = Types.None; Types.snd =
 228                         (let x2 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
 229                         x2) }, List.Nil)) }
 230                     | Bool.False ->
 231                       { Types.fst = { Types.fst = Nat.O; Types.snd =
 232                         (Identifiers.empty_set PreIdentifiers.LabelTag) };
 233                         Types.snd = List.Nil })
 234                  | Joint.COND (x, x0) ->
 235                    { Types.fst = { Types.fst = Nat.O; Types.snd =
 236                      (Identifiers.empty_set PreIdentifiers.LabelTag) };
 237                      Types.snd = List.Nil }
 238                  | Joint.Step_seq x ->
 239                    (match Identifiers.member PreIdentifiers.LabelTag visited'
 240                             (Obj.magic nxt) with
 241                     | Bool.True ->
 242                       { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
 243                         (Identifiers.add_set PreIdentifiers.LabelTag
 244                           (Identifiers.empty_set PreIdentifiers.LabelTag)
 245                           (Obj.magic nxt)) }; Types.snd = (List.Cons
 246                         ({ Types.fst = Types.None; Types.snd =
 247                         (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
 248                         x0) }, List.Nil)) }
 249                     | Bool.False ->
 250                       { Types.fst = { Types.fst = Nat.O; Types.snd =
 251                         (Identifiers.empty_set PreIdentifiers.LabelTag) };
 252                         Types.snd = List.Nil }))
 253               | Joint.Final x ->
 254                 { Types.fst = { Types.fst = Nat.O; Types.snd =
 255                   (Identifiers.empty_set PreIdentifiers.LabelTag) };
 256                   Types.snd = List.Nil }
 257               | Joint.FCOND (x0, x1, x2) ->
 258                 { Types.fst = { Types.fst = Nat.O; Types.snd =
 259                   (Identifiers.empty_set PreIdentifiers.LabelTag) };
 260                   Types.snd = List.Nil }
 261             in
 262             graph_visit p globals g
 263               (Identifiers.union_set PreIdentifiers.LabelTag
 264                 add_req_gen.Types.fst.Types.snd required') visited'
 265               (Obj.magic (List.append add_req_gen.Types.snd generated'))
 266               visiting'
 267               (Nat.plus add_req_gen.Types.fst.Types.fst (Nat.S gen_length))
 268               n' entry)) __)) __
 269
 270 (** val branch_compress :
 271     Joint.graph_params -> AST.ident List.list -> __ -> Graphs.label
 272     Types.sig0 -> __ **)
 273 let branch_compress p globals g entry =
 274   g
 275
 276 (** val filter_labels :
 277     PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> Bool.bool)
 278     -> 'a1 LabelledObjects.labelled_obj List.list -> (__, 'a1) Types.prod
 279     List.list **)
 280 let filter_labels tag test c =
 281   List.map (fun s ->
 282     let { Types.fst = l_opt; Types.snd = x } = s in
 283     { Types.fst =
 284     (Monad.m_bind0 (Monad.max_def Option.option) l_opt (fun l ->
 285       match test l with
 286       | Bool.True -> Monad.m_return0 (Monad.max_def Option.option) l
 287       | Bool.False -> Obj.magic Types.None)); Types.snd = x }) (Obj.magic c)
 288
 289 (** val linearise_code :
 290     Joint.uns_params -> AST.ident List.list -> __ -> Graphs.label Types.sig0
 291     -> (__, Graphs.label -> Nat.nat Types.option) Types.prod Types.sig0 **)
 292 let linearise_code p globals g entry_sig =
 293   let g0 = branch_compress p globals g entry_sig in
 294   let triple =
 295     graph_visit p globals g0 (Identifiers.empty_set PreIdentifiers.LabelTag)
 296       (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
 297       (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
 298       (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g0))
 299       (Types.pi1 entry_sig)
 300   in
 301   let sigma = triple.Types.fst.Types.fst in
 302   let required = triple.Types.fst.Types.snd in
 303   let crev = triple.Types.snd in
 304   let lbld_code = Util.rev (Obj.magic crev) in
 305   { Types.fst =
 306   (Obj.magic
 307     (filter_labels PreIdentifiers.LabelTag (fun l ->
 308       Identifiers.member PreIdentifiers.LabelTag required l) lbld_code));
 309   Types.snd = (Identifiers.lookup PreIdentifiers.LabelTag sigma) }
 310
 311 (** val linearise_int_fun :
 312     Joint.uns_params -> AST.ident List.list ->
 313     Joint.joint_closed_internal_function ->
 314     (Joint.joint_closed_internal_function, Graphs.label -> Nat.nat
 315     Types.option) Types.prod Types.sig0 **)
 316 let linearise_int_fun p globals f_sig =
 317   let code_sigma =
 318     linearise_code p globals (Types.pi1 f_sig).Joint.joint_if_code
 319       (Obj.magic (Types.pi1 f_sig).Joint.joint_if_entry)
 320   in
 321   let code = (Types.pi1 code_sigma).Types.fst in
 322   let sigma = (Types.pi1 code_sigma).Types.snd in
 323   { Types.fst = { Joint.joint_if_luniverse =
 324   (Types.pi1 f_sig).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
 325   (Types.pi1 f_sig).Joint.joint_if_runiverse; Joint.joint_if_result =
 326   (Types.pi1 f_sig).Joint.joint_if_result; Joint.joint_if_params =
 327   (Types.pi1 f_sig).Joint.joint_if_params; Joint.joint_if_stacksize =
 328   (Types.pi1 f_sig).Joint.joint_if_stacksize;
 329   Joint.joint_if_local_stacksize =
 330   (Types.pi1 f_sig).Joint.joint_if_local_stacksize; Joint.joint_if_code =
 331   code; Joint.joint_if_entry = (Obj.magic Nat.O) }; Types.snd = sigma }
 332
 333 (** val linearise :
 334     Joint.uns_params -> Joint.joint_program -> Joint.joint_program **)
 335 let linearise p pr =
 336   Joint.transform_joint_program (Joint.graph_params_to_params p)
 337     (Joint.lin_params_to_params p) (fun globals f_in ->
 338     (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst) pr
 339