Changeset 2286 for src/joint


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/joint
Files:
4 deleted
8 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r2185 r2286  
    2020  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
    2121
    22 
    2322definition is_address : (beval × beval) → Prop ≝ λa.
    24   ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
    25     \fst a = BVptr p p0 ∧ part_no … p0 = 0 ∧
    26     \snd a = BVptr p p1 ∧ part_no … p1 = 1.
    27 
     23  ∃b : Σb.bool_to_Prop (is_addressable (block_region b)).
     24  ∃p0,p1,o0,o1.
     25    \fst a = BVptr b p0 o0 ∧ part_no … p0 = 0 ∧
     26    \snd a = BVptr b p1 o1 ∧ part_no … p1 = 1 ∧
     27    bool_to_Prop (vsuffix … (eq_bv 8) o0 o1).
     28
     29(*
    2830definition is_addressb : (beval × beval) → bool ≝ λa.
    29   match a with
    30   [ mk_Prod a0 a1 ⇒
    31     match a0 with
    32     [ BVptr p0 part0 ⇒
    33       is_addressable (ptype p0) ∧ eqb part0 0 ∧
     31  let 〈a0,a1〉 ≝ a in
     32  match a0 with
     33  [ BVptr b0 part0 o0 ⇒
     34      is_addressable (block_region b0) ∧ eqb part0 0 ∧
    3435        match a1 with
    35         [ BVptr p1 part1 ⇒
    36           eq_pointer p0 p1 ∧ eqb part1 1
     36        [ BVptr b1 part1 o1 ⇒
     37          eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o1
    3738        | _ ⇒ false
    3839        ]
    39     | _ ⇒ false
    40     ]
     40  | _ ⇒ false
    4141  ].
    4242
    4343lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
    4444  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
    45 #P * *
    46 [4:|*: [|#b0|(*#r0*)#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
    47 #p0 #part0 #a1
    48 whd in match is_addressb; normalize nodelta
    49 elim (true_or_false_Prop (is_addressable (ptype p0)))
    50 #H >H
    51 [ @(eqb_elim part0 0) #Heq
    52   [ cases a1 [|#b0|(*#r0*)#part0|#p1#part1] whd in match (?∧?);
    53     [4: @eq_pointer_elim #Heq'
    54       [ @(eqb_elim part1 1) #Heq''
    55         [ #Ptrue #_ @Ptrue destruct
    56           %{p1} [assumption] %{part0} %{part1}
    57           % [ % [ % ]] try % assumption
     45#P * * [||#b0|(*#r0*)#part0|#b0#part0#o0] #a1
     46[5: whd in match is_addressb; normalize nodelta
     47  elim (true_or_false_Prop (is_addressable (block_region b0)))
     48  #H >H
     49  [ @(eqb_elim part0 0) #Heq
     50    [ cases a1 [||#b1|(*#r1*)#part1|#b1#part1#o1] whd in match (?∧?);
     51      [5: @eq_block_elim #Heq'
     52        [ @(eqb_elim part1 1) #Heq''
     53          [ elim (true_or_false_Prop (subvector_with … (eq_bv 8) o0 o1)) #Heq''' >Heq'''
     54            [ #Ptrue #_ @Ptrue destruct
     55              %{b1} [assumption] %{part0} %{part1} %{o0} %{o1}
     56              % [ % [ % [ % ]]] try assumption %
     57            ]
     58          ]
    5859        ]
    5960      ]
     
    6162  ]
    6263]
    63 #_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
    64 #H0 #H1 #H2 #H3 destruct /2 by absurd/
    65 qed.
     64#_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' ****
     65#H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/
     66qed.
     67*)
    6668
    6769(* CSC: only pointers to XRAM or code memory ATM *)
    6870definition address ≝ beval × beval.
    69 definition safe_address ≝ Sig address is_address.
     71
     72(* definition safe_address ≝ Sig address is_address.
    7073unification hint 0 ≔ ;
    7174P ≟ Prod beval beval
    7275(*------------------*)⊢
    73 safe_address ≡ Sig P is_address.
     76safe_address ≡ Sig P is_address. *)
    7477
    7578definition eq_address: address → address → bool ≝
     
    7982definition pointer_of_address: address → res pointer ≝
    8083 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
    81  
    82 definition pointer_of_address_safe : safe_address → pointer ≝
    83   λp.match \fst p return λx.\fst p = x → ? with
    84     [ BVptr ptr _ ⇒ λ_.ptr
    85     | _ ⇒ λabs.⊥
    86     ] (refl …).
    87 lapply abs -abs cases p
    88 * #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
    89 destruct(H0 H4)
    90 qed.
     84
     85lemma bevals_of_pointer_is_address :
     86  ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)).
     87* #b * #o whd in ⊢ (?%); whd
     88%{b} [ elim (block_region b) % ] %{(mk_part 0 ?)} [ %2 %1 ] %{(mk_part 1 ?)} [ %1 ]
     89@(vsplit_elim … 8 8 o) #o1 #o0 #EQ >EQ -o
     90%{[[o0]]} %{[[o1;o0]]}
     91% [2: change with (bool_to_Prop (if eq_bv ??? then ? else ?))
     92      >eq_bv_refl % ]
     93%%[2: normalize nodelta @vsplit_elim #pre >(Vector_O … pre) #post #EQ
     94      normalize in EQ; <EQ -pre -post
     95      whd in match (rvsplit ????);
     96      <(vsplit_prod … (refl …)) normalize nodelta
     97  | % [2: % ]
     98  ]
     99whd in match (rvsplit ????);
     100try <(vector_append_empty … o0) in ⊢ (??%?);
     101<(vsplit_prod … (refl …)) normalize nodelta %
     102qed.
     103
     104lemma is_address_to_pointer : ∀a.is_address a → ∃p.pointer_of_address a = return p.
     105* #a0 #a1 ** #bl #bl_prf ** #p0 #p0_prf ** #p1 #p1_prf * #o0' * #o1o0 ****
     106#EQ1 #EQ2 #EQ3 #EQ4 destruct
     107@(Vector_pair_elim … o1o0) #o1 #o0 #EQ >EQ -o1o0
     108@(Vector_singl_elim … o0') #o0'' #EQ >EQ -o0'
     109whd in ⊢ (?%→?);
     110@eq_bv_elim #EQ * >EQ -o0''
     111whd in match (pointer_of_address ?);
     112>eq_block_b_b >(eqb_n_n 1)
     113>vsuffix_vflatten
     114[2: change with (bool_to_Prop (vsuffix ????? ([[?]]@@[[?]])))
     115  @vsuffix_true change with (bool_to_Prop (if eq_bv ? o0 o0 then ? else ?))
     116  >eq_bv_refl % ]
     117normalize nodelta
     118whd in ⊢ (??(λ_.??%?));
     119% [2: % |]
     120qed.
     121
    91122(* For full 8051 memory spaces
    92123definition pointer_compat' ≝ λb,r.
     
    117148qed.
    118149*)
    119 lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     150(*lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
    120151** #a0 #a1 ***** #z #o
    121152#Hr
     
    130161@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
    131162#_ #_ normalize %
    132 qed.
     163qed.*)
    133164   
    134165definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
     
    136167example address_of_pointer_OK_to_safe :
    137168  ∀p,a.address_of_pointer p = OK … a → is_address a.
    138 #p
    139 lapply (refl … p)
    140 generalize in match p in ⊢ (???%→%); *(***)
    141 whd in match (address_of_pointer ?);
    142 #b (*#H*) #o #EQp * #a0 #a1
    143 normalize #EQ destruct(EQ)
    144 %{p} >EQp [ cases (block_region b) // | % [2: % [2: % [ % [ % ] ] ] ] %
    145 (*
    146 %{p} >EQp [1,3: %]
    147 % [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
    148 *)
    149 qed.
    150 
    151 definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
     169#p #a whd in match address_of_pointer; normalize nodelta
     170#EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     171//
     172qed.
     173
     174(*definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
    152175  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
    153176
     
    177200% [2: % [2: % [ % [ % ]] % |]|]
    178201qed.*)
     202*)
    179203
    180204(* Paolo: why only code pointers and not XRAM too? *)
    181 definition addr_add: address → nat → res address ≝
     205(*definition addr_add: address → nat → res address ≝
    182206 λaddr,n.
    183207  do ptr ← code_pointer_of_address addr ;
     
    206230normalize cases ptr #p #E @E
    207231qed.
     232*)
  • src/joint/Joint.ma

    r1601 r2286  
     1include "common/BackEndOps.ma".
     2include "common/CostLabel.ma".
     3include "common/Registers.ma".
    14include "ASM/I8051.ma".
    2 include "common/CostLabel.ma".
    3 include "common/AST.ma".
    4 include "common/Registers.ma".
    55include "common/Graphs.ma".
    6 
    7 record params__: Type[1] ≝
    8  { acc_a_reg: Type[0]
    9  ; acc_b_reg: Type[0]
    10  ; dpl_reg: Type[0]
    11  ; dph_reg: Type[0]
    12  ; pair_reg: Type[0]
    13  ; generic_reg: Type[0]
    14  ; call_args: Type[0]
    15  ; call_dest: Type[0]
    16  
    17  ; extend_statements: Type[0]
     6include "utilities/lists.ma".
     7include "common/LabelledObjects.ma".
     8include "ASM/Util.ma".
     9include "common/StructuredTraces.ma".
     10
     11(* Here is the structure of parameter records (downward edges are coercions,
     12   the ↓ edges are the only explicitly defined coercions). lin_params and
     13   graph_params are simple wrappers of unserialized_params, and the coercions
     14   from them to params instantiate the missing bits with values for linarized
     15   programs and graph programs respectively.
     16
     17        lin_params      graph_params
     18              |   \_____ /____   |
     19              |         /     \  |
     20              |        /      ↓  ↓
     21              |       |      params
     22              |       |        |
     23              |       |   stmt_params
     24              |       |    /   
     25          unserialized_params             
     26
     27unserialized_params : things unrelated to being in graph or linear form
     28stmt_params : adds successor type needed to define statements
     29params : adds type of code and related properties *)
     30
     31inductive possible_flows : Type[0] ≝
     32| Labels : list label → possible_flows
     33| Call : possible_flows.
     34
     35inductive argument (T : Type[0]) : Type[0] ≝
     36| Reg : T → argument T
     37| Imm : beval → argument T.
     38
     39definition psd_argument ≝ argument register.
     40 
     41definition psd_argument_from_reg : register → psd_argument ≝ Reg register.
     42coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
     43  on _r : register to psd_argument.
     44
     45definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
     46coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
     47  on _b : beval to psd_argument.
     48
     49definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     50coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     51  on _b : Byte to psd_argument.
     52
     53definition hdw_argument ≝ argument Register.
     54 
     55definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register.
     56coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
     57  on _r : Register to hdw_argument.
     58
     59definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
     60coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
     61  on _b : beval to hdw_argument.
     62
     63definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     64coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     65  on _b : Byte to hdw_argument.
     66
     67definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8.
     68definition zero_byte : Byte ≝ bv_zero 8.
     69
     70record unserialized_params : Type[1] ≝
     71 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
     72 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     73 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
     74 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
     75 ; dpl_reg: Type[0]   (* low address registers *)
     76 ; dph_reg: Type[0]   (* high address registers *)
     77 ; dpl_arg: Type[0]   (* low address registers *)
     78 ; dph_arg: Type[0]   (* high address registers *)
     79 ; snd_arg : Type[0]  (* second argument of binary op *)
     80 ; pair_move: Type[0] (* argument of move instructions *)
     81 ; call_args: Type[0] (* arguments of function calls *)
     82 ; call_dest: Type[0] (* possible destination of function computation *)
     83 (* other instructions not fitting in the general framework *)
     84 ; ext_seq : Type[0]
     85(* ; ext_branch : Type[0]
     86 ; ext_branch_labels : ext_branch → list label*)
     87 ; ext_call : Type[0]
     88 ; ext_tailcall : Type[0]
     89 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
     90 ; paramsT : Type[0]
     91 ; localsT: Type[0]
    1892 }.
    1993
    20 record params_: Type[1] ≝
    21  { pars__:> params__
    22  ; succ: Type[0]
     94inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
     95  | COMMENT: String → joint_seq p globals
     96  | COST_LABEL: costlabel → joint_seq p globals
     97  | MOVE: pair_move p → joint_seq p globals
     98  | POP: acc_a_reg p → joint_seq p globals
     99  | PUSH: acc_a_arg p → joint_seq p globals
     100  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     101  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
     102  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     103  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
     104  (* int done with generic move *)
     105(*| INT: generic_reg p → Byte → joint_seq p globals *)
     106  | CLEAR_CARRY: joint_seq p globals
     107  | SET_CARRY: joint_seq p globals
     108  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
     109  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
     110  | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
     111  | extension_seq : ext_seq p → joint_seq p globals
     112  | extension_call : ext_call p → joint_seq p globals.
     113
     114axiom EmptyString : String.
     115definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
     116
     117notation "r ← a1 .op. a2" with precedence 60 for
     118  @{'op2 $op $r $a1 $a2}.
     119notation "r ← . op . a" with precedence 60 for
     120  @{'op1 $op $r $a}.
     121notation "r ← a" with precedence 60 for
     122  @{'mov $r $a}. (* to be set in individual languages *)
     123notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
     124  @{'opaccs $op $r $s $a1 $a2}.
     125
     126interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
     127interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
     128interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
     129
     130coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     131  extension_seq on _s : ext_seq ? to joint_seq ??.
     132coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
     133  extension_call on _s : ext_call ? to joint_seq ??.
     134 
     135(* inductive joint_branch (p : step_params) : Type[0] ≝
     136  | COND: acc_a_reg p → label → joint_branch p
     137  | extension_branch : ext_branch p → joint_branch p.*)
     138
     139(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     140  extension_branch on _s : ext_branch ? to joint_branch ?.*)
     141
     142inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
     143  | step_seq : joint_seq p globals → joint_step p globals
     144  | COND: acc_a_reg p → label → joint_step p globals.
     145
     146coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
     147  step_seq on _s : joint_seq ?? to joint_step ??.
     148
     149definition step_flows ≝ λp,globals.λs : joint_step p globals.
     150  match s with
     151  [ step_seq s ⇒
     152    match s with
     153    [ CALL_ID _ _ _ ⇒ Call
     154    | extension_call _ ⇒ Call
     155    | _ ⇒ Labels … [ ]
     156    ]
     157  | COND _ l ⇒ Labels … [l]
     158  ].
     159
     160definition step_labels ≝
     161  λp, globals.λs : joint_step p globals.
     162    match step_flows … s with
     163    [ Labels lbls ⇒ lbls
     164    | Call ⇒ [ ]
     165    ].
     166
     167definition step_forall_labels : ∀p.∀globals.
     168    (label → Prop) → joint_step p globals → Prop ≝
     169λp,g,P,inst. All … P (step_labels … inst).
     170
     171definition step_classifier :
     172  ∀p.∀globals.
     173    joint_step p globals → status_class ≝ λp,g,s.
     174  match s with
     175  [ step_seq s ⇒
     176    match s with
     177    [ CALL_ID _ _ _ ⇒ cl_call
     178    | extension_call _ ⇒ cl_call
     179    | _ ⇒ cl_other
     180    ]
     181  | COND _ _ ⇒ cl_jump
     182  ].
     183
     184record stmt_params : Type[1] ≝
     185  { uns_pars :> unserialized_params
     186  ; succ : Type[0]
     187  ; succ_label : succ → option label
     188  }.
     189
     190inductive joint_fin_step (p: unserialized_params): Type[0] ≝
     191  | GOTO: label → joint_fin_step p
     192  | RETURN: joint_fin_step p
     193  | tailcall : ext_tailcall p → joint_fin_step p.
     194
     195definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     196  match s with
     197  [ GOTO l ⇒ Labels … [l]
     198  | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
     199  | _ ⇒ Labels … [ ]
     200  ].
     201
     202definition fin_step_labels ≝
     203  λp.λs : joint_fin_step p.
     204    match fin_step_flows … s with
     205    [ Labels lbls ⇒ lbls
     206    | Call ⇒ [ ]
     207    ].
     208
     209definition fin_step_classifier :
     210  ∀p : stmt_params.
     211    joint_fin_step p → status_class
     212  ≝ λp,s.
     213  match s with
     214  [ GOTO _ ⇒ cl_other
     215  | _ ⇒ cl_return
     216  ].
     217
     218inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
     219  | sequential: joint_step p globals → succ p → joint_statement p globals
     220  | final: joint_fin_step p → joint_statement p globals.
     221
     222definition stmt_classifier :
     223  ∀p : stmt_params.∀globals.
     224    joint_statement p globals → status_class
     225  ≝ λp,g,s.
     226  match s with
     227  [ sequential stp _ ⇒ step_classifier p g stp
     228  | final stp ⇒ fin_step_classifier p stp
     229  ].
     230
     231coercion extension_fin_to_fin_step : ∀p : stmt_params.
     232  ∀s : ext_tailcall p.joint_fin_step p ≝
     233  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
     234
     235coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
     236  ∀s : joint_fin_step p.joint_statement p globals ≝
     237  final on _s : joint_fin_step ? to joint_statement ??.
     238
     239record params : Type[1] ≝
     240 { stmt_pars :> stmt_params
     241 ; codeT: list ident → Type[0]
     242 ; code_point : Type[0]
     243 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
     244 ; point_of_label : ∀globals.codeT globals → label → option code_point
     245 ; point_of_succ : code_point → succ stmt_pars → code_point
    23246 }.
     247
     248definition code_has_point ≝
     249  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
     250
     251(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
     252
     253definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
     254unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
     255
     256definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
     257  match pt with
     258  [ mk_Sig pt' pt_prf ⇒
     259    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
     260    [ Some x ⇒ λ_.x
     261    | None ⇒ λabs.⊥
     262    ] (refl …)
     263  ]. normalize in pt_prf;
     264    >abs in pt_prf; // qed.
     265
     266definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     267  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
     268
     269definition forall_statements_i :
     270  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
     271    codeT p globals → Prop  ≝
     272  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
     273
     274lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
     275#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     276
     277lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
     278  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
     279#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     280
     281definition code_has_label ≝ λp,globals,c,l.
     282  match point_of_label p globals c l with
     283  [ Some pt ⇒ code_has_point … c pt
     284  | None ⇒ false
     285  ].
     286
     287definition stmt_explicit_labels :
     288  ∀p,globals.
     289  joint_statement p globals → list label ≝
     290  λp,globals,stmt. match stmt with
     291  [ sequential c _ ⇒ step_labels … c
     292  | final c ⇒ fin_step_labels … c
     293  ].
     294
     295definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
     296  option label ≝
     297 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
     298 
     299definition stmt_labels : ∀p : stmt_params.∀globals.
     300    joint_statement p globals → list label ≝
     301  λp,g,stmt.
     302  (match stmt_implicit_label … stmt with
     303     [ Some l ⇒ [l]
     304     | None ⇒ [ ]
     305     ]) @ stmt_explicit_labels … stmt.
     306
     307definition stmt_forall_labels ≝
     308  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
     309  All … P (stmt_labels … s).
     310
     311lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
     312  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
     313#p#globals#P #s
     314whd in ⊢ (% → ?);
     315whd in ⊢ (???% → ?);
     316elim (stmt_implicit_label ???) [2: #next * #_] //
     317qed.
     318
     319lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
     320  stmt_forall_labels … P s →
     321    opt_All … P (stmt_implicit_label … s).
     322#p#globals#P#s
     323whd in ⊢ (% → ?);
     324whd in ⊢ (???% → ?);
     325elim (stmt_implicit_label ???)
     326[ //
     327| #next * #Pnext #_ @Pnext
     328]
     329qed.
     330
     331definition code_forall_labels ≝
     332  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
     333
     334lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
     335  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
     336  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
     337
     338record lin_params : Type[1] ≝
     339  { l_u_pars : unserialized_params }.
     340 
     341lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     342#tag #A #lbl #l elim l [*]
     343** [2: #id] #a #tl #IH
     344[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
     345  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
     346  @eq_identifier_elim #Heq normalize nodelta
     347  [ #_ normalize / by /]
     348| whd in ⊢ (?%→?%?);
     349]
     350#H >(index_of_label_from_internal … H)
     351@le_S_S @(IH H)
     352qed.
     353
     354(* mv *)
     355lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
     356#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
     357#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
     358qed.
     359
     360lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
     361#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
     362#n' #H @le_S_S @(IH … H)
     363qed.
     364
     365lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
     366#A #l elim l
     367[ #n #ABS @⊥ /2 by absurd/
     368| #hd #tl #IH * normalize //
     369]
     370qed.
     371
     372definition lin_params_to_params ≝
     373  λlp : lin_params.
     374     mk_params
     375      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
     376    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
     377    (* code_point ≝ *)ℕ
     378    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
     379    (* point_of_label ≝ *)(λglobals,c,lbl.
     380      If occurs_exactly_once ?? lbl c then with prf do
     381        return index_of_label ?? lbl c
     382      else
     383        None ?)
     384    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
     385
     386coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     387  on _lp : lin_params to params.
     388 
     389lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     390  ∀pt.code_has_point … code pt = leb (S pt) (|code|).
     391#lp #globals #code elim code
     392[ #pt %
     393| #hd #tl #IH * [%]
     394  #n @IH
     395]qed.
     396
     397lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     398  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
     399#lp #globals #code #lbl
     400whd in match (code_has_label ????);
     401whd in match (point_of_label ????);
     402elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
     403#Heq >Heq normalize nodelta
     404[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
     405  #ABS elim(absurd ?? ABS) -ABS
     406  @index_of_label_length assumption ]] %
     407qed.
     408
     409record graph_params : Type[1] ≝
     410  { g_u_pars : unserialized_params }.
    24411
    25412(* One common instantiation of params via Graphs of joint_statements
    26413   (all languages but LIN) *)
    27 definition graph_params_ : params__ → params_ ≝
    28  λpars__. mk_params_ pars__ label.
    29 
    30 inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
    31   | COMMENT: String → joint_instruction p globals
    32   | COST_LABEL: costlabel → joint_instruction p globals
    33   | INT: generic_reg p → Byte → joint_instruction p globals
    34   | MOVE: pair_reg p → joint_instruction p globals
    35   | POP: acc_a_reg p → joint_instruction p globals
    36   | PUSH: acc_a_reg p → joint_instruction p globals
    37   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    38   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
    39   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    40   | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
    41   | CLEAR_CARRY: joint_instruction p globals
    42   | SET_CARRY: joint_instruction p globals
    43   | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
    44   | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    45   | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    46   | COND: acc_a_reg p → label → joint_instruction p globals
    47   | extension: extend_statements p → joint_instruction p globals.
    48 
    49 inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    50   | sequential: joint_instruction p globals → succ p → joint_statement p globals
    51   | GOTO: label → joint_statement p globals
    52   | RETURN: joint_statement p globals.
    53 
    54 record params0: Type[1] ≝
    55  { pars__' :> params__
    56  ; resultT: Type[0]
    57  ; paramsT: Type[0]
    58  }.
    59 
    60 record params1 : Type[1] ≝
    61  { pars0 :> params0
    62  ; localsT: Type[0]
    63  }.
    64 
    65 record params (globals: list ident): Type[1] ≝
    66  { succ_ : Type[0]
    67  ; pars1 :> params1
    68  ; codeT: Type[0]
    69  ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
    70  }.
    71  
    72 definition params__of_params: ∀globals. params globals → params_ ≝
    73  λglobals,pars. mk_params_ pars (succ_ … pars).
    74 coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
    75  on _p: params ? to params_.
    76 
    77 include alias "common/Graphs.ma". (* To pick the right lookup *)
    78 
    79 (* One common instantiation of params via Graphs of joint_statements
    80    (all languages but LIN) *)
    81 definition graph_params: params1 → ∀globals: list ident. params globals ≝
    82  λpars1,globals.
    83   mk_params globals label pars1
    84    (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
    85 
    86 
    87 (* CSC: special case where localsT is a list of register (RTL and ERTL) *)
    88 definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
    89 definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
    90 
    91 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
     414definition graph_params_to_params ≝
     415  λgp : graph_params.
     416     mk_params
     417      (mk_stmt_params (g_u_pars gp) label (Some ?))
     418    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
     419    (* code_point ≝ *)label
     420    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
     421    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
     422    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
     423
     424coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
     425on _gp : graph_params to params.
     426
     427lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     428  ∀pt.code_has_point … code pt = (pt ∈ code). // qed.
     429
     430lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     431  ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed.
     432
     433definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
     434  λs : joint_statement p globals.
     435  match s with
     436  [ sequential _ n ⇒ P n
     437  | _ ⇒ True
     438  ].
     439
     440definition statement_closed : ∀globals.∀p : params.
     441  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
     442λglobals,p,code,pt,s.
     443  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
     444  stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s.
     445
     446definition code_closed : ∀p : params.∀globals.
     447  codeT p globals → Prop ≝ λp,globals,code.
     448    forall_statements_i … (statement_closed … code) code.
     449
     450record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    92451{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    93452  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     453  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
     454     following, right? *)
    94455(*  joint_if_sig: signature;  -- dropped in front end *)
    95   joint_if_result   : resultT p;
     456  joint_if_result   : call_dest p;
    96457  joint_if_params   : paramsT p;
    97   joint_if_locals   : localsT p;
     458  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    98459(*CSC: XXXXX stacksize unused for LTL-...*)
    99460  joint_if_stacksize: nat;
    100   joint_if_code     : codeT … p;
    101 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    102   joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
    103 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    104   joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
     461  joint_if_code     : codeT p globals ;
     462  joint_if_entry : point_in_code … joint_if_code ;
     463  joint_if_exit : point_in_code … joint_if_code
    105464}.
    106465
    107 (* Currified form *)
    108 definition set_joint_if_exit ≝
    109   λglobals,pars.
    110   λexit: label.
    111   λp:joint_internal_function globals pars.
    112   λprf: lookup … (joint_if_code … p) exit ≠ None ?.
    113    mk_joint_internal_function globals pars
    114     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    115     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    116     (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
     466definition joint_closed_internal_function ≝
     467  λp,globals.
     468    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    117469
    118470definition set_joint_code ≝
    119471  λglobals: list ident.
    120   λpars: params globals.
    121   λint_fun: joint_internal_function globals pars.
    122   λgraph: codeT … pars.
     472  λpars: params.
     473  λint_fun: joint_internal_function pars globals.
     474  λgraph: codeT pars globals.
    123475  λentry.
    124476  λexit.
    125     mk_joint_internal_function globals pars
     477    mk_joint_internal_function pars globals
    126478      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    127479      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
     
    129481
    130482definition set_joint_if_graph ≝
    131   λglobals,pars.
     483  λglobals.λpars : graph_params.
    132484  λgraph.
    133   λp:joint_internal_function globals pars.
    134   λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    135   λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
    136     set_joint_code globals pars p graph
    137       (mk_Sig … (joint_if_entry … p) entry_prf) (mk_Sig … (joint_if_exit … p) exit_prf).
     485  λp:joint_internal_function pars globals.
     486  λentry_prf.
     487  λexit_prf.
     488    set_joint_code globals pars p
     489      graph
     490      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
     491      (mk_Sig … (joint_if_exit ?? p) exit_prf).
    138492
    139493definition set_luniverse ≝
     
    154508    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    155509    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    156 
     510   
    157511(* Specialized for graph_params *)
    158512definition add_graph ≝
    159   λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
    160    let code ≝ add … (joint_if_code ?? p) l stmt in
    161     mk_joint_internal_function … (graph_params … globals)
     513  λg_pars : graph_params.λglobals.λl:label.λstmt.
     514    λp:joint_internal_function g_pars globals.
     515   let code ≝ add … (joint_if_code … p) l stmt in
     516    mk_joint_internal_function …
    162517     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    163518     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    164      code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
    165   normalize nodelta;
    166   [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
    167   #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
    168 qed.
     519     code
     520     (pi1 … (joint_if_entry … p))
     521     (pi1 … (joint_if_exit … p)).
     522>graph_code_has_point whd in match code; >mem_set_add
     523@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     524#x #H <graph_code_has_point @H
     525qed.
    169526
    170527definition set_locals ≝
    171   λglobals,pars.
    172   λp : joint_internal_function globals pars.
     528  λpars,globals.
     529  λp : joint_internal_function pars globals.
    173530  λlocals.
    174    mk_joint_internal_function globals pars
     531   mk_joint_internal_function pars globals
    175532    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    176533    (joint_if_params … p) locals (joint_if_stacksize … p)
     
    180537
    181538definition joint_program ≝
    182  λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
     539 λp:params. program (joint_function p) nat.
  • src/joint/SemanticUtils.ma

    r2176 r2286  
    11include "joint/semantics.ma".
    22include alias "common/Identifiers.ma".
     3include "utilities/hide.ma".
     4include "ASM/BitVectorTrie.ma".
     5
     6record hw_register_env : Type[0] ≝
     7  { reg_env : BitVectorTrie beval 6
     8  ; carry_bit : bebit
     9  ; other_bit : bebit
     10  }.
     11
     12definition empty_hw_register_env: hw_register_env ≝
     13  mk_hw_register_env (Stub …) BBundef BBundef.
     14
     15include alias "ASM/BitVectorTrie.ma".
     16
     17definition hwreg_retrieve: hw_register_env → Register → beval ≝
     18 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
     19
     20definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
     21 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
     22  (carry_bit env) (other_bit env).
     23
     24definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
     25λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
     26
     27definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
     28λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
     29
    330
    431(*** Store/retrieve on pseudo-registers ***)
     32include alias "common/Identifiers.ma".
    533
    634axiom BadRegister : String.
     
    1341(*** Store/retrieve on hardware registers ***)
    1442
    15 definition init_hw_register_env: address → hw_register_env ≝
    16  λaddr.
    17   let 〈dpl,dph〉 ≝ addr in
     43definition init_hw_register_env: xpointer → hw_register_env ≝
     44 λsp.
     45  let 〈dpl,dph〉 ≝
     46    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
     47    [ OK p ⇒ λ_.p
     48    | _ ⇒ λprf.⊥
     49    ] (refl …) in
    1850  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    1951   hwreg_store RegisterDPL dpl env.
    20 
    21 (****************************************************************************)
    22 
    23 definition graph_pointer_of_label0:
    24  pointer → label → Σp:pointer. ptype p = Code ≝
    25  λoldpc,l.
    26   mk_pointer
    27    (mk_block Code (block_id (pblock oldpc))) (mk_offset (pos (word_of_identifier … l))).
    28 // qed.
    29 
    30 definition graph_pointer_of_label:
    31  ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
    32  λ_.λ_.λ_.λoldpc,l.
    33   OK ? (graph_pointer_of_label0 oldpc l).
    34 
    35 definition graph_label_of_pointer: pointer → res label ≝
    36  λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    37 
    38 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    39  But I can't use it directly because this one uses a concrete definition of
    40  pointer_of_label and it is used to istantiate the more_sem_params record
    41  where the abstract version is declared as a field. Is there a better way
    42  to organize the code? *)
    43 definition graph_succ_p: label → address → res address ≝
    44  λl,old.
    45   do ptr ← pointer_of_address old ;
    46   let newptr ≝ graph_pointer_of_label0 ptr l in
    47   address_of_pointer newptr.
    48 
    49 axiom BadProgramCounter: String.
    50 
    51 definition graph_fetch_function:
    52  ∀params1,sem_params,globals.
    53   genv … (graph_params params1 globals) →
    54    state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
    55  λparams1,sem_params,globals,ge,st.
    56   do p ← code_pointer_of_address (pc … st) ;
    57   let b ≝ pblock p in
    58   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    59   match def with
    60   [ Internal def' ⇒ OK … def'
    61   | External _ ⇒ Error … [MSG BadProgramCounter]].
    62 
    63 definition graph_fetch_statement:
    64  ∀params1,sem_params,globals.
    65   genv … (graph_params params1 globals) →
    66    state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
    67  λparams1,sem_params,globals,ge,st.
    68   do p ← code_pointer_of_address (pc … st) ;
    69   do f ← graph_fetch_function … ge st ;
    70   do l ← graph_label_of_pointer p;
    71   opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
     52@hide_prf
     53normalize in prf; destruct(prf)
     54qed.
     55
     56(******************************** GRAPHS **************************************)
     57
     58definition bitvector_from_pos :
     59  ∀n.Pos → BitVector n ≝
     60  λn,p.bitvector_of_Z n (Zpred (pos p)).
     61
     62definition pos_from_bitvector :
     63  ∀n.BitVector n → Pos ≝
     64  λn,v.
     65  match Zsucc (Z_of_unsigned_bitvector n v)
     66  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
     67  with
     68  [ OZ ⇒ λprf.⊥
     69  | pos x ⇒ λ_. x
     70  | neg x ⇒ λprf.⊥
     71  ] (refl …).
     72@hide_prf
     73elim v in prf;
     74[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
     75
     76lemma pos_pos_from_bitvector :
     77  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
     78#n #bv elim bv -n
     79[ %
     80| #n * #bv #IH [ % | @IH ]
     81]
     82qed.
     83
     84lemma bitvector_from_pos_from_bitvector :
     85  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
     86#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
     87>Zpred_Zsucc //
     88qed.
     89
     90lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
     91  (∀q,r.
     92    ppos m = natp_plus (natp_times q (ppos n)) r →
     93    natp_lt r n →
     94    P (〈q,r〉)) →
     95  P (divide m n).
     96#P #m #n #H
     97lapply (refl … (divide m n))
     98cases (divide ??) in ⊢ (???%→%);
     99#q #r #EQ elim (divide_ok … EQ) -EQ @H
     100qed.
     101
     102lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
     103  p < q → \snd (divide p q) = ppos p.
     104#p #q #H @divide_elim * [2: #quot ]
     105* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
     106@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
     107[ @(transitive_le … (quot*q)) ] /2 by /
     108qed.
     109
     110lemma pos_from_bitvector_from_pos :
     111  ∀n,p.
     112  p ≤ two_power_nat n →
     113  pos_from_bitvector n (bitvector_from_pos n p) = p.
     114#n #p #H
     115cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
     116[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
     117>pos_pos_from_bitvector
     118whd in match (bitvector_from_pos ??);
     119>Z_of_unsigned_bitvector_of_Z
     120cases p in H ⊢ %;
     121[ #_ %
     122|*: #p' #H
     123  whd in match (Zpred ?);
     124  whd in match (Z_two_power_nat ?);
     125  whd in ⊢ (??(?%)?);
     126  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
     127  whd
     128  <succ_pred_n try assumption % #ABS destruct(ABS)
     129]
     130qed.
     131
     132lemma pos_from_bitvector_max : ∀n,bv.
     133  pos_from_bitvector n bv ≤ two_power_nat n.
     134#n #bv
     135change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
     136>pos_pos_from_bitvector
     137@Zlt_to_Zle
     138@bv_Z_unsigned_max
     139qed.
     140
     141definition graph_offset_of_label : label → option offset ≝
     142  λl.let p ≝ word_of_identifier … l in
     143  if leb p (two_power_nat offset_size) then
     144    return mk_offset (bitvector_from_pos … p)
     145  else
     146    None ?.
     147
     148definition graph_label_of_offset: offset → label ≝
     149 λo.an_identifier ? (pos_from_bitvector ? (offv o)).
     150
     151definition make_sem_graph_params :
     152  ∀pars : graph_params.
     153  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
     154  sem_params ≝
     155  λpars,g_pars.
     156  mk_sem_params
     157    pars
     158    (mk_more_sem_params
     159      pars
     160      g_pars
     161      graph_offset_of_label
     162      graph_label_of_offset
     163      ??
     164    ).
     165whd in match graph_label_of_offset;
     166whd in match graph_offset_of_label;
     167whd in match word_of_identifier;
     168normalize nodelta * #x
     169@(leb_elim ? (two_power_nat ?)) normalize nodelta
     170[ #_ >bitvector_from_pos_from_bitvector %
     171| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
     172| #H whd >(pos_from_bitvector_from_pos … H) %
     173| #_ %
     174]
     175qed.
     176
     177(******************************** LINEAR **************************************)
     178
     179definition lin_offset_of_nat : ℕ → option offset ≝
     180  λn.
     181  if leb (S n) (2^offset_size) then
     182    return mk_offset (bitvector_of_nat ? n)
     183  else
     184    None ?.
     185
     186definition lin_nat_of_offset : offset → ℕ ≝
     187  λo.nat_of_bitvector ? (offv o).
     188
     189
     190definition make_sem_lin_params :
     191  ∀pars : lin_params.
     192  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
     193  sem_params ≝
     194  λpars,g_pars.
     195  mk_sem_params
     196    pars
     197    (mk_more_sem_params
     198      pars
     199      g_pars
     200      lin_offset_of_nat
     201      lin_nat_of_offset
     202      ??
     203    ).
     204[ * ] #x
     205whd in match lin_offset_of_nat;
     206whd in match lin_nat_of_offset;
     207normalize nodelta
     208@leb_elim normalize nodelta #H
     209[ >bitvector_of_nat_inverse_nat_of_bitvector %
     210| @⊥ cases H #H @H -H -H //
     211| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
     212| %
     213]
     214qed.
  • src/joint/Traces.ma

    r2186 r2286  
    1 include "joint/semantics_paolo.ma".
     1include "joint/semantics.ma".
    22
    33record evaluation_params : Type[1] ≝
     
    55 ; sparams:> sem_params
    66 ; exit: cpointer
    7  ; ev_genv: genv globals sparams
     7 ; ev_genv: genv sparams globals
    88 ; io_env : state sparams → ∀o:io_out.res (io_in o)
    99 } .
     
    5858   (* as_pc_of ≝ *) (pc …)
    5959   (* as_classifier ≝ *)
    60     (λs,cl.∃stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return stmt
     60    (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉
    6161     stmt_classifier … stmt = cl)
    6262   (* as_label_of_pc ≝ *)
    6363    (λpc.
    6464      match fetch_statement ? p … (ev_genv p) pc with
    65       [ OK stmt ⇒ cost_label_of_stmt … stmt
     65      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
    6666      | _ ⇒ None ?
    6767      ])
     
    6969    (λs1,s2.
    7070      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
    71       ∃stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return (sequential ?? stp nxt)
     71      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉
    7272      succ_pc p p (pc … s1) nxt = return pc … s2)
    7373   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
  • src/joint/TranslateUtils.ma

    r1995 r2286  
    11include "joint/Joint.ma".
    2 
    3 definition fresh_reg:
    4  ∀pars0,globals. joint_internal_function … (rtl_ertl_params pars0 globals) → (joint_internal_function … (rtl_ertl_params pars0 globals)) × register ≝
    5   λpars0,globals,def.
    6     let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    7      〈set_locals ?? (set_runiverse ?? def runiverse) (r::joint_if_locals ?? def), r〉.
    8 
    9 let rec fresh_regs (pars0:?) (globals: list ident) (def: joint_internal_function … (rtl_ertl_params pars0 globals)) (n: nat) on n ≝
    10   match n with
    11   [ O ⇒ 〈def, [ ]〉
     2include "joint/blocks.ma".
     3include "utilities/hide.ma".
     4
     5(* general type of functions generating fresh things *)
     6definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
     7
     8include alias "basics/lists/list.ma".
     9let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
     10  on n :
     11  freshT pars globals (Σl : list A. |l| = n) ≝
     12  match n  return λx.freshT … (Σl.|l| = x) with
     13  [ O ⇒ return «[ ], ?»
    1214  | S n' ⇒
    13     let 〈def', regs'〉 ≝ fresh_regs pars0 globals def n' in
    14     let 〈def', reg〉 ≝ fresh_reg … def' in
    15       〈def', reg :: regs'〉
    16   ].
    17  
    18 lemma fresh_regs_length:
    19  ∀pars0,globals.∀def: joint_internal_function … (rtl_ertl_params pars0 globals). ∀n: nat.
    20   |(\snd (fresh_regs … def n))| = n.
    21  #pars0 #globals #def #n elim n
    22   [ %
    23   | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    24     #def' #regs #EQ >EQ cases (fresh_reg ???)  normalize // ]
     15    ! regs' ← repeat_fresh … fresh n';
     16    ! reg ← fresh ;
     17    return «reg::regs',?»
     18  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
     19
     20definition fresh_label:
     21 ∀g_pars,globals.freshT globals g_pars label ≝
     22  λg_pars,globals,def.
     23    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     24     〈set_luniverse … def luniverse, r〉.
     25
     26(* insert into a graph a block of instructions *)
     27let rec adds_graph_list
     28  (g_pars: graph_params)
     29  (globals: list ident)
     30  (insts: list (joint_seq g_pars globals))
     31  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
     32  match insts with
     33  [ nil ⇒ return src
     34  | cons instr others ⇒
     35    ! mid ← fresh_label … ;
     36    ! def ← state_get … ;
     37    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
     38    adds_graph_list g_pars globals others mid
     39  ].
     40
     41definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     42  [ inl _ ⇒ true
     43  | inr _ ⇒ false
     44  ].
     45definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     46  [ inl _ ⇒ true
     47  | inr _ ⇒ false
     48  ].
     49
     50definition adds_graph :
     51  ∀g_pars : graph_params.
     52  ∀globals: list ident.
     53  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
     54       seq_block g_pars globals (joint_fin_step g_pars).
     55  label → if is_inl … b then label else unit →
     56  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
     57  λg_pars,globals,insts,src.
     58  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     59  [ inl b ⇒ λdst,def.
     60    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     61    add_graph … mid (sequential … (\snd b) dst) def
     62  | inr b ⇒ λdst,def.
     63    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     64    add_graph … mid (final … (\snd b)) def
     65  ].
     66
     67(* preserves first statement if a cost label (should be an invariant) *)
     68definition insert_prologue ≝
     69  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     70  λdef : joint_internal_function g_pars globals.
     71  let entry ≝ joint_if_entry … def in
     72  match stmt_at … entry
     73  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     74  with
     75  [ Some s ⇒ λ_.
     76    match s with
     77    [ sequential s' next ⇒
     78      match s' with
     79      [ step_seq s'' ⇒
     80        match s'' with
     81        [ COST_LABEL _ ⇒
     82          adds_graph ?? (inl … (s'' :: insts)) entry next def
     83        | _ ⇒
     84          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     85          add_graph … tmp s def'
     86        ]
     87      | _ ⇒
     88        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     89        add_graph … tmp s def'
     90      ]
     91    | _ ⇒
     92      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     93      add_graph … tmp s def'
     94    ]
     95  | None ⇒ Ⓧ
     96  ] (pi2 … entry).
     97
     98definition insert_epilogue ≝
     99  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     100  λdef : joint_internal_function g_pars globals.
     101  let exit ≝ joint_if_exit … def in
     102  match stmt_at … exit
     103  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     104  with
     105  [ Some s ⇒ λ_.
     106    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
     107    let def'' ≝ add_graph … tmp s def' in
     108    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
     109  | None ⇒ Ⓧ
     110  ] (pi2 … exit).
     111whd in match def''; >graph_code_has_point //
    25112qed.
    26113
    27 definition fresh_regs_strong:
    28  ∀pars0,globals. joint_internal_function … (rtl_ertl_params pars0 globals) →
    29   ∀n: nat. Σregs: (joint_internal_function … (rtl_ertl_params pars0 globals)) × (list register). |\snd regs| = n ≝
    30  λpars0,globals,def,n.fresh_regs pars0 globals def n. //
     114definition b_adds_graph :
     115  ∀g_pars: graph_params.
     116  ∀globals: list ident.
     117  (* fresh register creation *)
     118  freshT g_pars globals (localsT … g_pars) →
     119  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
     120       bind_seq_block g_pars globals (joint_fin_step g_pars).
     121  label → if is_inl … b then label else unit →
     122  joint_internal_function g_pars globals→
     123  joint_internal_function g_pars globals ≝
     124  λg_pars,globals,fresh_r,insts,src.
     125  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     126  [ inl b ⇒ λdst,def.
     127    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     128    adds_graph … (inl … stmts) src dst def
     129  | inr b ⇒ λdst,def.
     130    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     131    adds_graph … (inr … stmts) src dst def
     132  ].
     133
     134(* translation with inline fresh register allocation *)
     135definition b_graph_translate :
     136  ∀src_g_pars,dst_g_pars : graph_params.
     137  ∀globals: list ident.
     138  (* fresh register creation *)
     139  freshT dst_g_pars globals (localsT dst_g_pars) →
     140  (* initialized function definition with empty graph *)
     141  joint_internal_function dst_g_pars globals →
     142  (* functions dictating the translation *)
     143  (label → joint_step src_g_pars globals →
     144    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     145  (label → joint_fin_step src_g_pars →
     146    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
     147  (* source function *)
     148  joint_internal_function src_g_pars globals →
     149  (* destination function *)
     150  joint_internal_function dst_g_pars globals ≝
     151  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
     152  let f : label → joint_statement (src_g_pars : params) globals →
     153    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     154    λlbl,stmt,def.
     155    match stmt with
     156    [ sequential inst next ⇒
     157      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
     158    | final inst ⇒
     159      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
     160    ] in
     161  foldi … f (joint_if_code … def) empty.
     162
     163(* translation without register allocation *)
     164definition graph_translate :
     165  ∀src_g_pars,dst_g_pars : graph_params.
     166  ∀globals: list ident.
     167  (* initialized function definition with empty graph *)
     168  joint_internal_function dst_g_pars globals →
     169  (* functions dictating the translation *)
     170  (label → joint_step src_g_pars globals →
     171    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     172  (label → joint_fin_step src_g_pars →
     173    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
     174  (* source function *)
     175  joint_internal_function src_g_pars globals →
     176  (* destination function *)
     177  joint_internal_function dst_g_pars globals ≝
     178  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
     179  let f : label → joint_statement (src_g_pars : params) globals →
     180    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     181    λlbl,stmt,def.
     182    match stmt with
     183    [ sequential inst next ⇒
     184      adds_graph … (inl … (trans_step lbl inst)) lbl next def
     185    | final inst ⇒
     186      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
     187    ] in
     188  foldi … f (joint_if_code … def) empty.
     189
     190definition init_graph_if ≝
     191  λg_pars : graph_params.λglobals.
     192  λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
     193  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
     194  let graph ≝ add ? ? graph exit (RETURN …) in
     195  mk_joint_internal_function g_pars globals
     196    luniverse runiverse ret params locals stack_size
     197    graph entry exit.
     198>graph_code_has_point @map_mem_prop
     199[@graph_add_lookup] @graph_add
    31200qed.
    32201
    33 definition fresh_label:
    34  ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝
    35   λpars0,globals,def.
    36     let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
    37      〈r,set_luniverse … def luniverse〉.
    38 
     202
     203(*
    39204let rec add_translates
    40205  (pars1: params1) (globals: list ident)
     
    55220 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
    56221  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
     222  *)
  • src/joint/blocks.ma

    r2214 r2286  
    1 include "joint/Joint_paolo.ma".
     1include "joint/Joint.ma".
    22include "utilities/bindLists.ma".
    33
  • src/joint/linearise.ma

    r2214 r2286  
    1 include "joint/TranslateUtils_paolo.ma".
     1include "joint/TranslateUtils.ma".
    22include "utilities/hide.ma".
    33
  • src/joint/semantics.ma

    r2185 r2286  
    1 include "basics/lists/list.ma".
    21include "common/Globalenvs.ma".
    32include "common/IO.ma".
    4 include "common/SmallstepExec.ma".
     3(* include "common/SmallstepExec.ma". *)
    54include "joint/BEMem.ma".
    65include "joint/Joint.ma".
     
    1211   only the head is kept (or Undef if the list is empty) ??? *)
    1312
    14 record more_sem_params (p:params_): Type[1] ≝
     13(* Paolo: I'll put in this record the property about genv we need *)
     14record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
     15{ ge :> genv_t (fundef (F globals))
     16; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ?
     17}.
     18
     19definition genv ≝ λp.genv_gen (joint_internal_function p).
     20coercion genv_to_genv_t :
     21  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
     22  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
     23
     24definition cpointer ≝ Σp.ptype p = Code.
     25definition xpointer ≝ Σp.ptype p = XData.
     26unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
     27unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     28
     29record sem_state_params : Type[1] ≝
    1530 { framesT: Type[0]
    1631 ; empty_framesT: framesT
    17  ; regsT: Type[0]
    18  ; empty_regsT: address → regsT (* Stack pointer *)
    19  ; call_args_for_main: call_args p
    20  ; call_dest_for_main: call_dest p
    21 
    22  ; greg_store_: generic_reg p → beval → regsT → res regsT
    23  ; greg_retrieve_: regsT → generic_reg p → res beval
    24  ; acca_store_: acc_a_reg p → beval → regsT → res regsT
    25  ; acca_retrieve_: regsT → acc_a_reg p → res beval
    26  ; accb_store_: acc_b_reg p → beval → regsT → res regsT
    27  ; accb_retrieve_: regsT → acc_b_reg p → res beval
    28  ; dpl_store_: dpl_reg p → beval → regsT → res regsT
    29  ; dpl_retrieve_: regsT → dpl_reg p → res beval
    30  ; dph_store_: dph_reg p → beval → regsT → res regsT
    31  ; dph_retrieve_: regsT → dph_reg p → res beval
    32  ; pair_reg_move_: regsT → pair_reg p → res regsT
     32 ; regsT : Type[0]
     33 ; empty_regsT: xpointer → regsT (* Stack pointer *)
    3334 }.
    3435
    35 record sem_params: Type[1] ≝
    36  { spp :> params_
    37  ; more_sem_pars :> more_sem_params spp
    38  }.
    39 
    40 record state (p: sem_params): Type[0] ≝
    41  { st_frms: framesT ? p
    42  ; pc: address
    43  ; sp: pointer
    44  ; isp: pointer
    45  ; carry: beval
    46  ; regs: regsT ? p
     36record state (semp: sem_state_params): Type[0] ≝
     37 { st_frms: framesT semp
     38 ; sp: xpointer
     39 ; isp: xpointer
     40 ; carry: bebit
     41 ; regs: regsT semp
    4742 ; m: bemem
    4843 }.
    4944
    50 (*
    51 definition empty_state: ∀p. more_sem_params p → state p ≝
    52  mk_state … (empty_framesT …)
    53 *)
    54 
    55 definition genv ≝ λglobals.λp:params globals. genv_t (joint_function globals p).
    56 
    57 record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] ≝
    58  { more_sparams :> more_sem_params p
    59 
    60  (*CSC: XXXX succ_pc, pointer_of_label and fetch_statement all deal with fetching
    61    should we take 'em out in a different record to simplify the code? *)
    62  ; succ_pc: succ p → address → res address
    63  ; pointer_of_label: genv … p → pointer → label → res (Σp:pointer. ptype p = Code)
    64  ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    65 
    66  ; fetch_ra: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
    67  ; result_regs: genv globals p → state (mk_sem_params … more_sparams) → res (list (generic_reg p))
    68 
    69  ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    70    (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     45coercion sem_state_params_to_state nocomposites:
     46  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
     47
     48record state_pc (semp : sem_state_params) : Type[0] ≝
     49  { st_no_pc :> state semp
     50  ; pc : cpointer
     51  }.
     52
     53definition set_m: ∀p. bemem → state p → state p ≝
     54 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     55
     56definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
     57 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     58
     59definition set_sp: ∀p. ? → state p → state p ≝
     60 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
     61
     62definition set_isp: ∀p. ? → state p → state p ≝
     63 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     64
     65definition set_carry: ∀p. bebit → state p → state p ≝
     66 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     67
     68definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     69 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     70
     71definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
     72 λp,s,st. mk_state_pc … s (pc … st).
     73
     74definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
     75 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     76
     77axiom BadProgramCounter : String.
     78
     79definition function_of_block :
     80 ∀pars : params.
     81 ∀globals.
     82  genv pars globals →
     83  block →
     84  res (joint_internal_function pars globals) ≝
     85  λpars,globals,ge,b.
     86  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     87  match def with
     88  [ Internal def' ⇒ OK … def'
     89  | External _ ⇒ Error … [MSG BadProgramCounter]].
     90 
     91(* this can replace graph_fetch function and lin_fetch_function *)
     92definition fetch_function:
     93 ∀pars : params.
     94 ∀globals.
     95  genv pars globals →
     96  cpointer →
     97  res (joint_internal_function pars globals) ≝
     98 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
     99
     100inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     101  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     102  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
     103  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
     104
     105inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     106  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
     107  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
     108  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
     109  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     110
     111record more_sem_unserialized_params
     112  (uns_pars : unserialized_params)
     113  (F : list ident → Type[0]) : Type[1] ≝
     114  { st_pars :> sem_state_params (* automatic coercion has issues *)
     115  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     116  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     117  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
     118  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     119  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
     120  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
     121  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     122  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
     123  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
     124  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
     125  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
     126  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
     127  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
     128  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
     129  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     130
     131  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
     132  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
     133  ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
     134   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    71135     type of arguments. To be fixed using a dependent type *)
    72  ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    73  ; pop_frame: genv globals p → state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
    74 
    75  ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
    76  ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    77  }.
    78 
    79 record sem_params1 (globals: list ident): Type[1] ≝
    80  { p1:> params globals
    81  ; more_sparams1:> more_sem_params1 globals p1
    82  }.
    83 
    84 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    85  { more_sparams_1 :> more_sem_params1 … p
    86  ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams_1) → succ p → state (mk_sem_params … more_sparams_1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams_1)))
    87  }.
    88 
    89 record sem_params2 (globals: list ident): Type[1] ≝
    90  { p2:> params globals
    91  ; more_sparams2:> more_sem_params2 globals p2
    92  }.
    93 
    94 definition sem_params_of_sem_params1 ≝ λglobals. λsp1: sem_params1 globals. mk_sem_params sp1 sp1.
    95 coercion sem_params_of_sem_params1 : ∀globals. ∀_x:sem_params1 globals. sem_params
    96  ≝ sem_params_of_sem_params1 on _x: sem_params1 ? to sem_params.
    97 
    98 definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 … sp2 sp2.
    99 coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1 globals
    100  ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.
    101 
    102 definition set_m: ∀p. bemem → state p → state p ≝
    103  λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
    104 
    105 definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
    106  λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
    107 
    108 definition set_sp: ∀p. pointer → state p → state p ≝
    109  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    110 
    111 definition set_isp: ∀p. pointer → state p → state p ≝
    112  λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
    113 
    114 definition set_carry: ∀p. beval → state p → state p ≝
    115  λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
    116 
    117 definition set_pc: ∀p. address → state p → state p ≝
    118  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    119 
    120 definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
    121  λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    122 
    123 
    124 definition address_of_label: ∀globals. ∀p:sem_params1 globals. genv globals p → pointer → label → res address ≝
    125  λglobals,p,ge,ptr,l.
    126   do newptr ← pointer_of_label … p ge … ptr l ;
    127   OK … (address_of_code_pointer newptr).
    128 
    129 definition goto: ∀globals. ∀p:sem_params1 globals. genv globals p → label → state p → res (state p) ≝
    130  λglobals,p,ge,l,st.
    131   do oldpc ← pointer_of_address (pc … st) ;
    132   do newpc ← address_of_label … ge oldpc l ;
    133   OK … (set_pc … newpc st).
    134 
    135 definition next: ∀globals. ∀p:sem_params1 globals. succ … p → state p → res (state p) ≝
    136  λglobals,p,l,st.
    137   do l' ← succ_pc … p l (pc … st) ;
    138   OK … (set_pc … l' st).
    139 
    140 definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
    141  λp,dst,v,st.
    142   do regs  ← greg_store_ … dst v (regs … st);
    143   OK ? (set_regs … regs st).
    144 
    145 definition greg_retrieve: ∀p:sem_params. state p → generic_reg p → res beval ≝
    146  λp,st,dst.greg_retrieve_ … (regs … st) dst.
    147 
    148 definition acca_store: ∀p:sem_params. acc_a_reg p → beval → state p → res (state p) ≝
    149  λp,dst,v,st.
    150   do regs ← acca_store_ … dst v (regs … st);
    151   OK ? (set_regs … regs st).
    152 
    153 definition acca_retrieve: ∀p:sem_params. state p → acc_a_reg p → res beval ≝
    154  λp,st,dst.acca_retrieve_ … (regs … st) dst.
    155 
    156 definition accb_store: ∀p:sem_params. acc_b_reg p → beval → state p → res (state p) ≝
    157  λp,dst,v,st.
    158   do regs ← accb_store_ … dst v (regs … st);
    159   OK ? (set_regs … regs st).
    160 
    161 definition accb_retrieve: ∀p:sem_params. state p → acc_b_reg p → res beval ≝
    162  λp,st,dst.accb_retrieve_ … (regs … st) dst.
    163 
    164 definition dpl_store: ∀p:sem_params. dpl_reg p → beval → state p → res (state p) ≝
    165  λp,dst,v,st.
    166   do regs ← dpl_store_ … dst v (regs … st);
    167   OK ? (set_regs … regs st).
    168 
    169 definition dpl_retrieve: ∀p:sem_params. state p → dpl_reg p → res beval ≝
    170  λp,st,dst.dpl_retrieve_ … (regs … st) dst.
    171 
    172 definition dph_store: ∀p:sem_params. dph_reg p → beval → state p → res (state p) ≝
    173  λp,dst,v,st.
    174   do regs ← dph_store_ … dst v (regs … st);
    175   OK ? (set_regs … regs st).
    176 
    177 definition dph_retrieve: ∀p:sem_params. state p → dph_reg p → res beval ≝
    178  λp,st,dst.dph_retrieve_ … (regs … st) dst.
    179 
    180 definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
    181  λp,st,rs.
    182   do regs ← pair_reg_move_ … (regs … st) rs;
    183   OK … (set_regs … regs st).
    184 
    185 axiom FailedStore: String.
    186 
    187 definition push: ∀p. state p → beval → res (state p) ≝
    188  λp,st,v.
    189   let isp ≝ isp … st in
    190   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    191   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    192   OK … (set_m … m (set_sp … isp st)).
    193 
    194 definition pop: ∀p. state p → res (state p × beval) ≝
    195  λp,st.
    196   let isp ≝ isp ? st in
    197   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    198   let ist ≝ set_sp … isp st in
    199   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    200   OK ? 〈st,v〉.
    201 
    202 definition save_ra : ∀p. state p → address → res (state p) ≝
    203  λp,st,l.
    204   let 〈addrl,addrh〉 ≝ l in
    205   do st ← push … st addrl;
    206   push … st addrh.
    207 
    208 definition load_ra : ∀p.state p → res (state p × address) ≝
    209  λp,st.
    210   do 〈st,addrh〉 ← pop … st;
    211   do 〈st,addrl〉 ← pop … st;
    212   OK ? 〈st, 〈addrl,addrh〉〉.
    213 
    214 axiom MissingSymbol : String.
    215 axiom FailedLoad : String.
    216 axiom BadFunction : String.
     136  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
     137      state st_pars → res (state st_pars)
     138  ; fetch_external_args: external_function → state st_pars →
     139      res (list val)
     140  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
     141  ; call_args_for_main: call_args uns_pars
     142  ; call_dest_for_main: call_dest uns_pars
     143
     144  (* from now on, parameters that use the type of functions *)
     145  ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
     146  (* change of pc must be left to *_flow execution *)
     147  ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars →
     148      F globals → state st_pars → IO io_out io_in (state st_pars)
     149  ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
     150      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     151  ; eval_ext_call: ∀globals.genv_gen F globals →
     152      ext_call uns_pars → state st_pars →
     153      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
     154  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
     155  (* do something more in some op2 calculations (e.g. mark a register for correction
     156     with spilled_no in ERTL) *)
     157  ; post_op2 : ∀globals.genv_gen F globals →
     158    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
     159    state st_pars → state st_pars
     160  }.
     161
     162(*coercion msu_pars_to_ss_pars nocomposites :
     163∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
     164 ≝ st_pars
     165on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
     166
     167
     168definition helper_def_retrieve :
     169  ∀X : ? → ? → ? → Type[0].
     170  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     171  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     172    λX,f,up,F,p,st.f ?? p (regs … st).
     173
     174definition helper_def_store :
     175  ∀X : ? → ? → ? → Type[0].
     176  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     177  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     178  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
     179
     180definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     181definition acca_store ≝ helper_def_store ? acca_store_.
     182definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
     183definition accb_store ≝ helper_def_store ? accb_store_.
     184definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
     185definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
     186definition dpl_store ≝ helper_def_store ? dpl_store_.
     187definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
     188definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
     189definition dph_store ≝ helper_def_store ? dph_store_.
     190definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
     191definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
     192definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
     193definition pair_reg_move ≝
     194  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     195    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
     196    return set_regs ? r st.
     197
     198 
    217199axiom BadPointer : String.
    218200
     201(* this is preamble to all calls (including tail ones). The optional argument in
     202   input tells the function whether it has to save the frame for internal
     203   calls.
     204   the first element of the triple is the entry point of the function if
     205   it is an internal one, or false in case of an external one.
     206   The actual update of the pc is left to later, as it depends on
     207   serialization and on whether the call is a tail one. *)
    219208definition eval_call_block:
    220  ∀globals.∀p:sem_params1 globals. genv globals p → state p →
    221   block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    222  λglobals,p,ge,st,b,args,dest,ra.
    223   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b) : IO ???;
     209 ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     210  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
     211    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     212 λp,F,p',globals,ge,st,b,args,dest.
     213  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    224214    match fd with
    225     [ Internal fn ⇒
    226       ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    227       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    228       let l' ≝ joint_if_entry … fn in
    229       let st ≝ set_regs p regs st in
    230       let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) zero_offset in
    231       ! newpc ← address_of_label … ge pointer_in_fn l' ;
    232       let st ≝ set_pc … newpc st in
    233        return 〈 E0, st〉
     215    [ Internal fd ⇒
     216      return 〈Init ?? (block_id b) fd args dest, st〉
    234217    | External fn ⇒
    235       ! params ← fetch_external_args … fn st : IO ???;
     218      ! params ← fetch_external_args … p' fn st : IO ???;
    236219      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    237220      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    240223         fixed once we fully implement external functions. *)
    241224      let vs ≝ [mk_val ? evres] in
    242       ! st ← set_result … vs st;
    243       let st ≝ set_pc … ra st in
    244         return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    245      ].
    246 (*% qed.*)
    247 
    248 definition eval_call_id:
    249  ∀globals.∀p:sem_params1 globals. genv globals p → state p →
    250   ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    251  λglobals,p,ge,st,id,args,dest,ra.
    252   ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    253   eval_call_block … ge st b args dest ra.
    254 
    255 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    256  λglobals,p,ge,st.
    257   ! s ← fetch_statement … ge st : IO ???;
    258   match s return λ_. IO ??? with
    259     [ GOTO l ⇒
    260        ! st ← goto … p ge l st ;
    261        return 〈E0, st〉
    262     | sequential seq l ⇒
    263       match seq return λ_. IO ??? with
    264       [ extension c ⇒ exec_extended … p ge c l st
    265       | COST_LABEL cl ⇒
    266          ! st ← next … p l st ;
    267          return 〈Echarge cl, st〉
    268       | COMMENT c ⇒
    269          ! st ← next … p l st ;
    270          return 〈E0, st〉
    271       | INT dest v ⇒
    272          ! st ← greg_store p dest (BVByte v) st;
    273          ! st ← next … p l st ;
    274           return 〈E0, st〉
    275       | LOAD dst addrl addrh ⇒
    276         ! vaddrh ← dph_retrieve … st addrh;
    277         ! vaddrl ← dpl_retrieve … st addrl;
    278         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    279         ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    280         ! st ← acca_store p … dst v st;
    281         ! st ← next … p l st ;
    282           return 〈E0, st〉
    283       | STORE addrl addrh src ⇒
    284         ! vaddrh ← dph_retrieve … st addrh;
    285         ! vaddrl ← dpl_retrieve … st addrl;
    286         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    287         ! v ← acca_retrieve … st src;
    288         ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    289         let st ≝ set_m … m' st in
    290         ! st ← next … p l st ;
    291           return 〈E0, st〉
    292       | COND src ltrue ⇒
    293         ! v ← acca_retrieve … st src;
    294         ! b ← bool_of_beval v;
    295         if b then
    296          ! st ← goto … p ge ltrue st ;
    297          return 〈E0, st〉
    298         else
    299          ! st ← next … p l st ;
    300          return 〈E0, st〉
    301       | ADDRESS ident prf ldest hdest ⇒
    302         ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol … ge ident);
    303         ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset);
    304         ! st ← dpl_store p ldest laddr st;
    305         ! st ← dph_store p hdest haddr st;
    306         ! st ← next … p l st ;
    307           return 〈E0, st〉
    308       | OP1 op dacc_a sacc_a ⇒
    309         ! v ← acca_retrieve … st sacc_a;
    310         ! v ← Byte_of_val v;
    311           let v' ≝ BVByte (op1 eval op v) in
    312         ! st ← acca_store p dacc_a v' st;
    313         ! st ← next … p l st ;
    314           return 〈E0, st〉
    315       | OP2 op dacc_a sacc_a src ⇒
    316         ! v1 ← acca_retrieve … st sacc_a;
    317         ! v1 ← Byte_of_val v1;
    318         ! v2 ← greg_retrieve … st src;
    319         ! v2 ← Byte_of_val v2;
    320         ! carry ← bool_of_beval (carry … st);
    321           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    322           let v' ≝ BVByte v' in
    323           let carry ≝ beval_of_bool carry in
    324         ! st ← acca_store p dacc_a v' st;
    325           let st ≝ set_carry … carry st in
    326         ! st ← next … p l st ;
    327           return 〈E0, st〉
    328       | CLEAR_CARRY ⇒
    329         ! st ← next … p l (set_carry … BVfalse st) ;
    330          return 〈E0, st〉
    331       | SET_CARRY ⇒
    332         ! st ← next … p l (set_carry … BVtrue st) ;
    333          return 〈E0, st〉
    334       | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    335         ! v1 ← acca_retrieve … st sacc_a_reg;
    336         ! v1 ← Byte_of_val v1;
    337         ! v2 ← accb_retrieve … st sacc_b_reg;
    338         ! v2 ← Byte_of_val v2;
    339           let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    340           let v1' ≝ BVByte v1' in
    341           let v2' ≝ BVByte v2' in
    342         ! st ← acca_store p dacc_a_reg v1' st;
    343         ! st ← accb_store p dacc_b_reg v2' st;
    344         ! st ← next … p l st ;
    345           return 〈E0, st〉
    346       | POP dst ⇒
    347         ! 〈st,v〉 ← pop … st;
    348         ! st ← acca_store p dst v st;
    349         ! st ← next … p l st ;
    350           return 〈E0, st〉
    351       | PUSH src ⇒
    352         ! v ← acca_retrieve … st src;
    353         ! st ← push … st v;
    354         ! st ← next … p l st ;
    355           return 〈E0, st〉
    356       | MOVE dst_src ⇒
    357         ! st ← pair_reg_move … st dst_src ;
    358         ! st ← next … p l st ;
    359           return 〈E0, st〉
    360       | CALL_ID id args dest ⇒
    361         ! ra ← succ_pc … p l (pc … st) : IO ???;         
    362           eval_call_id … p ge st id args dest ra ]
    363     | RETURN ⇒
    364       ! 〈st,ra〉 ← fetch_ra … st;
    365       ! st ← pop_frame … ge st;
    366         return 〈E0,set_pc … ra st〉].
    367 (*cases addr //
    368 qed.*)
    369 
    370 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → state p → option int ≝
     225      ! st ← set_result … p' vs dest st : IO ???;
     226      return 〈Proceed ???, st〉
     227      ].
     228
     229axiom FailedStore: String.
     230
     231definition push: ∀p.state p → beval → res (state p) ≝
     232 λp,st,v.
     233  let isp' ≝ isp ? st in
     234  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
     235  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
     236  return set_m … m (set_isp … isp'' st).
     237  normalize elim (isp p st) #p #H @H
     238qed.
     239
     240definition pop: ∀p. state p → res ((state p ) × beval) ≝
     241 λp,st.
     242  let isp' ≝ isp ? st in
     243  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
     244  let ist ≝ set_isp … isp'' st in
     245  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
     246  OK ? 〈ist,v〉.
     247  normalize elim (isp p st) #p #H @H
     248qed.
     249
     250definition save_ra : ∀p. state p → cpointer → res (state p) ≝
     251 λp,st,l.
     252  ! 〈addrl,addrh〉 ← address_of_pointer l ; (* always succeeds *)
     253  ! st' ← push … st addrl;
     254  push … st' addrh.
     255
     256definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
     257 λp,st.
     258  do 〈st',addrh〉 ← pop … st;
     259  do 〈st'',addrl〉 ← pop … st';
     260  do pr ← pointer_of_address 〈addrh, addrl〉;
     261  match ptype pr return λx.ptype pr = x → res (? × cpointer) with
     262  [ Code ⇒ λprf.return 〈st'', «pr,prf»〉
     263  | _ ⇒ λ_.Error … [MSG BadPointer]
     264  ] (refl …).
     265
     266(* parameters that are defined by serialization *)
     267record more_sem_params (pp : params) : Type[1] ≝
     268  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
     269  ; offset_of_point : code_point pp → option offset (* can overflow *)
     270  ; point_of_offset : offset → code_point pp
     271  ; point_of_offset_of_point :
     272    ∀pt.opt_All ? (eq ? pt) (option_map ?? point_of_offset (offset_of_point pt))
     273  ; offset_of_point_of_offset :
     274    ∀o.offset_of_point (point_of_offset o) = Some ? o
     275  }.
     276
     277(*
     278coercion ms_pars_to_msu_pars nocomposites :
     279∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
     280 ≝ msu_pars
     281on _msp : more_sem_params ? to more_sem_unserialized_params ??.
     282
     283definition ss_pars_of_ms_pars ≝
     284  λp.λpp : more_sem_params p.
     285  st_pars … (msu_pars … pp).
     286coercion ms_pars_to_ss_pars nocomposites :
     287∀p : params.∀msp : more_sem_params p.sem_state_params ≝
     288ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
     289
     290axiom CodePointerOverflow : String.
     291
     292definition pointer_of_point : ∀p.more_sem_params p →
     293  cpointer→ code_point p → res cpointer ≝
     294  λp,msp,ptr,pt.
     295  ! o ← opt_to_res ? [MSG CodePointerOverflow] (offset_of_point ? msp pt) ;
     296  return «mk_pointer (pblock ptr) o, ?».
     297elim ptr #ptr' #EQ <EQ % qed.
     298
     299definition point_of_pointer :
     300  ∀p.more_sem_params p → cpointer → code_point p ≝
     301  λp,msp,ptr.point_of_offset p msp (poff ptr).
     302
     303lemma point_of_pointer_of_point :
     304  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     305  pointer_of_point p msp ptr1 pt = return ptr2 →
     306  point_of_pointer p msp ptr2 = pt.
     307#p #msp #ptr1 #ptr2 #pt normalize
     308lapply (point_of_offset_of_point p msp pt)
     309cases (offset_of_point ???) normalize
     310[ * #ABS destruct(ABS)
     311| #o #EQ1 #EQ2 destruct %
     312]
     313qed.
     314
     315lemma pointer_of_point_block :
     316  ∀p,msp,ptr1,ptr2,pt.
     317  pointer_of_point p msp ptr1 pt = return ptr2 →
     318  pblock ptr2 = pblock ptr1.
     319#p #msp #ptr1 #ptr2 #pt normalize
     320cases (offset_of_point ???) normalize
     321[ #ABS destruct(ABS)
     322| #o #EQ destruct(EQ) %
     323]
     324qed.
     325
     326lemma pointer_of_point_uses_block :
     327  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
     328#p #msp ** #b1 #o1 #EQ1
     329        ** #b2 #o2 #EQ2
     330#pt #EQ3 destruct normalize //
     331qed.
     332
     333lemma pointer_of_point_of_pointer :
     334  ∀p,msp.∀ptr1,ptr2 : cpointer.
     335    pblock ptr1 = pblock ptr2 →
     336    pointer_of_point p msp ptr1 (point_of_pointer p msp ptr2) = return ptr2.
     337#p #msp ** #b1 #o1 #EQ1
     338        ** #b2 #o2 #EQ2
     339#EQ3 destruct
     340normalize >offset_of_point_of_offset normalize %
     341qed.
     342
     343axiom ProgramCounterOutOfCode : String.
     344axiom PointNotFound : String.
     345axiom LabelNotFound : String.
     346
     347definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     348  genv p globals → cpointer →
     349  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
     350  λp,msp,globals,ge,ptr.
     351  let pt ≝ point_of_pointer ? msp ptr in
     352  ! fn ← fetch_function … ge ptr ;
     353  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
     354  return 〈fn, stmt〉.
     355 
     356definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     357  genv p globals → cpointer → label → res cpointer ≝
     358  λp,msp,globals,ge,ptr,lbl.
     359  ! fn ← fetch_function … ge ptr ;
     360  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     361            (point_of_label … (joint_if_code … fn) lbl) ;
     362  pointer_of_point p msp ptr pt.
     363
     364definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     365  cpointer → succ p → res cpointer ≝
     366  λp,msp,ptr,nxt.
     367  let curr ≝ point_of_pointer p msp ptr in
     368  pointer_of_point p msp ptr (point_of_succ p curr nxt).
     369
     370record sem_params : Type[1] ≝
     371  { spp :> params
     372  ; more_sem_pars :> more_sem_params spp
     373  }.
     374
     375(* definition msu_pars_of_s_pars :
     376∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
     377≝ λp : sem_params.
     378  msu_pars … (more_sem_pars p).
     379coercion s_pars_to_msu_pars nocomposites :
     380∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
     381msu_pars_of_s_pars
     382on p : sem_params to more_sem_unserialized_params ??.
     383
     384definition ss_pars_of_s_pars :
     385∀p : sem_params.sem_state_params
     386≝ λp : sem_params.
     387  st_pars … (msu_pars … (more_sem_pars p)).
     388coercion s_pars_to_ss_pars nocomposites :
     389∀p : sem_params.sem_state_params ≝
     390ss_pars_of_s_pars
     391on _p : sem_params to sem_state_params.
     392
     393definition ms_pars_of_s_pars :
     394∀p : sem_params.more_sem_params (spp p)
     395≝ more_sem_pars.
     396coercion s_pars_to_ms_pars nocomposites :
     397∀p : sem_params.more_sem_params (spp p) ≝
     398ms_pars_of_s_pars
     399on p : sem_params to more_sem_params ?.*)
     400
     401(* definition address_of_label: ∀globals. ∀p:sem_params.
     402  genv globals p → pointer → label → res address ≝
     403 λglobals,p,ge,ptr,l.
     404  do newptr ← pointer_of_label … p ? ge … ptr l ;
     405  OK … (address_of_code_pointer newptr). *)
     406
     407definition goto: ∀globals.∀p : sem_params.
     408  genv p globals → label → state p → cpointer → res (state_pc p) ≝
     409 λglobals,p,ge,l,st,b.
     410  ! newpc ← pointer_of_label ? p … ge b l ;
     411  return mk_state_pc ? st newpc.
     412
     413(*
     414definition empty_state: ∀p. more_sem_params p → state p ≝
     415 mk_state … (empty_framesT …)
     416*)
     417
     418definition next : ∀p : sem_params.succ p → state p → cpointer → res (state_pc p) ≝
     419 λp,l,st,pc.
     420 ! newpc ← succ_pc ? p … pc l ;
     421 return mk_state_pc … st newpc.
     422
     423axiom MissingSymbol : String.
     424axiom FailedLoad : String.
     425axiom BadFunction : String.
     426axiom SuccessorNotProvided : String.
     427
     428definition eval_seq_no_pc :
     429 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
     430  state p → ∀s:joint_seq p globals.
     431  IO io_out io_in (state p) ≝
     432 λp,globals,ge,curr_fn,st,seq.
     433 match seq return λx.IO ??? with
     434  [ extension_seq c ⇒
     435    eval_ext_seq … ge c curr_fn st
     436  | LOAD dst addrl addrh ⇒
     437    ! vaddrh ← dph_arg_retrieve … st addrh ;
     438    ! vaddrl ← dpl_arg_retrieve … st addrl;
     439    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     440    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     441    acca_store p … dst v st
     442 | STORE addrl addrh src ⇒
     443    ! vaddrh ← dph_arg_retrieve … st addrh;
     444    ! vaddrl ← dpl_arg_retrieve … st addrl;
     445    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     446    ! v ← acca_arg_retrieve … st src;
     447    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
     448    return set_m … m' st
     449  | ADDRESS id prf ldest hdest ⇒
     450    let addr ≝ opt_safe ? (find_symbol … ge id) ? in
     451    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
     452    ! st' ← dpl_store … ldest laddr st;
     453    dph_store … hdest haddr st'
     454  | OP1 op dacc_a sacc_a ⇒
     455    ! v ← acca_retrieve … st sacc_a;
     456    ! v' ← be_op1 op v ;
     457    acca_store … dacc_a v' st
     458  | OP2 op dacc_a sacc_a src ⇒
     459    ! v1 ← acca_arg_retrieve … st sacc_a;
     460    ! v2 ← snd_arg_retrieve … st src;
     461    ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ;
     462    ! st' ← acca_store … dacc_a v' st;
     463    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
     464  | CLEAR_CARRY ⇒
     465    return set_carry … (BBbit false) st
     466  | SET_CARRY ⇒
     467    return set_carry … (BBbit true) st
     468  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     469    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     470    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
     471    ! 〈v1',v2'〉 ← be_opaccs op v1 v2 ;
     472    ! st' ← acca_store … dacc_a_reg v1' st;
     473    accb_store … dacc_b_reg v2' st'
     474  | POP dst ⇒
     475    ! 〈st',v〉 ← pop p st;
     476    acca_store … p dst v st'
     477  | PUSH src ⇒
     478    ! v ← acca_arg_retrieve … st src;
     479    push … st v
     480  | MOVE dst_src ⇒
     481    pair_reg_move … st dst_src
     482  | CALL_ID id args dest ⇒
     483    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     484    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
     485    return st'
     486  | extension_call s ⇒
     487    !〈flow, st'〉 ← eval_ext_call … ge s st ;
     488    return st'
     489  | _ ⇒ return st
     490  ].
     491  @find_symbol_exists
     492  lapply prf
     493  elim globals [*]
     494  #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ]
     495  #G %2 @IH @G
     496  qed.
     497
     498definition eval_seq_pc :
     499 ∀p:sem_params.∀globals. genv p globals → state p →
     500  ∀s:joint_seq p globals.
     501  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
     502  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     503  [ CALL_ID id args dest ⇒
     504    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     505    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
     506    return flow
     507  | extension_call s ⇒
     508    !〈flow, st'〉 ← eval_ext_call … ge s st ;
     509    return flow
     510  | _ ⇒ return Proceed ???
     511  ].
     512
     513definition eval_step :
     514 ∀p:sem_params.∀globals. genv p globals →
     515  joint_internal_function p globals → state p →
     516  ∀s:joint_step p globals.
     517  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
     518  λp,globals,ge,curr_fn,st,s.
     519  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
     520  [ step_seq s ⇒
     521    ! flow ← eval_seq_pc ?? ge st s ;
     522    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
     523    return 〈flow,st'〉
     524  | COND src ltrue ⇒
     525    ! v ← acca_retrieve … st src;
     526    ! b ← bool_of_beval v;
     527    if b then
     528      return 〈Redirect ??? ltrue, st〉
     529    else
     530      return 〈Proceed ???, st〉
     531  ].
     532  %1 % qed.
     533
     534definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
     535  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
     536  IO io_out io_in (state p) ≝
     537 λp,globals,ge,curr_fn,st,s.
     538  match s return λx.IO ??? with
     539    [ tailcall c ⇒
     540      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
     541      return st'
     542    | _ ⇒ return st
     543    ].
     544
     545definition eval_fin_step_pc :
     546 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
     547  ∀s:joint_fin_step p.
     548  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
     549  λp,g,ge,curr_fn,st,s.
     550  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
     551  [ tailcall c ⇒
     552    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
     553    return flow 
     554  | GOTO l ⇒ return FRedirect … l
     555  | RETURN ⇒ return FEnd1 ??
     556  ]. %1 % qed.
     557
     558definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
     559  state p → Z → joint_internal_function p globals → call_args p →
     560  res (state_pc p) ≝
     561  λp,globals,ge,st,id,fn,args.
     562    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     563              args st ;
     564    let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
     565    let l' ≝ joint_if_entry … fn in
     566    let st' ≝ set_regs p regs st in
     567    let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in
     568    ! pc ← pointer_of_point ? p … pointer_in_fn l' ;
     569    return mk_state_pc ? st' pc. % qed.
     570
     571(* The pointer provided is the one to the *next* instruction. *)
     572definition eval_step_flow :
     573 ∀p:sem_params.∀globals.∀flows.genv p globals →
     574 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
     575 λp,globals,flows,ge,st,nxt,cmd.
     576 match cmd with
     577  [ Redirect _ l ⇒
     578    goto … ge l st nxt
     579  | Init id fn args dest ⇒
     580    ! st' ← save_frame … nxt dest st ;
     581    do_call ?? ge st' id fn args
     582  | Proceed _ ⇒
     583    return mk_state_pc ? st nxt
     584  ].
     585
     586definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
     587  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
     588  λp,globals,lbls,ge,st,curr,cmd.
     589  match cmd with
     590  [ FRedirect _ l ⇒ goto … ge l st curr
     591  | FTailInit id fn args ⇒
     592    do_call … ge st id fn args
     593  | _ ⇒
     594    ! 〈st',ra〉 ← fetch_ra … st ;
     595    ! fn ← fetch_function … ge curr ;
     596    ! st'' ← pop_frame … ge fn st';
     597    return mk_state_pc ? st'' ra
     598  ].
     599
     600definition eval_statement :
     601 ∀globals.∀p:sem_params.genv p globals →
     602  state_pc p → joint_internal_function p globals → joint_statement p globals →
     603    IO io_out io_in (state_pc p) ≝
     604 λglobals,p,ge,st,curr_fn,stmt.
     605 match stmt with
     606 [ sequential s nxt ⇒
     607   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
     608   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
     609   eval_step_flow … ge st' nxtptr flow
     610 | final s ⇒
     611   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
     612   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
     613   eval_fin_step_flow … ge st' (pc … st) flow
     614 ].
     615
     616definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
     617  state_pc p → IO io_out io_in (state_pc p) ≝
     618  λglobals,p,ge,st.
     619  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
     620  eval_statement … ge st fn s.
     621
     622(* Paolo: what if in an intermediate language main finishes with an external
     623  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
     624  not static... *)
     625definition is_final: ∀globals:list ident. ∀p: sem_params.
     626  genv p globals → cpointer → state_pc p → option int ≝
    371627 λglobals,p,ge,exit,st.res_to_opt ? (
    372   do s ← fetch_statement … ge st;
     628  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
    373629  match s with
    374    [ RETURN ⇒
    375       do 〈st,ra〉 ← fetch_ra … st;
    376       if eq_address ra exit then
    377        do regs ← result_regs … ge st ;
    378        do vals ← mmap … (λreg.greg_retrieve … st reg) regs ;
     630  [ final s' ⇒
     631    match s' with
     632    [ RETURN ⇒
     633      do 〈st',ra〉 ← fetch_ra … st;
     634      if eq_pointer ra exit then
     635       do vals ← read_result … ge (joint_if_result … fn) st' ;
    379636       Word_of_list_beval vals
    380637      else
    381        Error ? []
    382    | _ ⇒ Error ? []]).
    383 
     638       Error ? [ ]
     639   | _ ⇒ Error ? [ ]
     640   ]
     641 | _ ⇒ Error ? [ ]
     642 ]).
     643
     644(*
    384645record evaluation_parameters : Type[1] ≝
    385646 { globals: list ident
    386  ; sparams2: sem_params2 globals
    387  ; exit: address
    388  ; genv2: genv globals sparams2
     647 ; sparams:> sem_params
     648 ; exit: cpointer
     649 ; genv2: genv globals sparams
    389650 }.
    390651
     652(* Paolo: with structured traces, eval need not emit labels. However, this
     653  changes trans_system. For now, just putting a dummy thing for
     654  the transition. *)
    391655definition joint_exec: trans_system io_out io_in ≝
    392   mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
    393    (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G))
    394    (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
     656  mk_trans_system … evaluation_parameters (λG. state_pc G)
     657   (λG.is_final (globals G) G (genv2 G) (exit G))
     658   (λG,st.! 〈flag,st'〉 ← eval_state_flag (globals G) G (genv2 G) st ; return 〈E0, st'〉).
    395659
    396660definition make_global :
    397  ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
     661 ∀pars: sem_params.
    398662  joint_program pars → evaluation_parameters
    399663
    400  λpars,sparams.
     664 λpars.
    401665 (* Invariant: a -1 block is unused in common/Globalenvs *)
    402666 let b ≝ mk_block Code (-1) in
    403  let ptr ≝ mk_pointer b zero_offset in
    404  let addr ≝ address_of_code_pointer ptr in
    405   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
     667 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
     668  (λp. mk_evaluation_parameters
     669    (prog_var_names … p)
     670    (mk_sem_params … pars)
     671    ptr
     672    (globalenv_noinit … p)
     673  ).
    406674% qed.
    407675
    408676axiom ExternalMain: String.
     677
    409678definition make_initial_state :
    410  ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    411  ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
    412 λpars,sparams,p.
    413   let sem_globals ≝ make_global pars sparams p in
     679 ∀pars: sem_params.
     680 ∀p: joint_program … pars. res (state_pc pars) ≝
     681λpars,p.
     682  let sem_globals ≝ make_global pars p in
    414683  let ge ≝ genv2 sem_globals in
    415684  let m ≝ alloc_mem … p in
    416685  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    417686  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    418   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) zero_offset in
    419   let spp ≝ mk_pointer spb (offset_of_Z external_ram_size) in
    420   let ispp ≝ mk_pointer ispb (offset_of_Z 47) in
    421   do sp ← address_of_pointer spp ;
     687  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
     688  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
     689  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    422690  let main ≝ prog_main … p in
    423   let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
    424   let trace_state ≝
    425    eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
    426     (call_dest_for_main … (sparams …)) (exit sem_globals) in
    427   match trace_state with
    428   [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
    429   | Wrong msg ⇒ Error … msg
    430   | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    431   ].
    432 (*[3: % | cases ispb | cases spb] *; #r #off #E >E %
    433 qed.*)
     691  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
     692  (* use exit sem_globals as ra and call_dest_for_main as dest *)
     693  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
     694  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     695  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
     696  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
     697  match main_fd with
     698  [ Internal fn ⇒
     699    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
     700  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     701  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
     702qed.
    434703
    435704definition joint_fullexec :
    436  ∀pars:∀globals.params globals.
    437  ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    438  fullexec io_out io_in ≝
    439  λpars,sparams.
    440   mk_fullexec ??? joint_exec (make_global pars sparams) (make_initial_state pars sparams).
     705 ∀pars:sem_params.fullexec io_out io_in ≝
     706 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
     707*)
Note: See TracChangeset for help on using the changeset viewer.