Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (8 years ago)
Author:
sacerdot
Message:

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/interpret2.ml

    r2880 r2905  
    165165  let cm = Fetch.load_code_memory c.ASM.oc in
    166166  mk_preclassified_system_of_abstract_status
    167     (ASMCosts.aSM_abstract_status cm c.ASM.costlabels) (fun st ->
     167    (ASMCosts.oC_abstract_status cm c.ASM.costlabels) (fun st ->
    168168    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
    169169      (Interpret.execute_1 (Fetch.load_code_memory c.ASM.oc) (Obj.magic st)))
    170170    (Obj.magic (Status.initialise_status cm))
    171171
     172open Assembly
     173
     174(** val execute_1_pseudo_instruction' :
     175    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     176    (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
     177    Status.pseudoStatus **)
     178let execute_1_pseudo_instruction' cm sigma policy status =
     179  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
     180    Assembly.ticks_of cm sigma policy x) status
     181
     182(** val classify_pseudo_instruction :
     183    ASM.pseudo_instruction -> StructuredTraces.status_class **)
     184let classify_pseudo_instruction = function
     185| ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
     186| ASM.Comment x -> StructuredTraces.Cl_other
     187| ASM.Cost x -> StructuredTraces.Cl_other
     188| ASM.Jmp x -> StructuredTraces.Cl_other
     189| ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
     190| ASM.MovSuccessor (x, x0, x1) -> StructuredTraces.Cl_other
     191| ASM.Call x -> StructuredTraces.Cl_call
     192| ASM.Mov (x, x0) -> StructuredTraces.Cl_other
     193
     194(** val aSM_classify :
     195    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
     196    StructuredTraces.status_class **)
     197let aSM_classify cm s =
     198  classify_pseudo_instruction
     199    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
     200
     201(** val aSM_as_label_of_pc :
     202    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
     203    Types.option **)
     204let aSM_as_label_of_pc prog pc =
     205  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
     206  | ASM.Instruction x -> Types.None
     207  | ASM.Comment x -> Types.None
     208  | ASM.Cost label -> Types.Some label
     209  | ASM.Jmp x -> Types.None
     210  | ASM.Jnz (x, x0, x1) -> Types.None
     211  | ASM.MovSuccessor (x, x0, x1) -> Types.None
     212  | ASM.Call x -> Types.None
     213  | ASM.Mov (x, x0) -> Types.None
     214
     215(** val aSM_abstract_status :
     216    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     217    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
     218let aSM_abstract_status prog sigma policy =
     219  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
     220    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
     221    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
     222    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
     223    StructuredTraces.as_result = (fun x -> Types.None);
     224    StructuredTraces.as_call_ident = (fun x -> Positive.One
     225    (* absurd case *)); StructuredTraces.as_tailcall_ident = (fun x ->
     226    assert false (* absurd case *)) }
     227
     228(** val aSM_preclassified_system :
     229    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     230    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
     231let aSM_preclassified_system c sigma policy =
     232  mk_preclassified_system_of_abstract_status
     233    (aSM_abstract_status c sigma policy) (fun st ->
     234    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
     235      (execute_1_pseudo_instruction' c sigma policy (Obj.magic st)))
     236    (Obj.magic (Status.initialise_status c))
     237
Note: See TracChangeset for help on using the changeset viewer.