Changeset 3165


Ignore:
Timestamp:
Apr 19, 2013, 11:46:59 AM (4 years ago)
Author:
campbell
Message:

A little bit of progress on Callstate case.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r3155 r3165  
    811811  (* Cminor env/mem *)
    812812  ∀cm_env, cm_m.
    813   (* fresh label generator for function *)
    814   ∀func_univ: universe SymbolTag.
    815   (* specify fblock *)
    816   find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef →
    817   find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef →
    818   ∀cl_fun_id, cm_fun_id.
     813  (* specify fblock; as a consequence of these and INV we can deduce that
     814     cm_fundef is the translation of cl_fundef *)
     815  ∀fun_id.
     816  find_funct_id clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? 〈cl_fundef,fun_id〉 →
     817  find_funct_id (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? 〈cm_fundef,fun_id〉 →
    819818  ∀tmpenv.
    820819  (*match cl_fundef with
     
    852851  All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
    853852  clight_cminor_rel cl_ge cm_ge INV
    854    (ClCallstate cl_fun_id cl_fundef cl_args_values cl_k cl_m)
    855    (CmCallstate cm_fun_id cm_fundef cm_args_values cm_m cm_st)
     853   (ClCallstate fun_id cl_fundef cl_args_values cl_k cl_m)
     854   (CmCallstate fun_id cm_fundef cm_args_values cm_m cm_st)
    856855(* --------------------------------------------------------------------------- *)
    857856(* special while state *)
     
    17401739qed.
    17411740
     1741(* TODO: move *)
     1742lemma extract_pair' : ∀A,B,C.  ∀u:A×B. ∀Q:A → B → C. ∀x.
     1743((let 〈a,b〉 ≝ u in Q a b) = x) →
     1744∃a,b. 〈a,b〉 = u ∧ Q a b = x.
     1745#A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed.
     1746
    17421747(*
    17431748lemma lset_inclusion_Exists :
     
    17831788   subtrace corresponding to a measurable Clight subtrace.
    17841789 *)
     1790(* WIP
     1791lemma clight_cminor_call :
     1792    ∀g,g'.
     1793    ∀INV:clight_cminor_inv g g'.
     1794    ∀s1,s1'.
     1795    clight_cminor_rel g g' INV s1 s1' →
     1796    Clight_classify s1 = cl_call →
     1797    ∀s2,tr2,s3,tr3.
     1798    step … (pcs_exec cl_pre) g s1 = Value … 〈tr2,s2〉 →   
     1799    step … (pcs_exec cl_pre) g s2 = Value … 〈tr3,s3〉 →   
     1800    Clight_labelled s2 →
     1801    after_n_steps 1 ?? (pcs_exec cm_pre) g' s1' (λs.cminor_normal s) (λtr2',s2'.
     1802      tr2 = tr2' ∧
     1803      bool_to_Prop (Cminor_labelled s2') ∧
     1804      ∃m.
     1805      after_n_steps m ?? (pcs_exec cm_pre) g' s2' (λs.cminor_normal s) (λtr3',s3'.
     1806        tr3 = tr3' ∧
     1807        clight_cminor_rel g g' INV s2 s2')
     1808    ).
     1809#Xg #Xg' #XINV #Xs1 #Xs1' *
     1810[ #g #g' #INV #cl_s #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #fInv #sInv #kInv #Erettyp #func_univ #Hfresh_globals #Hfresh_function #Htranslate_fn #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag #Htranslate_inv #Htranslate_s #Hlbls_inc #tmpenv #Htmpenv #CONT #Em #HtmpEm #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #Henv_below
     1811  #CL whd in CL:(??%?); destruct
     1812| #g #g' #INV #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #stmt_univ #tmpenv #Htmpenv #Em #HEm_tmp #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #CONT
     1813  #CL whd in CL:(??%?); destruct
     1814| #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #INJ #HEm_fn #cl_args #cm_args #Hargs
     1815  #CL #s2 #tr2 #s3 #tr3 #STEP1 #STEP2 #CS2
     1816 
     1817  (* Note that cm_fd is the translation of cl_fd *)
     1818  cases (trans_fn … INV … Hfind_cl)
     1819  #func_univ * #cm_fd' * #Hglobals_fresh * #Hfundef_fresh * #Htranslate
     1820  >Hfind_cm #E destruct
     1821 
     1822  (* Must be a CL_Internal function *)
     1823  cases cl_fd in Hfundef_fresh Htranslate Hfind_cl CONT STEP1;
     1824  [ #cl_f
     1825  | #ext #ext_argtys #ext_retty
     1826  ]
     1827  #Hfundef_fresh #Htranslate #Hfind_cl #CONT #STEP1
     1828  [2: cases (bindIO_inversion ??????? STEP1) -STEP1 #vs * #_ #STEP1
     1829      whd in STEP1:(??%%); destruct ]
     1830  -cl_fd
     1831
     1832  (* Invert Clight STEP1 *) 
     1833  cases (extract_pair' ?????? STEP1) -STEP1 #cl_env * #cl_m1 * #ALLOC #STEP1
     1834  cases (bindIO_inversion ??????? STEP1) -STEP1 #cl_m2 * #BIND #STEP1
     1835  whd in STEP1:(??%%); destruct
     1836*)
     1837
    17851838(*
    17861839lemma clight_cminor_call_return :
     
    23532406    [ 1,2: >addition_n_0 >mk_offset_offv_id
    23542407    | 3: ]
    2355     >(find_funct_to_find_funct_id ???? Hfind_funct_cm)
     2408    >Hfind_funct_cm
    23562409    whd in match (opt_to_res ???); normalize nodelta
    23572410    (* Again, isolate cases by type similarity *)
     
    28772930  #cl_ge #cm_ge #INV' #cl_k #cm_st #cl_fundef #cm_fundef
    28782931  #fblock #target_type #cl_env #cl_m #cm_env #cm_m
    2879   #func_univ #Hfind_cl #Hfind_cm
    2880   #cl_id #cm_id #tmpenv #Hcont_rel
     2932  #fn_id #Hfind_cl #Hfind_cm
     2933  #tmpenv #Hcont_rel
    28812934  #Em #Hinj #Hem_fn_id
    28822935  #cl_args_values #cm_args_values #Hall2
     
    29833036 
    29843037(* TODO: move to globalenvs *)
    2985 lemma find_funct_match:
    2986     ∀M:matching.∀initV,initW.
     3038(* The hypotheses are a little strong - we don't need to know that the size of
     3039   the initialisation data is the same. *)
     3040lemma find_funct_id_match:
     3041    ∀M:matching.
     3042    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    29873043    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    29883044    ∀MATCH:match_program … M p p'.
    2989     ∀v. ∀f: m_A M (prog_var_names … p).
    2990     find_funct … (globalenv … initV p) v = Some ? f
     3045    ∀v. ∀f: m_A M (prog_var_names … p). ∀id.
     3046    find_funct_id … (globalenv … initV p) v = Some ? 〈f,id〉
    29913047    ∃tf : m_B M (prog_var_names … p').
    2992     find_funct … (globalenv … initW p') v = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
     3048    find_funct_id … (globalenv … initW p') v = Some ? 〈tf,id〉 ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
    29933049[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
    2994 #M #initV #initW #p #p' #MP * [ | #sz #i | | #p ] #f
     3050#M #initV #initW #varsOK #p #p' #MP * [ | #sz #i | | #p ] #f #id
    29953051[ 1,2,3: #FF whd in FF:(??%?); destruct ]
    2996 whd in ⊢ (??%? → ?); @eq_offset_elim #OFF #FFP
    2997 [2: whd in FFP:(??%?); destruct ]
    2998 cases (find_funct_ptr_match M initV initW … MP (pblock p) f FFP)
     3052#FFI cases (find_funct_id_ptr ????? FFI) #b * * #E destruct #FS #FFPI
     3053cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SFB
     3054cases (find_funct_ptr_match M initV initW … MP ? f FFP)
    29993055#f' * #FFP' #MF %{f'} %
    3000 [ whd in ⊢ (??%?); >OFF >reflexive_eq_offset @FFP'
     3056[ @find_funct_ptr_id_conv
     3057  @(make_find_funct_ptr_id ???? id FFP' ?)
     3058  whd in ⊢ (??%?); >(symbols_match … initV … MP) [ @SFB | @varsOK ]
    30013059| @MF
    30023060] qed.
     
    30103068[2: #sym lapply (find_symbol_match (clight_cminor_matching p) ????? MATCHES)
    30113069    [4: #H @sym_eq @H | #X #Y * #id #r #v1 #v2 * % | skip | skip ]
    3012 |3: #v #f #FF cases (find_funct_match … MATCHES … FF)
     3070|3: #v #f #id #FF cases (find_funct_id_match … MATCHES … FF)
    30133071  [ #f' * #FF' whd in ⊢ (% → ?); * #H1 * #H2 #Efd
    30143072    % [2: %{f'} %{H1} %{H2} % [ >Efd
     
    30223080   ]
    30233081  | skip
     3082  | #X #Y * #id' #r #v1 #v2 * %
    30243083  ]
    30253084| skip
     
    31913250  whd in ⊢ (??%?); >FFP'
    31923251  whd in ⊢ (??%?); %
    3193 | @(CMR_call … FFP FFP' … (ClCm_cont_stop …))
    3194   [ @(Some ? (ASTint I32 Signed))
    3195   | @(empty_map …)
    3196   | @(empty_map …)
    3197   | @(new_universe …)
     3252| @(CMR_call … b (Some ? (ASTint I32 Signed)) (empty_map …) ? (empty_map …) … (ClCm_cont_stop …))
     3253  [ @find_funct_ptr_id_conv @make_find_funct_ptr_id
     3254    [ @FFP
     3255    | @(symbol_for_block_fn … FINDSYM FFP)
     3256    ]
     3257  | @find_funct_ptr_id_conv @make_find_funct_ptr_id
     3258    [ @FFP'
     3259    | @(symbol_for_block_fn … FFP') >M_findsym @FINDSYM
     3260    ]
    31983261  | @([ ])
    31993262  | %
  • src/Clight/toCminorCorrectnessExpr.ma

    r2822 r3165  
    1111  globals : list (ident × region × type);
    1212  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
    13   trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f
     13  trans_fn : ∀v,f,id. find_funct_id … ge_cl v = Some ? 〈f,id〉
    1414    ∃tmp_u,f',H1,H2.
    1515      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
    16       find_funct … ge_cm v = Some ? f'
     16      find_funct_id … ge_cm v = Some ? 〈f',id〉
    1717}.
    1818
Note: See TracChangeset for help on using the changeset viewer.