Changeset 2910


Ignore:
Timestamp:
Mar 19, 2013, 11:19:32 PM (4 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).

Files:
6 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2909 r2910  
    209209  | Bool.False -> Types.None
    210210
     211(** val oC_as_call_ident :
     212    ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
     213    Status.status Types.sig0 -> AST.ident **)
     214let oC_as_call_ident prog cm s0 =
     215  let pc =
     216    (Types.pi1 (Interpret.execute_1' cm (Types.pi1 s0))).Status.program_counter
     217  in
     218  (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     219           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     220           (Nat.S Nat.O)))))))))))))))) pc prog.ASM.symboltable with
     221   | Types.None -> assert false (* absurd case *)
     222   | Types.Some id -> id)
     223
    211224(** val oC_abstract_status :
    212225    ASM.labelled_object_code -> StructuredTraces.abstract_status **)
     
    224237  StructuredTraces.as_result = (fun st ->
    225238  as_result_of_finaladdr (Fetch.load_code_memory prog.ASM.oc) (Obj.magic st)
    226     prog.ASM.final_pc); StructuredTraces.as_call_ident = (fun x ->
    227   Positive.One (* absurd case *)); StructuredTraces.as_tailcall_ident =
    228   (fun x -> assert false (* absurd case *)) }
     239    prog.ASM.final_pc); StructuredTraces.as_call_ident =
     240  (Obj.magic (oC_as_call_ident prog code_memory));
     241  StructuredTraces.as_tailcall_ident = (fun clearme ->
     242  let st = clearme in
     243  (match AbstractStatus.current_instruction code_memory (Obj.magic st) with
     244   | ASM.ACALL x ->
     245     (fun _ ->
     246       Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call
     247         StructuredTraces.Cl_tailcall __)
     248   | ASM.LCALL x ->
     249     (fun _ ->
     250       Obj.magic StructuredTraces.status_class_discr StructuredTraces.Cl_call
     251         StructuredTraces.Cl_tailcall __)
     252   | ASM.AJMP x ->
     253     (fun _ ->
     254       Obj.magic StructuredTraces.status_class_discr
     255         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     256   | ASM.LJMP x ->
     257     (fun _ ->
     258       Obj.magic StructuredTraces.status_class_discr
     259         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     260   | ASM.SJMP x ->
     261     (fun _ ->
     262       Obj.magic StructuredTraces.status_class_discr
     263         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     264   | ASM.MOVC (x, y) ->
     265     (fun _ ->
     266       Obj.magic StructuredTraces.status_class_discr
     267         StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     268   | ASM.RealInstruction clearme0 ->
     269     (match clearme0 with
     270      | ASM.ADD (x, y) ->
     271        (fun _ ->
     272          Obj.magic StructuredTraces.status_class_discr
     273            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     274      | ASM.ADDC (x, y) ->
     275        (fun _ ->
     276          Obj.magic StructuredTraces.status_class_discr
     277            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     278      | ASM.SUBB (x, y) ->
     279        (fun _ ->
     280          Obj.magic StructuredTraces.status_class_discr
     281            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     282      | ASM.INC x ->
     283        (fun _ ->
     284          Obj.magic StructuredTraces.status_class_discr
     285            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     286      | ASM.DEC x ->
     287        (fun _ ->
     288          Obj.magic StructuredTraces.status_class_discr
     289            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     290      | ASM.MUL (x, y) ->
     291        (fun _ ->
     292          Obj.magic StructuredTraces.status_class_discr
     293            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     294      | ASM.DIV (x, y) ->
     295        (fun _ ->
     296          Obj.magic StructuredTraces.status_class_discr
     297            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     298      | ASM.DA x ->
     299        (fun _ ->
     300          Obj.magic StructuredTraces.status_class_discr
     301            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     302      | ASM.JC x ->
     303        (fun _ ->
     304          Obj.magic StructuredTraces.status_class_discr
     305            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     306      | ASM.JNC x ->
     307        (fun _ ->
     308          Obj.magic StructuredTraces.status_class_discr
     309            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     310      | ASM.JB (x, y) ->
     311        (fun _ ->
     312          Obj.magic StructuredTraces.status_class_discr
     313            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     314      | ASM.JNB (x, y) ->
     315        (fun _ ->
     316          Obj.magic StructuredTraces.status_class_discr
     317            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     318      | ASM.JBC (x, y) ->
     319        (fun _ ->
     320          Obj.magic StructuredTraces.status_class_discr
     321            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     322      | ASM.JZ x ->
     323        (fun _ ->
     324          Obj.magic StructuredTraces.status_class_discr
     325            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     326      | ASM.JNZ x ->
     327        (fun _ ->
     328          Obj.magic StructuredTraces.status_class_discr
     329            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     330      | ASM.CJNE (x, y) ->
     331        (fun _ ->
     332          Obj.magic StructuredTraces.status_class_discr
     333            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     334      | ASM.DJNZ (x, y) ->
     335        (fun _ ->
     336          Obj.magic StructuredTraces.status_class_discr
     337            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     338      | ASM.ANL x ->
     339        (fun _ ->
     340          Obj.magic StructuredTraces.status_class_discr
     341            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     342      | ASM.ORL x ->
     343        (fun _ ->
     344          Obj.magic StructuredTraces.status_class_discr
     345            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     346      | ASM.XRL x ->
     347        (fun _ ->
     348          Obj.magic StructuredTraces.status_class_discr
     349            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     350      | ASM.CLR x ->
     351        (fun _ ->
     352          Obj.magic StructuredTraces.status_class_discr
     353            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     354      | ASM.CPL x ->
     355        (fun _ ->
     356          Obj.magic StructuredTraces.status_class_discr
     357            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     358      | ASM.RL x ->
     359        (fun _ ->
     360          Obj.magic StructuredTraces.status_class_discr
     361            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     362      | ASM.RLC x ->
     363        (fun _ ->
     364          Obj.magic StructuredTraces.status_class_discr
     365            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     366      | ASM.RR x ->
     367        (fun _ ->
     368          Obj.magic StructuredTraces.status_class_discr
     369            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     370      | ASM.RRC x ->
     371        (fun _ ->
     372          Obj.magic StructuredTraces.status_class_discr
     373            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     374      | ASM.SWAP x ->
     375        (fun _ ->
     376          Obj.magic StructuredTraces.status_class_discr
     377            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     378      | ASM.MOV x ->
     379        (fun _ ->
     380          Obj.magic StructuredTraces.status_class_discr
     381            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     382      | ASM.MOVX x ->
     383        (fun _ ->
     384          Obj.magic StructuredTraces.status_class_discr
     385            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     386      | ASM.SETB x ->
     387        (fun _ ->
     388          Obj.magic StructuredTraces.status_class_discr
     389            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     390      | ASM.PUSH x ->
     391        (fun _ ->
     392          Obj.magic StructuredTraces.status_class_discr
     393            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     394      | ASM.POP x ->
     395        (fun _ ->
     396          Obj.magic StructuredTraces.status_class_discr
     397            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     398      | ASM.XCH (x, y) ->
     399        (fun _ ->
     400          Obj.magic StructuredTraces.status_class_discr
     401            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     402      | ASM.XCHD (x, y) ->
     403        (fun _ ->
     404          Obj.magic StructuredTraces.status_class_discr
     405            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     406      | ASM.RET ->
     407        (fun _ ->
     408          Obj.magic StructuredTraces.status_class_discr
     409            StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
     410      | ASM.RETI ->
     411        (fun _ ->
     412          Obj.magic StructuredTraces.status_class_discr
     413            StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
     414      | ASM.NOP ->
     415        (fun _ ->
     416          Obj.magic StructuredTraces.status_class_discr
     417            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     418      | ASM.JMP x ->
     419        (fun _ ->
     420          Obj.magic StructuredTraces.status_class_discr
     421            StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))) __) }
    229422
    230423(** val trace_any_label_length :
     
    313506   | Nat.S program_size' ->
    314507     (fun _ ->
    315        (let { Types.fst = eta31815; Types.snd = ticks } =
     508       (let { Types.fst = eta16; Types.snd = ticks } =
    316509          Fetch.fetch (Fetch.load_code_memory prog.ASM.oc) program_counter'
    317510        in
    318        let { Types.fst = instruction; Types.snd = program_counter'' } =
    319          eta31815
     511       let { Types.fst = instruction; Types.snd = program_counter'' } = eta16
    320512       in
    321513       (fun _ ->
  • extracted/aSMCosts.mli

    r2909 r2910  
    120120  'a1 -> 'a1 Status.preStatus -> BitVector.word -> Integers.int Types.option
    121121
     122val oC_as_call_ident :
     123  ASM.labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie ->
     124  Status.status Types.sig0 -> AST.ident
     125
    122126val oC_abstract_status :
    123127  ASM.labelled_object_code -> StructuredTraces.abstract_status
  • 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 :
  • extracted/interpret2.mli

    r2909 r2910  
    159159  Types.option
    160160
     161open AssocList
     162
     163val aSM_as_call_ident :
     164  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     165  (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
     166  AST.ident
     167
    161168val aSM_abstract_status :
    162169  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
  • src/ASM/ASMCosts.ma

    r2907 r2910  
    2525qed.
    2626
     27definition OC_as_call_ident:
     28 ∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident
     29
     30 λprog,cm,s0.
     31  let pc ≝ program_counter ?? (execute_1' cm s0) in
     32  match lookup_opt ?? pc (symboltable prog) with
     33  [ None ⇒ ⊥ | Some id ⇒ id ].
     34cases daemon (*CSC: we need a specification of the symboltable for this *)
     35qed.
     36
    2737definition OC_abstract_status: labelled_object_code → abstract_status ≝
    2838 λprog.
     
    3747      (next_instruction_properly_relates_program_counters code_memory)
    3848      (λst. as_result_of_finaladdr … st (final_pc prog))
    39       ?
     49      (OC_as_call_ident prog …)
    4050      ?.
    41   #x cases daemon (* XXX: (tail)call_ident function *)
     51 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
     52 try (#x #y #abs) try (#x #abs) try #abs destruct
    4253qed.
    4354
  • src/ASM/Interpret2.ma

    r2907 r2910  
    105105   as_result_of_finaladdr … st finaladdr.
    106106
     107include "common/AssocList.ma".
     108
     109definition ASM_as_call_ident:
     110 ∀prog,sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
     111
     112 λprog,sigma,policy,s0.
     113  let st ≝ execute_1_pseudo_instruction' prog sigma policy s0 in
     114  let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
     115  match lbl with
     116  [ None ⇒ ⊥
     117  | Some lbl' ⇒
     118     match assoc_list_lookup ?? lbl' (eq_identifier …) (renamed_symbols prog) with
     119     [ None ⇒ ⊥ | Some id ⇒ id ]].
     120cases daemon (*CSC: we need a specification of the renamed_symbols for this *)
     121qed.
     122
    107123definition ASM_abstract_status:
    108124 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
     
    117133      (ASM_next_instruction_properly_relates_program_counters prog)
    118134      (ASM_as_result …)
    119       ?
     135      (ASM_as_call_ident prog sigma policy …)
    120136      ?.
    121   #x cases daemon (* XXX: (tail)call_ident function *)
     137 * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
     138 normalize try (#x #y #abs) try (#x #abs) try #abs destruct (abs)
    122139qed.
    123140
Note: See TracChangeset for help on using the changeset viewer.