Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret.ml

    r2717 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
     5open String
     6
     7open Exp
     8
     9open Arithmetic
     10
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
     19open Integers
     20
     21open AST
     22
     23open LabelledObjects
     24
     25open Proper
     26
     27open PositiveMap
     28
    329open Deqsets
    430
     31open ErrorMessages
     32
     33open PreIdentifiers
     34
     35open Errors
     36
     37open Extralib
     38
     39open Setoids
     40
     41open Monad
     42
     43open Option
     44
     45open Div_and_mod
     46
     47open Jmeq
     48
     49open Russell
     50
     51open Util
     52
     53open List
     54
     55open Lists
     56
     57open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
     64
     65open Hints_declaration
     66
     67open Core_notation
     68
     69open Pts
     70
     71open Logic
     72
     73open Types
     74
     75open Identifiers
     76
     77open CostLabel
     78
     79open ASM
     80
     81open Status
     82
     83open StatusProofs
     84
     85open Fetch
     86
     87open Hide
     88
     89open Division
     90
     91open Z
     92
     93open BitVectorZ
     94
     95open Pointers
     96
     97open Coqlib
     98
     99open Values
     100
     101open Events
     102
     103open IOMonad
     104
     105open IO
     106
    5107open Sets
    6108
    7 open Bool
    8 
    9 open Relations
    10 
    11 open Nat
    12 
    13 open Hints_declaration
    14 
    15 open Core_notation
    16 
    17 open Pts
    18 
    19 open Logic
    20 
    21 open Types
    22 
    23 open List
    24 
    25109open Listb
    26 
    27 open String
    28 
    29 open LabelledObjects
    30 
    31 open BitVectorTrie
    32 
    33 open Exp
    34 
    35 open Arithmetic
    36 
    37 open Integers
    38 
    39 open AST
    40 
    41 open CostLabel
    42 
    43 open Proper
    44 
    45 open PositiveMap
    46 
    47 open ErrorMessages
    48 
    49 open PreIdentifiers
    50 
    51 open Errors
    52 
    53 open Extralib
    54 
    55 open Setoids
    56 
    57 open Monad
    58 
    59 open Option
    60 
    61 open Lists
    62 
    63 open Positive
    64 
    65 open Identifiers
    66 
    67 open Extranat
    68 
    69 open Vector
    70 
    71 open Div_and_mod
    72 
    73 open Jmeq
    74 
    75 open Russell
    76 
    77 open Util
    78 
    79 open FoldStuff
    80 
    81 open BitVector
    82 
    83 open ASM
    84 
    85 open Status
    86 
    87 open StatusProofs
    88 
    89 open Fetch
    90110
    91111open StructuredTraces
     
    572592             in
    573593             let new_acc =
    574                Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S
     594               Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S
    575595                 (Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl'
    576596             in
     
    14661486       in
    14671487       let new_acc =
    1468          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     1488         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    14691489           (Nat.S (Nat.S Nat.O)))) nl nu
    14701490       in
     
    18401860       in
    18411861       let new_acc =
    1842          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     1862         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    18431863           (Nat.S (Nat.S Nat.O)))) acc_nu arg_nl
    18441864       in
    18451865       let new_arg =
    1846          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     1866         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    18471867           (Nat.S (Nat.S Nat.O)))) arg_nu acc_nl
    18481868       in
     
    18791899       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
    18801900       let new_pc =
    1881          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1901         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    18821902           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    18831903           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
     
    19041924       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
    19051925       let new_pc =
    1906          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1926         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    19071927           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    19081928           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
     
    19141934       let s0 = add_ticks1 s in
    19151935       let dptr =
    1916          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1936         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    19171937           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    19181938           (Nat.S (Nat.S Nat.O))))))))
     
    19211941       in
    19221942       let big_acc =
    1923          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1943         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    19241944           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    19251945           (Nat.S (Nat.S Nat.O))))))))
     
    24362456                 in
    24372457                 let new_acc =
    2438                    Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
    2439                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl'
     2458                   Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S
     2459                     (Nat.S (Nat.S (Nat.S Nat.O)))) nu acc_nl'
    24402460                 in
    24412461                 let s1 = Status.set_8051_sfr cm s0 Status.SFR_ACC_A new_acc
     
    33413361       (fun _ ->
    33423362       let new_acc =
    3343          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     3363         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    33443364           (Nat.S (Nat.S Nat.O)))) nl nu
    33453365       in
     
    37263746       (fun _ ->
    37273747       let new_acc =
    3728          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     3748         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    37293749           (Nat.S (Nat.S Nat.O)))) acc_nu arg_nl
    37303750       in
    37313751       let new_arg =
    3732          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     3752         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    37333753           (Nat.S (Nat.S Nat.O)))) arg_nu acc_nl
    37343754       in
     
    37683788       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
    37693789       let new_pc =
    3770          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3790         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    37713791           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    37723792           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
     
    37953815       let s2 = Status.set_8051_sfr cm s1 Status.SFR_SP new_sp0 in
    37963816       let new_pc =
    3797          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3817         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    37983818           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    37993819           (Nat.S (Nat.S Nat.O)))))))) high_bits low_bits
     
    38053825       let s0 = add_ticks1 s in
    38063826       let dptr =
    3807          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3827         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38083828           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38093829           (Nat.S (Nat.S Nat.O))))))))
     
    38123832       in
    38133833       let big_acc =
    3814          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3834         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38153835           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38163836           (Nat.S (Nat.S Nat.O))))))))
     
    38343854(** val compute_target_of_unconditional_jump :
    38353855    BitVector.word -> ASM.instruction -> BitVector.word **)
    3836 let compute_target_of_unconditional_jump program_counter0 = function
     3856let compute_target_of_unconditional_jump program_counter = function
    38373857| ASM.ACALL x ->
    38383858  BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    38693889             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    38703890               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3871                (Nat.S (Nat.S Nat.O))))))))))) program_counter0
     3891               (Nat.S (Nat.S Nat.O))))))))))) program_counter
    38723892           in
    38733893          (fun _ ->
    38743894          let new_addr =
    3875             Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     3895            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    38763896              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38773897              (Nat.S (Nat.S Nat.O))))))))))) pc_bu a
     
    39263946          Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    39273947            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3928             Nat.O)))))))))))))))) program_counter0
     3948            Nat.O)))))))))))))))) program_counter
    39293949            (Arithmetic.sign_extension r))
    39303950      | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
     
    39513971(** val program_counter_after_other :
    39523972    BitVector.word -> ASM.instruction -> BitVector.word **)
    3953 let program_counter_after_other program_counter0 instruction0 =
    3954   match is_unconditional_jump instruction0 with
     3973let program_counter_after_other program_counter instruction =
     3974  match is_unconditional_jump instruction with
    39553975  | Bool.True ->
    3956     compute_target_of_unconditional_jump program_counter0 instruction0
    3957   | Bool.False -> program_counter0
     3976    compute_target_of_unconditional_jump program_counter instruction
     3977  | Bool.False -> program_counter
    39583978
    39593979(** val addr_of_relative :
     
    40524072            in
    40534073            let new_addr =
    4054               Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     4074              Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    40554075                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    40564076                (Nat.S (Nat.S (Nat.S Nat.O))))))))))) fiv a
     
    41464166          (fun _ ->
    41474167            let big_acc =
    4148               Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4168              Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41494169                (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41504170                (Nat.S (Nat.S (Nat.S Nat.O))))))))
     
    41544174            in
    41554175            let dptr =
    4156               Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4176              Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41574177                (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41584178                (Nat.S (Nat.S (Nat.S Nat.O))))))))
     
    41784198          (fun _ ->
    41794199            let big_acc =
    4180               Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4200              Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41814201                (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41824202                (Nat.S (Nat.S (Nat.S Nat.O))))))))
     
    42404260    | ASM.Instruction instr0 ->
    42414261      execute_1_preinstruction ticks cm (fun x y ->
    4242         Fetch.address_of_word_labels cm.Types.snd x) instr0 s0
     4262        Fetch.address_of_word_labels cm.ASM.code x) instr0 s0
    42434263    | ASM.Comment cmt ->
    42444264      Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
     
    42494269      in
    42504270      Status.set_program_counter cm s1
    4251         (Fetch.address_of_word_labels cm.Types.snd jmp)
     4271        (Fetch.address_of_word_labels cm.ASM.code jmp)
    42524272    | ASM.Jnz (acc, dst1, dst2) ->
    42534273      (match Bool.notb
     
    42624282         in
    42634283         Status.set_program_counter cm s1
    4264            (Fetch.address_of_word_labels cm.Types.snd dst1)
     4284           (Fetch.address_of_word_labels cm.ASM.code dst1)
    42654285       | Bool.False ->
    42664286         let s1 =
     
    42684288         in
    42694289         Status.set_program_counter cm s1
    4270            (Fetch.address_of_word_labels cm.Types.snd dst2))
     4290           (Fetch.address_of_word_labels cm.ASM.code dst2))
    42714291    | ASM.MovSuccessor (dst, ws, lbl) ->
    42724292      let s1 =
    42734293        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    42744294      in
    4275       let addr = Fetch.address_of_word_labels cm.Types.snd lbl in
     4295      let addr = Fetch.address_of_word_labels cm.ASM.code lbl in
    42764296      let { Types.fst = high; Types.snd = low } =
    42774297        Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    43014321        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    43024322      in
    4303       let a = Fetch.address_of_word_labels cm.Types.snd call in
     4323      let a = Fetch.address_of_word_labels cm.ASM.code call in
    43044324      let new_sp =
    43054325        Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    43244344      let s5 = Status.write_at_stack_pointer cm s4 pc_bu in
    43254345      Status.set_program_counter cm s5 a
    4326     | ASM.Mov (dptr, ident0) ->
     4346    | ASM.Mov (dptr, ident) ->
    43274347      let s1 =
    43284348        Status.set_clock cm s0 (Nat.plus ticks.Types.fst s0.Status.clock)
    43294349      in
    4330       let the_preamble = cm.Types.fst in
     4350      let the_preamble = cm.ASM.preamble in
    43314351      let data_labels = Status.construct_datalabels the_preamble in
    43324352      Status.set_arg_16 cm s1
    43334353        (Status.get_arg_16 cm s1 (ASM.DATA16
    4334           (Identifiers.lookup_def PreIdentifiers.ASMTag data_labels ident0
     4354          (Identifiers.lookup_def PreIdentifiers.ASMTag data_labels ident
    43354355            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    43364356              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    43404360
    43414361(** val execute_1_pseudo_instruction :
    4342     (ASM.preamble, ASM.labelled_instruction List.list) Types.prod ->
    4343     (BitVector.word -> __ -> (Nat.nat, Nat.nat) Types.prod) ->
    4344     Status.pseudoStatus -> Status.pseudoStatus **)
     4362    ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat,
     4363    Nat.nat) Types.prod) -> Status.pseudoStatus -> Status.pseudoStatus **)
    43454364let execute_1_pseudo_instruction cm ticks_of s =
    43464365  let { Types.fst = instr; Types.snd = pc } =
    4347     Status.fetch_pseudo_instruction cm.Types.snd s.Status.program_counter
     4366    ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter
    43484367  in
    43494368  let ticks = ticks_of s.Status.program_counter __ in
Note: See TracChangeset for help on using the changeset viewer.