Changeset 2407


Ignore:
Timestamp:
Oct 19, 2012, 11:18:52 AM (7 years ago)
Author:
campbell
Message:

Sigh, continue in for loops was broken too.

Location:
src/Clight
Files:
3 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2391 r2407  
    11741174    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    11751175    [ ASTint _ _ ⇒ λe1'.         
    1176         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    11771176        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
    11781177        let 〈entry, exit〉 as E2 ≝ labels in
     
    12131212          (St_label exit St_skip)
    12141213        in
    1215         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    12161214        OK ? «〈fgens2, converted_loop〉, ?»
    12171215    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    12221220    [ ASTint _ _ ⇒ λe1'.
    12231221        let 〈labels, ul1〉 as E ≝ mklabels ul in
    1224         let 〈entry, exit〉 as E2 ≝ labels in                           
    1225         do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag rettyp s1;
    1226         do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) rettyp s2;
    1227         do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) rettyp s3;
    1228         (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1222        let 〈continue, exit〉 as E2 ≝ labels in
     1223        let 〈entry, ul2〉 ≝ generate_fresh_label … ul1 in
     1224        do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls flag rettyp s1;
     1225        (* The choice of flag is arbitrary - Clight's semantics give no meaning
     1226           to continue or break in s2 because in C it must be an expression. *)
     1227        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls flag rettyp s2;
     1228        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo continue exit) rettyp s3;
    12291229        let converted_loop ≝
    12301230          St_seq
     
    12321232            (St_label entry
    12331233              (St_seq
    1234                 (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
     1234                (St_ifthenelse ?? e1' (St_seq s3' (St_label continue (St_seq s2' (St_goto entry)))) St_skip)
    12351235                (St_label exit St_skip)
    12361236            ))
     
    13891389| @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t
    13901390  #H @(Htmps_pres3 … H)
     1391| % //
    13911392| whd #l #H normalize in H;
    13921393  cases (Exists_append … H) #Hcase
     
    13991400      [ 1: @(proj1 … Hlabel)
    14001401      | 2: normalize >append_nil >append_nil >append_cons
    1401            @Exists_append_r @Exists_append_l @Exists_append_r
     1402           @Exists_append_r @Exists_append_l @Exists_append_r %2
    14021403           @(proj2 … Hlabel)
    14031404      ]
     
    14221423              | 2: #H %1 %2 assumption
    14231424              | 3: #H <H %1 %1 normalize
    1424                    @Exists_append_r whd %1 //
    1425               | 4: * [ 1: #H <H %1 %1 normalize
    1426                        @Exists_append_r @(Exists_add ?? (nil ?))
    1427                        @Exists_append_r @Exists_append_r
    1428                        whd %1 //
    1429                      | 2: * ]
    1430               ]
    1431 |  @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
    1432    #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
    1433                    @Exists_append_r @Exists_append_l @Exists_append_l                   
    1434                    @Exists_append_r @Exists_append_l assumption
    1435               | 2: #H %1 %2 assumption
    1436               | 3: #H <H %1 %1 normalize
    1437                    @Exists_append_r whd %1 //
     1425                   @Exists_append_r %2 @Exists_append_l @Exists_append_l
     1426                   @Exists_append_r %1 %
    14381427              | 4: * [ 1: #Eq <Eq %1 %1 whd normalize
    14391428                       @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r
    14401429                       @Exists_append_r whd %1 //
    14411430                     | 2: * ]
     1431              ]
     1432| % %1 normalize @Exists_append_r %2 @Exists_append_l @Exists_append_l
     1433  @Exists_append_r % %
     1434| @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)
     1435   #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?))
     1436                   @Exists_append_r @Exists_append_l @Exists_append_l                   
     1437                   @Exists_append_r %2 @Exists_append_l assumption
     1438              | 2: #H %1 %2 assumption
     1439              | 3: /2/
    14421440              ]
    14431441| whd %1 %1 normalize /2/
Note: See TracChangeset for help on using the changeset viewer.