Changeset 3178 for src/Clight

Timestamp:

Apr 25, 2013, 6:03:24 PM (6 years ago)

Author:

campbell

Message:

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

Location:

src/Clight

Files:

• Csyntax.ma (modified) (4 diffs)
• memoryInjections.ma (modified) (2 diffs)
• toCminorCorrectness.ma (modified) (4 diffs)
• toCminorMeasurable.ma (modified) (2 diffs)

src/Clight/Csyntax.ma

@@ -346 +346 @@
 
 (* * Natural alignment of a type, in bytes. *)
-let rec alignof (t: type) : nat ≝ (*1*) 
-(* these are old values for 32 bit machines *)
+let rec alignof (t: type) : nat ≝ 1. 
+(* these are old values for 32 bit machines 
   match t with
   [ Tvoid ⇒ 1
@@ -363 +363 @@
   [ Fnil ⇒ 1
   | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
-  ].
+  ].*)
 
 (*
@@ -412 +412 @@
                         (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f')
   ].
-
+(*
 lemma alignof_fields_pos:
   ∀f. alignof_fields f > 0.
 @fieldlist_ind //;
 #i #t #fs' #IH @max_r @IH qed. 
-
+*)
 lemma alignof_pos:
   ∀t. alignof t > 0.
-#t elim t; normalize; //;
+#t elim t; normalize; //;(*
 [ 1,2: #z cases z; /2/;
 | 3,4: #i @alignof_fields_pos
-] qed.
+]*) qed.
 
 (* * Size of a type, in bytes. *)
@@ -450 +450 @@
   | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
   ].
-(* TODO: needs some Z_times results
+
 lemma sizeof_pos:
   ∀t. sizeof t > 0.
-#t0
-napply (type_ind2 (λt. sizeof t > 0)
-                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
-[ 1,4,6,9: //;
-| #i cases i;#s //;
-| #f cases f;//
-| #t #n #H whd in ⊢ (?%?);
-Proof.
-  intro t0.
-  apply (type_ind2 (fun t => sizeof t > 0)
-                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
-  intros; simpl; auto; try omega.
-  destruct i; omega.
-  destruct f; omega.
-  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
-  destruct H. 
-  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). 
-  generalize (Zmax1 1 (sizeof_struct f 0)). omega. 
-  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). 
-  generalize (Zmax1 1 (sizeof_union f)). omega. 
-  split. omega. auto.
-  destruct H0. split; intros.
-  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
-  apply H1. 
-  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
-Qed.
-
+#t elim t //
+[ * //
+| #t' * [ /2/ | #n #H change with (0 < ?) whd in ⊢ (??%); change with (0*0) in ⊢ (?%?); @lt_times // ]
+| #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1
+  >commutative_plus cases (sizeof_struct ??) [2:#x] whd in ⊢ (?(?%?)?);
+  //
+| #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1
+  >commutative_plus cases (sizeof_union ?) [2:#x] whd in ⊢ (?(?%?)?);
+  //
+] qed.
+
+(*
 Lemma sizeof_struct_incr:
   forall fld pos, pos <= sizeof_struct fld pos.

src/Clight/memoryInjections.ma

@@ -759 +759 @@
 #Halloc destruct (Halloc) /2/
 qed.
+
+lemma new_block_invalid_before_alloc :
+  ∀m,m',z1,z2,new_block.
+  alloc m z1 z2 = 〈m', new_block〉 →
+  ¬valid_block m new_block.
+* #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *)
+whd in match (alloc ???(*?*)); whd in match (valid_block ??);
+#Halloc destruct (Halloc) /2/
+qed.
+
 
 (* All data in a valid block is unchanged after an alloc. *)
@@ -1467 +1477 @@
 ] qed.   
 
+(* And show the compatibility of the new injection. *)
+
+lemma alloc_memory_inj_m1_to_m2_compat :
+  ∀E:embedding.
+  ∀m1,m2,m1':mem.
+  ∀z1,z2:Z.
+  ∀target,new_block.
+  ∀delta:offset.
+  alloc m1 z1 z2 = 〈m1', new_block〉 →
+  memory_inj E m1 m2 →
+  embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x).
+#E #m1 #m2 #m1' #z1 #z2 #target #new_block #delta #ALLOC #MI
+whd
+#b @eq_block_elim
+[ #E destruct %1 @(mi_freeblock … MI) /2/
+| #_ %2 %
+] qed.
+
+
 (* -------------------------------------- *)
 (* Lemmas pertaining to [free] *)

src/Clight/toCminorCorrectness.ma

@@ -1747 +1747 @@
 #A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed.
 
+lemma pair_as_elim:
+  ∀A,B,C: Type[0].
+  ∀p.
+  ∀T: ∀a:A. ∀b:B. 〈a,b〉 = p → C.
+  ∀P: A×B → C → Prop.
+    (∀lft, rgt. ∀E:〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt E)) →
+      P p (let 〈lft, rgt〉 as E ≝ p in T lft rgt E).
+#A #B #C * /2/
+qed.
+
+(* TODO: move *)
+lemma alloc_low_bound : ∀m,l,h,m',b.
+  alloc m l h = 〈m',b〉 →
+  low_bound m' b = l.
+* #contents #next #next_ok #l #h #m' #b #E
+whd in E:(??%%); destruct
+whd in ⊢ (??%?); >update_block_s
+%
+qed.
+
+lemma alloc_high_bound : ∀m,l,h,m',b.
+  alloc m l h = 〈m',b〉 →
+  high_bound m' b = h.
+* #contents #next #next_ok #l #h #m' #b #E
+whd in E:(??%%); destruct
+whd in ⊢ (??%?); >update_block_s
+%
+qed.
+
+(* Weaker version of Zlt_to_Zle *)
+lemma Zlt_Zle : ∀x,y:Z. x < y → x ≤ y.
+#x #y #H
+@(transitive_Zle … (Zsucc_le x)) @Zlt_to_Zle @H
+qed.
+
+axiom unZoo : ∀off:Z.
+  off < Z_two_power_nat 16 →
+  Zoo (offset_of_Z off) = off.
+
+lemma le_to_Zle : ∀x,y:nat. le x y → Zle x y.
+#x #y #H @(le_ind ????? H)
+[ //
+| #m #H1 #H2 >Zsucc_pos @(transitive_Zle … (Zsucc_le m)) assumption
+] qed.
+
+lemma lt_to_Zlt : ∀x,y:nat. lt x y → Zlt x y.
+#x #y whd in ⊢ (% → ?); #H
+<(Zpred_Zsucc x) @Zle_to_Zlt
+<Zsucc_pos
+@le_to_Zle assumption
+qed.
+
+lemma Zlt_Zsucc : ∀z:Z. z < Zsucc z.
+/2/
+qed.
+
+lemma Zle_Zlt_Zsucc : ∀x,y:Z. x ≤ y → x < Zsucc y.
+/2/
+qed.
+
+theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p.
+#n #m #p #Hle #Hlt lapply (Zlt_to_Zle … Hlt)
+@Zlt_to_Zle_to_Zlt @Zle_Zlt_Zsucc assumption
+qed.
+
+
+(* This roughly corresponds to lemma 69 of Leroy and Blazy *)
+(*
+lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame.
+∀Em. memory_inj Em cl_m cm_m →
+Z_of_nat stacksize < Z_two_power_nat 16 →
+alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 →
+∀L, cl_env, cl_m1.
+exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 →
+(∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧
+  match c with
+  [ Local ⇒ True
+  | Stack off ⇒ 
+    le O off ∧ le (sizeof ty + off) stacksize ∧
+    (∀v',off',t'. v≠v' → lookup' vartypes v' = return 〈Stack off',t'〉 → le (off' + sizeof t') off ∨ le (off + sizeof ty) off')
+  | Global _ ⇒ False
+  ]) →
+∃Em'. memory_inj Em' cl_m1 cm_m1 ∧
+  embedding_compatible Em Em' ∧
+  ∀v. Exists … (λx.\fst x = v) L →
+  ∃b,c,t. lookup … cl_env v = Some ? b ∧
+    lookup' vartypes v = return 〈c,t〉 ∧
+    match c with
+    [ Local ⇒ Em' b = None ?
+    | Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉
+    | Global _ ⇒ False
+    ].
+#vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L
+cut (block_implementable_bv cm_m1 cm_frame)
+[ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % //
+  cases stacksize // ] #cm_bi
+lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi)
+lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid
+cut (∀b:block. ∀delta':offset.
+    Em b=Some (block×offset) 〈cm_frame,delta'〉 → 
+    ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 →
+    high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off)
+      ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta')
+[ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V
+  @(absurd … V) @(new_block_invalid_before_alloc … cm_alloc) ]
+
+generalize in match Em; -Em generalize in match empty_env; elim L
+[ #cl_env #Em #_ #Inj #cl_env' #cl_m1 #cl_alloc
+  whd in cl_alloc:(??%%); destruct #H
+  %{Em} % [ % [ @Inj | // ] | #v * ]
+| * #v #ty #tl #IH
+  #cl_env #Em #Hexisting #Inj #cl_env' #cl_m1
+  whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H
+  cases (H v ty ?) [2: %1 % ] *
+  [ #r * #L *
+  | #off * #L * * #off_low #off_high #other
+    lapply (alloc_memory_inj_m1_to_m2 … (offset_of_Z off) cm_frame_valid … cm_bi … cl_alloc … Inj)
+    [ #b #delta' #NE #E @(Hexisting … E … L)
+    | cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U
+      [ /2/
+      | @(transitive_Zle … HIGH) >unZoo
+        [ <eq_plus_Zplus /2/
+        | @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off))
+          [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/
+          | @(transitive_Zlt … stacksize) [ <eq_plus_Zplus @(lt_to_Zlt … off_high) | // ]
+          ]
+        ]
+      ]
+    | >unZoo
+        [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc) 
+*)
 (*
 lemma lset_inclusion_Exists :
@@ -1790 +1921 @@
    subtrace corresponding to a measurable Clight subtrace.
  *)
-(* WIP
+(* WIP 
+include "common/ExtraMonads.ma".
+
 lemma clight_cminor_call :
     ∀g,g'.
@@ -1831 +1964 @@
       whd in STEP1:(??%%); destruct ]
   -cl_fd
+  (* and the Cminor one must be Internal *)
+  @('bind_inversion Htranslate) #cm_f #Htranslate' #E
+  whd in E:(??%%); destruct
+
+  (* Invert function translation *)
+  (* NB: if you want to examine the proof state in here, you probably want to
+     turn off the pretty printer - it doesn't cope well with a large proof
+     term. *)
+  @('bind_inversion Htranslate') * * #lbls #Ilbls #ul #Hbuild_label_env
+  whd in ⊢ (??%? → ?);
+  @pair_as_elim #vartypes #stacksize #Hcharacterise
+  letin uv ≝ (mk_tmpgen ?? [ ] ??) #H
+  @('bind_inversion H) -H #s0 #Htranslate_statement #H
+  @('bind_inversion H) -H * * #fgens #s1 #Is #Halloc_params
+  letin cm_params ≝ (map ??? (fn_params cl_f))
+  whd in ⊢ (??%? → ?);
+  letin cm_vars ≝ (map ??? (?@fn_vars cl_f)) #H
+  @('bind_inversion H) -H #D #Hcheck_distinct_env
+  whd in ⊢ (??%% → ?); generalize in ⊢ (??(??(???????%))? → ?);
+  (* It's safe to use the pretty printer again. *)
+  #cm_Sinv #H destruct
 
   (* Invert Clight STEP1 *)  
@@ -1836 +1990 @@
   cases (bindIO_inversion ??????? STEP1) -STEP1 #cl_m2 * #BIND #STEP1
   whd in STEP1:(??%%); destruct
+
+  whd whd in ⊢ (??%?);
+  @pair_elim #cm_m1 #cm_frame #CM_ALLOC
+
+ (〈vartypes,stacksize〉=characterise_vars (globals g g' INV) cl_f)
+We need to build an extended memory injection to reflect the new allocations;
+then the bind functions put the correct local variables in;
+then after execution the appropriate number of Cminor steps the stored values
+match.
+
+Oh, and there are the locals too.
+
+
+alloc_memory_inj_m2 shows that embedding is fine after the Cminor alloc
+
+∀Em. memory_inj Em cl_m cm_m →
+(∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) →
+exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 →
+alloc cm_m O (f_stacksize cm_f) = 〈cm_m1,cm_frame〉 →
+∃Em'.
+  memory_inj Em' cl_m1 cm_m1 ∧
+  (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) ∧
+  (∀v,v'. value_eq Em v v' → value_eq Em' v v') ∧
+  (∀b1.∀delta. Em' b1=Some ? 〈cm_frame,delta〉 →
+             mem block b1 (blocks_of_env cl_env)).
+             
+  ∀b. Em b = Em' b ∨ (Em b = None ? ∧ ∃off. Em' b = Some ? 〈cm_frame,off〉).
+
+
+translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f →
+All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args →
+exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 →
+∃cm_en,Hcm_args_present.
+  bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧
+  
+
 *)
 

src/Clight/toCminorMeasurable.ma

@@ -64 +64 @@
   #ge #ge' #RG #Xs1 #Xs2 * //
   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #E
-  | #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #H169 #H170 #E
+  | #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 #H168 #E
   | #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 #H140 #H141 #H142 #E
   ] whd in E:(??%?); destruct
@@ -71 +71 @@
   [ #H189 #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 *
   | #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 #H255 #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 #H266 *
-  | #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 #H295 #H296
+  | #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 #H278 #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 #H292 #H293 #H294 
   | #H314 #H315 #H316 #H317 #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 #H331 #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 #H342 #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 #H356 #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 #H370 #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 *
   ] (* FIXME *) cases daemon