Ignore:
Timestamp:
Mar 19, 2013, 11:19:32 PM (8 years ago)
Author:
sacerdot
Message:

Abstract statuses for ASM and OC completed.
A simple test program can now be run in every pass of the compiler, always
showing the same behaviour (up to initialization).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret2.ml

    r2909 r2910  
    221221  ASMCosts.as_result_of_finaladdr prog st finaladdr
    222222
     223open AssocList
     224
     225(** val aSM_as_call_ident :
     226    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     227    (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
     228    AST.ident **)
     229let aSM_as_call_ident prog sigma policy s0 =
     230  let st = execute_1_pseudo_instruction' prog sigma policy (Types.pi1 s0) in
     231  let { Types.fst = lbl; Types.snd = instr } =
     232    Util.nth_safe
     233      (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     234        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     235        Nat.O)))))))))))))))) st.Status.program_counter) prog.ASM.code
     236  in
     237  (match lbl with
     238   | Types.None -> assert false (* absurd case *)
     239   | Types.Some lbl' ->
     240     (match AssocList.assoc_list_lookup lbl'
     241              (Identifiers.eq_identifier PreIdentifiers.ASMTag)
     242              prog.ASM.renamed_symbols with
     243      | Types.None -> assert false (* absurd case *)
     244      | Types.Some id -> id))
     245
    223246(** val aSM_abstract_status :
    224247    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     
    230253    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
    231254    StructuredTraces.as_result = (Obj.magic (aSM_as_result prog));
    232     StructuredTraces.as_call_ident = (fun x -> Positive.One
    233     (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
    234     assert false (* absurd case *)) }
     255    StructuredTraces.as_call_ident =
     256    (Obj.magic (aSM_as_call_ident prog sigma policy));
     257    StructuredTraces.as_tailcall_ident = (fun clearme ->
     258    let st = clearme in
     259    (match (ASM.fetch_pseudo_instruction prog.ASM.code
     260             (Obj.magic st).Status.program_counter).Types.fst with
     261     | ASM.Instruction clearme0 ->
     262       (match clearme0 with
     263        | ASM.ADD (x, y) ->
     264          (fun _ ->
     265            Obj.magic StructuredTraces.status_class_discr
     266              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     267        | ASM.ADDC (x, y) ->
     268          (fun _ ->
     269            Obj.magic StructuredTraces.status_class_discr
     270              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     271        | ASM.SUBB (x, y) ->
     272          (fun _ ->
     273            Obj.magic StructuredTraces.status_class_discr
     274              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     275        | ASM.INC x ->
     276          (fun _ ->
     277            Obj.magic StructuredTraces.status_class_discr
     278              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     279        | ASM.DEC x ->
     280          (fun _ ->
     281            Obj.magic StructuredTraces.status_class_discr
     282              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     283        | ASM.MUL (x, y) ->
     284          (fun _ ->
     285            Obj.magic StructuredTraces.status_class_discr
     286              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     287        | ASM.DIV (x, y) ->
     288          (fun _ ->
     289            Obj.magic StructuredTraces.status_class_discr
     290              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     291        | ASM.DA x ->
     292          (fun _ ->
     293            Obj.magic StructuredTraces.status_class_discr
     294              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     295        | ASM.JC x ->
     296          (fun _ ->
     297            Obj.magic StructuredTraces.status_class_discr
     298              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     299        | ASM.JNC x ->
     300          (fun _ ->
     301            Obj.magic StructuredTraces.status_class_discr
     302              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     303        | ASM.JB (x, y) ->
     304          (fun _ ->
     305            Obj.magic StructuredTraces.status_class_discr
     306              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     307        | ASM.JNB (x, y) ->
     308          (fun _ ->
     309            Obj.magic StructuredTraces.status_class_discr
     310              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     311        | ASM.JBC (x, y) ->
     312          (fun _ ->
     313            Obj.magic StructuredTraces.status_class_discr
     314              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     315        | ASM.JZ x ->
     316          (fun _ ->
     317            Obj.magic StructuredTraces.status_class_discr
     318              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     319        | ASM.JNZ x ->
     320          (fun _ ->
     321            Obj.magic StructuredTraces.status_class_discr
     322              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     323        | ASM.CJNE (x, y) ->
     324          (fun _ ->
     325            Obj.magic StructuredTraces.status_class_discr
     326              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     327        | ASM.DJNZ (x, y) ->
     328          (fun _ ->
     329            Obj.magic StructuredTraces.status_class_discr
     330              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     331        | ASM.ANL x ->
     332          (fun _ ->
     333            Obj.magic StructuredTraces.status_class_discr
     334              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     335        | ASM.ORL x ->
     336          (fun _ ->
     337            Obj.magic StructuredTraces.status_class_discr
     338              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     339        | ASM.XRL x ->
     340          (fun _ ->
     341            Obj.magic StructuredTraces.status_class_discr
     342              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     343        | ASM.CLR x ->
     344          (fun _ ->
     345            Obj.magic StructuredTraces.status_class_discr
     346              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     347        | ASM.CPL x ->
     348          (fun _ ->
     349            Obj.magic StructuredTraces.status_class_discr
     350              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     351        | ASM.RL x ->
     352          (fun _ ->
     353            Obj.magic StructuredTraces.status_class_discr
     354              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     355        | ASM.RLC x ->
     356          (fun _ ->
     357            Obj.magic StructuredTraces.status_class_discr
     358              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     359        | ASM.RR x ->
     360          (fun _ ->
     361            Obj.magic StructuredTraces.status_class_discr
     362              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     363        | ASM.RRC x ->
     364          (fun _ ->
     365            Obj.magic StructuredTraces.status_class_discr
     366              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     367        | ASM.SWAP x ->
     368          (fun _ ->
     369            Obj.magic StructuredTraces.status_class_discr
     370              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     371        | ASM.MOV x ->
     372          (fun _ ->
     373            Obj.magic StructuredTraces.status_class_discr
     374              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     375        | ASM.MOVX x ->
     376          (fun _ ->
     377            Obj.magic StructuredTraces.status_class_discr
     378              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     379        | ASM.SETB x ->
     380          (fun _ ->
     381            Obj.magic StructuredTraces.status_class_discr
     382              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     383        | ASM.PUSH x ->
     384          (fun _ ->
     385            Obj.magic StructuredTraces.status_class_discr
     386              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     387        | ASM.POP x ->
     388          (fun _ ->
     389            Obj.magic StructuredTraces.status_class_discr
     390              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     391        | ASM.XCH (x, y) ->
     392          (fun _ ->
     393            Obj.magic StructuredTraces.status_class_discr
     394              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     395        | ASM.XCHD (x, y) ->
     396          (fun _ ->
     397            Obj.magic StructuredTraces.status_class_discr
     398              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     399        | ASM.RET ->
     400          (fun _ ->
     401            Obj.magic StructuredTraces.status_class_discr
     402              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
     403        | ASM.RETI ->
     404          (fun _ ->
     405            Obj.magic StructuredTraces.status_class_discr
     406              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
     407        | ASM.NOP ->
     408          (fun _ ->
     409            Obj.magic StructuredTraces.status_class_discr
     410              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     411        | ASM.JMP x ->
     412          (fun _ ->
     413            Obj.magic StructuredTraces.status_class_discr
     414              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
     415     | ASM.Comment x ->
     416       (fun _ ->
     417         Obj.magic StructuredTraces.status_class_discr
     418           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     419     | ASM.Cost x ->
     420       (fun _ ->
     421         Obj.magic StructuredTraces.status_class_discr
     422           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     423     | ASM.Jmp x ->
     424       (fun _ ->
     425         Obj.magic StructuredTraces.status_class_discr
     426           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     427     | ASM.Jnz (x, y, abs) ->
     428       (fun _ ->
     429         Obj.magic StructuredTraces.status_class_discr
     430           StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     431     | ASM.MovSuccessor (x, y, abs) ->
     432       (fun _ ->
     433         Obj.magic StructuredTraces.status_class_discr
     434           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     435     | ASM.Call x ->
     436       (fun _ ->
     437         Obj.magic StructuredTraces.status_class_discr
     438           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
     439     | ASM.Mov (x, y) ->
     440       (fun _ ->
     441         Obj.magic StructuredTraces.status_class_discr
     442           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }
    235443
    236444(** val aSM_preclassified_system :
Note: See TracChangeset for help on using the changeset viewer.