Ignore:
Timestamp:
Oct 9, 2012, 3:10:07 PM (8 years ago)
Author:
campbell
Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2389 r2391  
    5151                         gather_mem_vars_stmt s1 ∪
    5252                         gather_mem_vars_stmt s2
    53 | Swhile e1 s1 _ ⇒ gather_mem_vars_expr e1 ∪
    54                    gather_mem_vars_stmt s1
     53| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
     54                 gather_mem_vars_stmt s1
    5555| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
    5656                   gather_mem_vars_stmt s1
     
    926926[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    927927| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    928 | Swhile _ s _ ⇒ labels_defined s
     928| Swhile _ s ⇒ labels_defined s
    929929| Sdowhile _ s ⇒ labels_defined s
    930930| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     
    11241124axiom ReturnMismatch : String.
    11251125
    1126 definition optional_cost : option costlabel → stmt → stmt ≝
    1127 λo,s. match o with [ Some l ⇒ St_cost l s | None ⇒ s ].
    1128 
    11291126let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s
    11301127  : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝
     
    11731170   but the behaviour of the next stage means that we can put in Cminor skips and
    11741171   goto labels before the cost label. *)
    1175 | Swhile e1 s1 cl
     1172| Swhile e1 s1
    11761173    do e1' ← translate_expr vars e1;
    11771174    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     
    11831180        let converted_loop ≝
    11841181          St_label entry
    1185             (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) (St_label exit (optional_cost cl St_skip)))
     1182          (St_seq
     1183            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
     1184            (St_label exit St_skip))
    11861185        in         
    11871186          OK ? «〈fgens2, converted_loop〉, ?»
     
    13541353                | 3,6: #H %2 assumption ] ]
    13551354try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
    1356 [ 1,10,22: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    1357 | cases cl normalize /3/
    1358 | (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
    1359 |*) 3,11: whd #l #H normalize in H;
    1360          elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
    1361          @conj
    1362          [ 1,3: @(proj1 … Hlabel)
    1363          | 2,4: whd @or_intror normalize in ⊢ (???%);
    1364                 [ @Exists_append_l @Exists_append_l | %2 @Exists_append_l @Exists_append_l @Exists_append_l ]
    1365                 @(proj2 … Hlabel) ]
    1366 | cases cl normalize /3/
    1367 | 5,13,16: whd %1 %1 normalize /2/
    1368 | 6,15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1355[ 1,7,19: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1356| 2,8: whd #l #H normalize in H;
     1357       elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label)
     1358       @conj
     1359       [ 1,3: @(proj1 … Hlabel)
     1360       | 2,4: whd @or_intror normalize in ⊢ (???%);
     1361              [ @Exists_append_l @Exists_append_l @Exists_append_l | %2 @Exists_append_l @Exists_append_l @Exists_append_l ]
     1362              @(proj2 … Hlabel) ]
     1363| whd %1 %1 normalize /2/
     1364| 4,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    13691365   #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H
    13701366              | 2,6: #H %1 %2 assumption
     
    13741370                                               | 2,4: * ]
    13751371              ]
    1376 | 7: normalize %1 %1 %1 //
    1377 | 8,14: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ]
    1378 | cases cl normalize /3/
     1372| normalize %1 %1 %1 //
     1373| 6,11: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ]
    13791374| whd %1 %1 normalize %2 %1 %
     1375| 10,13: normalize %1 %1 %1 %
    13801376| normalize %1 %1 %2 %2 /2/
    13811377| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
Note: See TracChangeset for help on using the changeset viewer.