Changeset 2389


Ignore:
Timestamp:
Oct 5, 2012, 12:57:19 PM (7 years ago)
Author:
campbell
Message:

Fix dowhile statements, and carefully arrange the translation so that
we get nice cost labelling properties.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2353 r2389  
    11691169    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    11701170    ] e1'
     1171(* Performing loop conversions while keeping good cost labelling properties is
     1172   a little tricky.  In principle we should have a cost label in each branch,
     1173   but the behaviour of the next stage means that we can put in Cminor skips and
     1174   goto labels before the cost label. *)
    11711175| Swhile e1 s1 cl ⇒
    11721176    do e1' ← translate_expr vars e1;
     
    11891193    [ ASTint _ _ ⇒ λe1'.
    11901194        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
    1191         let 〈entry, exit〉 as E2 ≝ labels in             
    1192         do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1;
     1195        let 〈condexpr, exit〉 as E2 ≝ labels in
     1196        let 〈body, ul2〉 ≝ generate_fresh_label … ul1 in
     1197        do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls (ConvertTo condexpr exit) rettyp s1;
     1198        (* This is particularly carefully implemented, we need to reach the
     1199           cost label in s1' or the cost label after the loop (if they are
     1200           present) after the ifthenelse, and we're only allowed skips and
     1201           goto labels in between.  So we structure it like a while with a goto
     1202           into the middle (the CFG will be essentially the same, anyway.) *)
    11931203        let converted_loop ≝
    1194           St_label entry
    1195            (St_seq
    1196              (St_seq
    1197                s1'
    1198                (St_ifthenelse ?? e1' (St_goto entry) St_skip)
    1199              )
    1200              (St_label exit St_skip))
     1204        St_seq
     1205          (St_seq
     1206            (St_goto body)
     1207            (St_label condexpr
     1208              (St_ifthenelse ?? e1'
     1209                (St_label body
     1210                  (St_seq
     1211                    s1'
     1212                    (St_goto condexpr)))
     1213                St_skip)))
     1214          (St_label exit St_skip)
    12011215        in
    12021216        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     
    13401354                | 3,6: #H %2 assumption ] ]
    13411355try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption
    1342 [ 1,10,20: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1356[ 1,10,22: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    13431357| cases cl normalize /3/
    13441358| (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //
     
    13471361         @conj
    13481362         [ 1,3: @(proj1 … Hlabel)
    1349          | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l
    1350               @(proj2 … Hlabel) ]
    1351 | 30: whd %2 %2 whd /2/
    1352 | 31: whd %2 whd /2/
     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) ]
    13531366| cases cl normalize /3/
    1354 | 5,17: whd %1 %1 normalize /2/
    1355 | 6,13: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    1356    #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H
     1367| 5,13,16: whd %1 %1 normalize /2/
     1368| 6,15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1369   #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H
    13571370              | 2,6: #H %1 %2 assumption
    13581371              | 3,7: #H <H %1 %1 normalize /2/
    1359               | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2
     1372              | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 [2: %2]
    13601373                                                 @Exists_append_r normalize /2/
    13611374                                               | 2,4: * ]
    13621375              ]
    13631376| 7: normalize %1 %1 %1 //
    1364 | 8,15: normalize %1 %1 %2 @Exists_append_r normalize /2/
     1377| 8,14: normalize %1 %1 %2 [ @Exists_append_r normalize /2/ | %1 % ]
    13651378| cases cl normalize /3/
    1366 | 12,14: whd %1 %1 normalize /2/
    1367 | 16: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
    1368                    | 2: #H elim (Hlabels_tr1 label H)
    1369                          #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
    1370                          [ 1: // | 2: whd %2 assumption ]
    1371                    ]
    1372 | 18: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    1373    #l * try * [ 1: #H %1 %1 normalize %2 @H
    1374               | 2: #H %1 %2 assumption
    1375               | 3: #H %2 assumption ]
    1376 | 19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    1377    #H @(Htmps_pres3 … (Htmps_pres2 … H))
    1378 | 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    1379    #H @(Htmps_pres3 … H)
    1380 | 22: whd #l #H normalize in H;
    1381       cases (Exists_append … H) #Hcase
    1382       [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
    1383         [ 1: @(proj1 … Hlabel)
    1384         | 2: normalize @Exists_append_l @(proj2 … Hlabel)
    1385         ]
    1386       | 2: cases (Exists_append … Hcase) #Hcase2
    1387         [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
    1388           [ 1: @(proj1 … Hlabel)
    1389           | 2: normalize >append_nil >append_nil >append_cons
    1390                @Exists_append_r @Exists_append_l @Exists_append_r
    1391                @(proj2 … Hlabel)
    1392           ]
    1393         | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
    1394           [ 1: @(proj1 … Hlabel)
    1395           | 2: normalize >append_nil >append_nil >append_cons
    1396              @Exists_append_r @Exists_append_l @Exists_append_l
    1397              @(proj2 … Hlabel)
    1398           ]
    1399         ]
     1379| whd %1 %1 normalize %2 %1 %
     1380| normalize %1 %1 %2 %2 /2/
     1381| whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]
     1382               | 2: #H elim (Hlabels_tr1 label H)
     1383                    #lab * #Hlookup #Hdef @(ex_intro … lab) @conj
     1384                    [ 1: // | 2: whd %2 assumption ]
     1385               ]
     1386| normalize %1 %1 %1 %
     1387| @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1388  #l * try * [ 1: #H %1 %1 normalize %2 @H
     1389             | 2: #H %1 %2 assumption
     1390             | 3: #H %2 assumption ]
     1391| @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1392  #H @(Htmps_pres3 … (Htmps_pres2 … H))
     1393| @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
     1394  #H @(Htmps_pres3 … H)
     1395| whd #l #H normalize in H;
     1396  cases (Exists_append … H) #Hcase
     1397  [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj
     1398    [ 1: @(proj1 … Hlabel)
     1399    | 2: normalize @Exists_append_l @(proj2 … Hlabel)
     1400    ]
     1401  | 2: cases (Exists_append … Hcase) #Hcase2
     1402    [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
     1403      [ 1: @(proj1 … Hlabel)
     1404      | 2: normalize >append_nil >append_nil >append_cons
     1405           @Exists_append_r @Exists_append_l @Exists_append_r
     1406           @(proj2 … Hlabel)
    14001407      ]
    1401 | 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
    1402 | 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1408    | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj
     1409      [ 1: @(proj1 … Hlabel)
     1410      | 2: normalize >append_nil >append_nil >append_cons
     1411         @Exists_append_r @Exists_append_l @Exists_append_l
     1412         @(proj2 … Hlabel)
     1413      ]
     1414    ]
     1415  ]
     1416| #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))
     1417| @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    14031418   #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H
    14041419              | 2: #H %1 %2 assumption
    14051420              | 3: #H %2 assumption ]
    1406 | 25: whd %1 %1 normalize /2/
    1407 | 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1421| whd %1 %1 normalize /2/
     1422| @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    14081423   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    14091424                   @Exists_append_r @Exists_append_l @Exists_append_l
     
    14181433                     | 2: * ]
    14191434              ]
    1420 | 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1435| @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    14211436   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    14221437                   @Exists_append_r @Exists_append_l @Exists_append_l                   
     
    14301445                     | 2: * ]
    14311446              ]
    1432 | 28: whd %1 %1 normalize /2/
    1433 | 29: whd %1 %1 normalize
    1434       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
    1435       whd %1 //
    1436 | 32: whd %1 %2 whd @(ex_intro … l) @E
     1447| whd %1 %1 normalize /2/
     1448| whd %1 %1 normalize
     1449  @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r
     1450  whd %1 //
     1451| normalize %2 /3/
     1452| normalize /4/
     1453| whd %1 %2 whd @(ex_intro … l) @E
    14371454] qed.
    14381455
Note: See TracChangeset for help on using the changeset viewer.