Changeset 2824 for src


Ignore:
Timestamp:
Mar 8, 2013, 5:37:57 PM (7 years ago)
Author:
tranquil
Message:
  • moved sum on lists notation to extranat
  • used sum on lists to define portion of stack occupied by globals
  • corrected probable bug in joint semantics, where initial state would not move stack pointer past globals before setting up main
Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2819 r2824  
    448448qed.
    449449
    450 definition first_free_stack_addr : ltl_program → nat ≝
    451  λp.
    452   let globals_addr_internal ≝
    453    λoffset : nat.
    454    λx_size: ident × region × nat.
    455     let 〈x, region, size〉 ≝ x_size in
    456      offset + size in
    457  foldl … globals_addr_internal 0 (prog_vars … p).
    458 
     450(* Paolo: does it really have sense to do here the first stack address computation,
     451   when it is an info easily available from any program in the back end?
     452   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
    459453definition ertlptr_to_ltl:
    460454 fixpoint_computer → coloured_graph_computer → ertlptr_program →
     
    462456  λthe_fixpoint,build,pr.
    463457   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    464    〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
     458   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
    465459%
    466460qed.
  • src/common/StructuredTraces.ma

    r2769 r2824  
    104104#a #H #G [ % | @⊥ /2 by absurd/ ]
    105105qed.
    106 
    107 notation > "Σ_{ ident i ∈ l } f"
    108   with precedence 20
    109   for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
    110 notation < "Σ_{ ident i ∈ l } f"
    111   with precedence 20
    112 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
    113106
    114107definition lift_cost_map_id :
  • src/joint/Joint.ma

    r2823 r2824  
    603603   [ ] (prog_funct ?? pr).
    604604
     605definition globals_stacksize : ∀p.joint_program p → nat ≝
     606 λpars,p.
     607 Σ_{entry ∈ prog_vars … p}(\snd entry).
     608
  • src/joint/Traces.ma

    r2821 r2824  
    7272  let m0 ≝ alloc_mem … p in
    7373  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
     74  let globals_size ≝ globals_stacksize … p in
     75  (* stack pointer should start at 2^16 - |globals|, right?
     76     first call to main shuold bring it to 2^16 - |globals| - |main stack|
     77     Also, on words 2^16 - |globals| = - |globals| *)
    7478  let spp : xpointer ≝
    75     «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
     79    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-globals_size))),
    7680     pi2 … spb» in
    7781(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
  • src/utilities/extranat.ma

    r2767 r2824  
    167167qed.
    168168
     169(* notation for sum *)
     170notation > "Σ_{ ident i ∈ l } f"
     171  with precedence 20
     172  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
     173notation < "hvbox(Σ_{ ident i break ∈ l } break f)"
     174  with precedence 20
     175for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     176
Note: See TracChangeset for help on using the changeset viewer.