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