Changeset 2773 for extracted/policyFront.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/policyFront.ml
r2717 r2773 1 1 open Preamble 2 2 3 open BitVectorTrie 4 3 5 open String 4 6 7 open Exp 8 9 open Arithmetic 10 11 open Vector 12 13 open FoldStuff 14 15 open BitVector 16 17 open Extranat 18 19 open Integers 20 21 open AST 22 5 23 open LabelledObjects 6 24 7 open BitVectorTrie 8 9 open Exp 10 11 open Arithmetic 12 13 open Integers 14 15 open AST 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 Setoids 40 41 open Monad 42 43 open Option 44 45 open Div_and_mod 46 47 open Jmeq 48 49 open Russell 50 51 open Util 52 53 open List 54 55 open Lists 56 57 open Bool 58 59 open Relations 60 61 open Nat 62 63 open Positive 64 65 open Hints_declaration 66 67 open Core_notation 68 69 open Pts 70 71 open Logic 72 73 open Types 74 75 open Identifiers 16 76 17 77 open CostLabel 18 19 open Proper20 21 open PositiveMap22 23 open Deqsets24 25 open ErrorMessages26 27 open PreIdentifiers28 29 open Errors30 31 open Extralib32 33 open Setoids34 35 open Monad36 37 open Option38 39 open Lists40 41 open Positive42 43 open Identifiers44 45 open Extranat46 47 open Vector48 49 open Div_and_mod50 51 open Jmeq52 53 open Russell54 55 open Types56 57 open List58 59 open Util60 61 open FoldStuff62 63 open Bool64 65 open Hints_declaration66 67 open Core_notation68 69 open Pts70 71 open Logic72 73 open Relations74 75 open Nat76 77 open BitVector78 78 79 79 open ASM … … 134 134 135 135 (** val strip_target : 136 ASM.identifier 0ASM.preinstruction > (ASM.subaddressing_mode >136 ASM.identifier ASM.preinstruction > (ASM.subaddressing_mode > 137 137 ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum **) 138 138 let strip_target = function … … 184 184 185 185 (** val expand_relative_jump_unsafe : 186 Assembly.jump_length > ASM.identifier 0ASM.preinstruction >186 Assembly.jump_length > ASM.identifier ASM.preinstruction > 187 187 ASM.instruction List.list **) 188 188 let expand_relative_jump_unsafe jmp_len i = … … 347 347 (** val create_label_map : 348 348 ASM.labelled_instruction List.list > Fetch.label_map Types.sig0 **) 349 let create_label_map program 0=350 (Fetch.create_label_cost_map program 0).Types.fst349 let create_label_map program = 350 (Fetch.create_label_cost_map program).Types.fst 351 351 352 352 (** val select_reljump_length : 353 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 0353 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 354 354 > Nat.nat > Assembly.jump_length **) 355 355 let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len = … … 411 411 412 412 (** val select_call_length : 413 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 0413 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 414 414 > Assembly.jump_length **) 415 415 let select_call_length labels old_sigma inc_sigma ppc lbl = … … 473 473 474 474 (** val select_jump_length : 475 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 0475 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 476 476 > Assembly.jump_length **) 477 477 let select_jump_length labels old_sigma inc_sigma ppc lbl = … … 535 535 536 536 (** val destination_of : 537 ASM.identifier 0 ASM.preinstruction > ASM.identifier0Types.option **)537 ASM.identifier ASM.preinstruction > ASM.identifier Types.option **) 538 538 let destination_of = function 539 539  ASM.ADD (x, x0) > Types.None … … 576 576  ASM.JMP x > Types.None 577 577 578 (** val length_of : ASM.identifier 0ASM.preinstruction > Nat.nat **)578 (** val length_of : ASM.identifier ASM.preinstruction > Nat.nat **) 579 579 let length_of = function 580 580  ASM.ADD (x, x0) > Nat.O … … 639 639 640 640 (** val jump_expansion_step_instruction : 641 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 0641 Fetch.label_map > ppc_pc_map > ppc_pc_map > Nat.nat > ASM.identifier 642 642 ASM.preinstruction > Assembly.jump_length Types.option **) 643 643 let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i = … … 652 652 ASM.labelled_instruction List.list Types.sig0 > Fetch.label_map > 653 653 ppc_pc_map Types.option Types.sig0 **) 654 let jump_expansion_start program 0labels =654 let jump_expansion_start program labels = 655 655 let final_policy = 656 FoldStuff.foldl_strong (Types.pi1 program 0) (fun prefix0x tl _ p >657 let { Types.fst = pc; Types.snd = sigma 0} = Types.pi1 p in656 FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p > 657 let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in 658 658 let { Types.fst = label; Types.snd = instr } = x in 659 659 let isize = instruction_size_jmplen Assembly.Short_jump instr in … … 664 664 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 665 665 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 666 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix 0)))666 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix))) 667 667 { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump } 668 sigma 0) }) { Types.fst = Nat.O; Types.snd =668 sigma) }) { Types.fst = Nat.O; Types.snd = 669 669 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 670 670 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset
for help on using the changeset viewer.