Changeset 2968


Ignore:
Timestamp:
Mar 26, 2013, 7:07:51 PM (4 years ago)
Author:
sacerdot
Message:

The initial status memory was not really initialized. Now it is.

Files:
5 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_fullexec.ml

    r2960 r2968  
    194194    (fun p_stacks ->
    195195    Obj.magic
    196       (Monad.m_return0 (Monad.max_def Errors.res0)
    197         (Traces.make_initial_state { Traces.prog_spars = g; Traces.prog =
    198           (Obj.magic p_stacks).Types.fst; Traces.stack_sizes =
    199           (Obj.magic p_stacks).Types.snd }))) }
     196      (Traces.make_initial_state { Traces.prog_spars = g; Traces.prog =
     197        (Obj.magic p_stacks).Types.fst; Traces.stack_sizes =
     198        (Obj.magic p_stacks).Types.snd })) }
    200199
    201200(** val joint_preclassified_system :
  • extracted/traces.ml

    r2967 r2968  
    503503  joint_make_global x0
    504504
    505 (** val make_initial_state : prog_params -> Joint_semantics.state_pc **)
     505(** val make_initial_state :
     506    prog_params -> Joint_semantics.state_pc Errors.res **)
    506507let make_initial_state pars =
    507508  let p = pars.prog in
    508509  let ge = ev_genv pars.prog_spars in
    509   let m0 =
    510     (Globalenvs.globalenv_allocmem (fun x -> x) p.Joint.joint_prog).Types.snd
    511   in
    512   (let { Types.fst = m; Types.snd = spb } =
    513      GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
    514    in
    515   (fun _ ->
    516   let globals_size =
    517     Joint.globals_stacksize (Joint_semantics.spp'__o__spp pars.prog_spars) p
    518   in
    519   let spp = { Pointers.pblock = spb; Pointers.poff =
    520     (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    521       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    522       Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
    523   in
    524   let main = p.Joint.joint_prog.AST.prog_main in
    525   let st = { Joint_semantics.st_frms = (Types.Some
    526     (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
    527     Joint_semantics.istack = Joint_semantics.Empty_is;
    528     Joint_semantics.carry = (ByteValues.BBbit Bool.False);
    529     Joint_semantics.regs =
    530     ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
    531       spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
    532     globals_size }
    533   in
    534   { Joint_semantics.st_no_pc =
    535   (Joint_semantics.set_sp (prog_spars__o__spp'__o__msu_pars__o__st_pars pars)
    536     spp st); Joint_semantics.pc = Joint_semantics.init_pc;
    537   Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) })) __
     510  Obj.magic
     511    (Monad.m_bind0 (Monad.max_def Errors.res0)
     512      (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog))
     513      (fun m0 ->
     514      (let { Types.fst = m; Types.snd = spb } =
     515         GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
     516       in
     517      (fun _ ->
     518      let globals_size =
     519        Joint.globals_stacksize
     520          (Joint_semantics.spp'__o__spp pars.prog_spars) p
     521      in
     522      let spp = { Pointers.pblock = spb; Pointers.poff =
     523        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     524          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     525          (Nat.S Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
     526      in
     527      let main = p.Joint.joint_prog.AST.prog_main in
     528      let st = { Joint_semantics.st_frms = (Types.Some
     529        (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
     530        Joint_semantics.istack = Joint_semantics.Empty_is;
     531        Joint_semantics.carry = (ByteValues.BBbit Bool.False);
     532        Joint_semantics.regs =
     533        ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
     534          spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
     535        globals_size }
     536      in
     537      Monad.m_return0 (Monad.max_def Errors.res0)
     538        { Joint_semantics.st_no_pc =
     539        (Joint_semantics.set_sp
     540          (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st);
     541        Joint_semantics.pc = Joint_semantics.init_pc;
     542        Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) }))
     543        __))
    538544
    539545(** val joint_classify_step :
  • extracted/traces.mli

    r2960 r2968  
    351351  prog_params -> evaluation_params Types.sig0
    352352
    353 val make_initial_state : prog_params -> Joint_semantics.state_pc
     353val make_initial_state : prog_params -> Joint_semantics.state_pc Errors.res
    354354
    355355val joint_classify_step :
  • src/joint/Traces.ma

    r2967 r2968  
    2323
    2424definition make_initial_state :
    25  ∀pars: prog_params.state_pc pars
     25 ∀pars: prog_params.res (state_pc pars)
    2626λpars.let p ≝ prog pars in
    2727  let ge ≝ ev_genv pars in
    2828  (* this is going to change shortly: globals will not reside in globalenv anymore *)
    29   let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
     29  ! m0 ← init_mem … (λx.x) p ;
    3030  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
    3131  let globals_size ≝ globals_stacksize … p in
     
    4545    (* mem ≝ *)m
    4646    (* stack_usage ≝ *)globals_size in
     47  return
    4748  mk_state_pc ?
    4849    (* state_no_pc ≝ *)(set_sp … spp st)
  • src/joint/joint_fullexec.ma

    r2952 r2968  
    1616    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
    1717    (λp_stacks.
    18       return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
     18      make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
    1919
    2020definition joint_preclassified_system : sem_params →
Note: See TracChangeset for help on using the changeset viewer.