Changeset 1197


Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (8 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 deleted
26 edited
5 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma

    r1153 r1197  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
    149 definition RegisterForbidden: list Register ≝
    150   [ RegisterSST; RegisterST0; RegisterST1;
    151     RegisterSPL; RegisterSPH ].
    152149definition RegisterParams: list Register ≝
    153150  [ Register30; Register31; Register32; Register33;
     
    173170  [Register20; Register21; Register22; Register23; Register24;
    174171   Register25; Register26; Register27].
     172definition RegistersForbidden ≝
     173  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
     174   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
     175   RegisterST2; RegisterST3; RegisterSST].
     176(* registers minus forbidden *)
     177definition RegistersAllocatable ≝
     178  [Register00; Register01; Register02; Register03; Register04;
     179   Register05; Register06; Register07; Register10; Register11;
     180   Register12; Register13; Register14; Register15; Register16;
     181   Register17; Register20; Register21; Register22; Register23;
     182   Register24; Register25; Register26; Register27; Register30;
     183   Register31; Register32; Register33; Register34; Register35;
     184   Register36; Register37].
    175185
    176186definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  • Deliverables/D3.3/id-lookup-branch/ASM/Util.ma

    r1098 r1197  
    1111example not_implemented: False. cases daemon qed.
    1212
     13notation "⊥" with precedence 90
     14  for @{ match ? in False with [ ] }.
     15
    1316notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    1417 with precedence 10
    1518for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     19
     20(*
     21notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
     22 with precedence 10
     23for @{
     24  match $t with
     25  [ pair ${ident x} y' ⇒
     26    match y' with
     27    [ pair ${ident y} ${ident z} ⇒ $s ]
     28  ]
     29}.
     30*)
    1631
    1732definition ltb ≝
     
    3247  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    3348  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     49  ].
     50
     51let rec forall
     52  (A: Type[0]) (f: A → bool) (l: list A)
     53    on l ≝
     54  match l with
     55  [ nil        ⇒ true
     56  | cons hd tl ⇒ f hd ∧ forall A f tl
    3457  ].
    3558
     
    614637  ]
    615638qed.
     639
     640lemma nth_append_first:
     641 ∀A:Type[0].
     642 ∀n:nat.∀l1,l2:list A.∀d:A.
     643   n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
     644 #A #n #l1 #l2 #d
     645 generalize in match n; -n; elim l1
     646 [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
     647 | #h #t #Hind #k normalize
     648   cases k -k
     649   [ #Hk normalize @refl
     650   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
     651   ] 
     652 ]
     653qed.
     654
     655lemma nth_append_second:
     656 ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
     657  nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
     658 #A #n #l1 #l2 #d
     659 generalize in match n; -n; elim l1
     660 [ normalize #k #Hk <(minus_n_O) @refl
     661 | #h #t #Hind #k normalize
     662   cases k -k;
     663   [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
     664   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
     665   ]
     666 ]
     667qed.
     668
    616669   
    617670notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
     
    699752qed.
    700753
    701 
    702 notation "⊥" with precedence 90
    703   for @{ match ? in False with [ ] }.
    704754
    705755let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
  • Deliverables/D3.3/id-lookup-branch/Clight/clightPrintMatita.ml

    r965 r1197  
    367367
    368368let print_globvar p (((id, init), ty)) =
    369   fprintf p "@[<hov 2>〈〈〈ident_of_nat %i (* %s *),@ %a〉,@ Any〉,@ %s〉@]"
     369  fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ Any〉,@ 〈%a,@ %s〉〉@]"
    370370    (id_i id)
    371371    id
     
    466466  collect_program prog;
    467467  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
    468   fprintf p "@[<v 2>definition myprog := mk_program clight_fundef type@ ";
     468  fprintf p "@[<v 2>definition myprog := mk_program clight_fundef ((list init_data) × type)@ ";
    469469(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    470470  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
  • Deliverables/D3.3/id-lookup-branch/Clight/test/duff.c.ma

    r965 r1197  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* copy *), CL_Internal (
    66     mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     
    409409
    410410example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    411 normalize @refl
     411normalize  (* you can examine the result here *)
     412@refl
    412413qed.
  • Deliverables/D3.3/id-lookup-branch/Clight/test/factorial.c.ma

    r978 r1197  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    66  〈ident_of_nat 1 (* main *), CL_Internal (
     
    4141example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    4242normalize  (* you can examine the result here *)
    43 @refl qed.
     43@refl
     44qed.
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1153 r1197  
    44include "utilities/lists.ma".
    55include "utilities/deppair.ma".
    6 (*
    7 let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
    8 match e with
    9 [ Expr ed ty ⇒
    10     match ed with
    11     [ Ederef e1 ⇒ mem_vars_expr mem_vars e1
    12     | Eaddrof e1 ⇒ mem_vars_addr mem_vars e1
    13     | Eunop _ e1 ⇒ mem_vars_expr mem_vars e1
    14     | Ebinop _ e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
    15                        mem_vars_expr mem_vars e2
    16     | Ecast _ e1 ⇒ mem_vars_expr mem_vars e1
    17     | Econdition e1 e2 e3 ⇒ mem_vars_expr mem_vars e1 ∧
    18                             mem_vars_expr mem_vars e2 ∧
    19                             mem_vars_expr mem_vars e3
    20     | Eandbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
    21                        mem_vars_expr mem_vars e2
    22     | Eorbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
    23                       mem_vars_expr mem_vars e2
    24     | Efield e1 _ ⇒ mem_vars_expr mem_vars e1
    25     | Ecost _ e1 ⇒ mem_vars_expr mem_vars e1
    26     | _ ⇒ True
    27     ]
    28 ]
    29 and mem_vars_addr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
    30 match e with
    31 [ Expr ed ty ⇒
    32     match ed with
    33     [ Evar x ⇒ mem_set ? mem_vars x = true
    34     | Ederef e1 ⇒ mem_vars_expr mem_vars e1
    35     | Efield e1 _ ⇒ mem_vars_addr mem_vars e1
    36     | _ ⇒ False (* not an lvalue *)
    37     ]
    38 ].
    39 
    40 let rec mem_vars_stmt (mem_vars:identifier_set SymbolTag) (s:statement) on s : Prop ≝
    41 match s with
    42 [ Sskip ⇒ True
    43 | Sassign e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
    44                   mem_vars_expr mem_vars e2
    45 | Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ] ∧
    46                     mem_vars_expr mem_vars e2 ∧
    47                     All ? (mem_vars_expr mem_vars) es
    48 | Ssequence s1 s2 ⇒ mem_vars_stmt mem_vars s1 ∧
    49                     mem_vars_stmt mem_vars s2
    50 | Sifthenelse e1 s1 s2 ⇒ mem_vars_expr mem_vars e1 ∧
    51                          mem_vars_stmt mem_vars s1 ∧
    52                          mem_vars_stmt mem_vars s2
    53 | Swhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
    54                  mem_vars_stmt mem_vars s1
    55 | Sdowhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
    56                    mem_vars_stmt mem_vars s1
    57 | Sfor s1 e1 s2 s3 ⇒ mem_vars_stmt mem_vars s1 ∧
    58                      mem_vars_expr mem_vars e1 ∧
    59                      mem_vars_stmt mem_vars s2 ∧
    60                      mem_vars_stmt mem_vars s3
    61 | Sbreak ⇒ True
    62 | Scontinue ⇒ True
    63 | Sreturn oe1 ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ]
    64 | Sswitch e1 ls ⇒ mem_vars_expr mem_vars e1 ∧
    65                   mem_vars_ls mem_vars ls
    66 | Slabel _ s1 ⇒ mem_vars_stmt mem_vars s1
    67 | Sgoto _ ⇒ True
    68 | Scost _ s1 ⇒ mem_vars_stmt mem_vars s1
    69 ]
    70 and mem_vars_ls (mem_vars:identifier_set SymbolTag) (ls:labeled_statements) on ls : Prop ≝
    71 match ls with
    72 [ LSdefault s1 ⇒ mem_vars_stmt mem_vars s1
    73 | LScase _ s1 ls1 ⇒ mem_vars_stmt mem_vars s1 ∧
    74                     mem_vars_ls mem_vars ls1
    75 ].
    76 *)
     6
     7(* Identify local variables that must be allocated memory. *)
    778
    789let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
     
    693624whd // >E @I
    694625qed.
    695 (*
    696 definition translate_assign ≝
    697 λvars,e1,e2.
    698     do e2' ← translate_expr vars e2;
    699     do q ← match access_mode (typeof e2) with
    700            [ By_value q ⇒ OK ? q
    701            | By_reference r ⇒ OK ? (Mpointer r)
    702            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    703            ];
    704     match e1 with
    705     [ Expr ed1 ty1 ⇒
    706         match ed1 with
    707         [ Evar id ⇒
    708             do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    709             match c with
    710             [ Local ⇒ OK ? (St_assign id e2')
    711             | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2')
    712             | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2')
    713             ]
    714         | _ ⇒
    715             do e1' ← translate_addr vars e1;
    716             OK ? (St_store q e1' e2')
    717         ]
    718     ].
    719 *)
    720626
    721627definition lenv ≝ identifier_map SymbolTag (identifier Label).
  • Deliverables/D3.3/id-lookup-branch/Cminor/cminorMatitaPrinter.ml

    r966 r1197  
    2828
    2929let print_var n (id, sz, init) =
    30   Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
     30  Printf.sprintf "(pair ?? (pair ?? id_%s Any) [%s])"
    3131    id
    3232    (match init with
  • Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma

    r966 r1197  
    44
    55
    6 definition id_search := ident_of_nat 0.
    7 definition id_search_high := ident_of_nat 10.
    8 definition id_search_i := ident_of_nat 11.
    9 definition id_search_low := ident_of_nat 12.
    10 definition id_search_tab := ident_of_nat 13.
    11 definition id_search_size := ident_of_nat 14.
    12 definition id_search_to_find := ident_of_nat 15.
    13 definition C_cost8 := costlabel_of_nat 9.
    14 definition C_cost6 := costlabel_of_nat 8.
    15 definition C_cost4 := costlabel_of_nat 7.
    16 definition C_cost5 := costlabel_of_nat 6.
    17 definition C_cost2 := costlabel_of_nat 5.
    18 definition C_cost3 := costlabel_of_nat 4.
    19 definition C_cost0 := costlabel_of_nat 3.
    20 definition C_cost1 := costlabel_of_nat 2.
    21 definition C_cost7 := costlabel_of_nat 1.
    22 definition f_search := Internal ? (mk_internal_function
    23   (Some ? (ASTint I8 Unsigned))
    24   [pair ?? id_search_tab (ASTptr Any); pair ?? id_search_size (ASTint I8 Unsigned); pair ?? id_search_to_find (ASTint I8 Unsigned)]
    25   [pair ?? id_search_high (ASTint I8 Unsigned); pair ?? id_search_i (ASTint I8 Unsigned); pair ?? id_search_low (ASTint I8 Unsigned)]
     6definition id__div32u := ident_of_nat 0.
     7definition id__div32u_quo := ident_of_nat 4.
     8definition id__div32u_rem := ident_of_nat 5.
     9definition id__div32u_x := ident_of_nat 6.
     10definition id__div32u_y := ident_of_nat 7.
     11definition C_cost2 := costlabel_of_nat 3.
     12definition C_cost0 := costlabel_of_nat 2.
     13definition C_cost1 := costlabel_of_nat 1.
     14definition f__div32u := Internal ? (mk_internal_function
     15  (Some ? (ASTint I32 Unsigned))
     16  [pair ?? id__div32u_x (ASTint I32 Unsigned); pair ?? id__div32u_y (ASTint I32 Unsigned)]
     17  [pair ?? id__div32u_quo (ASTint I32 Unsigned); pair ?? id__div32u_rem (ASTint I32 Unsigned)]
    2618  0 (
    27   St_cost C_cost8 (
    28   St_seq (
    29     St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    30   ) (
    31   St_seq (
    32     St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Osub (Id (ASTint I8 Unsigned) id_search_size) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))
     19  St_cost C_cost2 (
     20  St_seq (
     21    St_assign (ASTint I32 Unsigned) id__div32u_quo (Op1 (ASTint I8 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     22  ) (
     23  St_seq (
     24    St_assign (ASTint I32 Unsigned) id__div32u_rem (Id (ASTint I32 Unsigned) id__div32u_x)
    3325  ) (
    3426  St_seq (
     
    3729        St_loop (
    3830          St_seq (
    39             St_ifthenelse I8 Unsigned (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) Onotbool (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Cge) (Id (ASTint I8 Unsigned) id_search_high) (Id (ASTint I8 Unsigned) id_search_low))) (
     31            St_ifthenelse I32 Signed (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onotbool (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocmpu Cge) (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y))) (
    4032              St_exit 0
    4133            ) (
     
    4335          ) (
    4436          St_block (
    45             St_cost C_cost6 (
    46             St_seq (
    47               St_assign (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Odivu (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Oadd (Id (ASTint I8 Unsigned) id_search_high) (Id (ASTint I8 Unsigned) id_search_low)) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 2)))))
    48             ) (
    49             St_seq (
    50               St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Ceq) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
    51                 St_cost C_cost4 (
     37            St_cost C_cost0 (
     38            St_seq (
     39              St_assign (ASTint I32 Unsigned) id__div32u_rem (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Osub (Id (ASTint I32 Unsigned) id__div32u_rem) (Id (ASTint I32 Unsigned) id__div32u_y))
     40            ) (
     41            St_assign (ASTint I32 Unsigned) id__div32u_quo (Op2 (ASTint I32 Unsigned) (ASTint I32 Unsigned) (ASTint I32 Unsigned) Oadd (Id (ASTint I32 Unsigned) id__div32u_quo) (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
     42            )
     43            )
     44          )
     45          )
     46        )
     47      )
     48    ) (
     49    St_cost C_cost1 (
     50    St_skip    )
     51    )
     52  ) (
     53  St_return (Some ? (dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32u_quo)))
     54  )
     55  )
     56  )
     57  )
     58
     59)).
     60
     61definition id__div32s := ident_of_nat 8.
     62definition id__div32s__tmp2 := ident_of_nat 14.
     63definition id__div32s_sign := ident_of_nat 15.
     64definition id__div32s_x1 := ident_of_nat 16.
     65definition id__div32s_y1 := ident_of_nat 17.
     66definition id__div32s__tmp_0 := ident_of_nat 18.
     67definition id__div32s_x := ident_of_nat 19.
     68definition id__div32s_y := ident_of_nat 20.
     69definition C_cost7 := costlabel_of_nat 13.
     70definition C_cost5 := costlabel_of_nat 12.
     71definition C_cost6 := costlabel_of_nat 11.
     72definition C_cost3 := costlabel_of_nat 10.
     73definition C_cost4 := costlabel_of_nat 9.
     74definition f__div32s := Internal ? (mk_internal_function
     75  (Some ? (ASTint I32 Signed))
     76  [pair ?? id__div32s_x (ASTint I32 Signed); pair ?? id__div32s_y (ASTint I32 Signed)]
     77  [pair ?? id__div32s__tmp2 (ASTint I32 Unsigned); pair ?? id__div32s_sign (ASTint I32 Signed); pair ?? id__div32s_x1 (ASTint I32 Unsigned); pair ?? id__div32s_y1 (ASTint I32 Unsigned); pair ?? id__div32s__tmp_0 (ASTint I32 Unsigned)]
     78  0 (
     79  St_cost C_cost7 (
     80  St_seq (
     81    St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Id (ASTint I32 Signed) id__div32s_x))
     82  ) (
     83  St_seq (
     84    St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Id (ASTint I32 Signed) id__div32s_y))
     85  ) (
     86  St_seq (
     87    St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))
     88  ) (
     89  St_seq (
     90    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Id (ASTint I32 Signed) id__div32s_x) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
     91      St_cost C_cost5 (
     92      St_seq (
     93        St_assign (ASTint I32 Unsigned) id__div32s_x1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_x)))
     94      ) (
     95      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_sign))
     96      )
     97      )
     98    ) (
     99      St_cost C_cost6 (
     100      St_skip      )
     101    )
     102  ) (
     103  St_seq (
     104    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Id (ASTint I32 Signed) id__div32s_y) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
     105      St_cost C_cost3 (
     106      St_seq (
     107        St_assign (ASTint I32 Unsigned) id__div32s_y1 (Op1 (ASTint I32 Signed) (ASTint I32 Unsigned) (Ocastint Signed I32) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_y)))
     108      ) (
     109      St_assign (ASTint I32 Signed) id__div32s_sign (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Id (ASTint I32 Signed) id__div32s_sign))
     110      )
     111      )
     112    ) (
     113      St_cost C_cost4 (
     114      St_skip      )
     115    )
     116  ) (
     117  St_seq (
     118    St_seq (
     119      St_call (Some ? id__div32s__tmp_0) (Cst ? (Oaddrsymbol id__div32u 0)) [dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_x1); dp ?? (ASTint I32 Unsigned) (Id (ASTint I32 Unsigned) id__div32s_y1)]
     120    ) (
     121    St_assign (ASTint I32 Unsigned) id__div32s__tmp2 (Id (ASTint I32 Unsigned) id__div32s__tmp_0)
     122    )
     123  ) (
     124  St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Id (ASTint I32 Signed) id__div32s_sign) (Op1 (ASTint I32 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I32 Unsigned) id__div32s__tmp2)))))
     125  )
     126  )
     127  )
     128  )
     129  )
     130  )
     131  )
     132
     133)).
     134
     135definition id_search := ident_of_nat 21.
     136definition id_search__tmp4 := ident_of_nat 31.
     137definition id_search_high := ident_of_nat 32.
     138definition id_search_i := ident_of_nat 33.
     139definition id_search_low := ident_of_nat 34.
     140definition id_search__tmp_1 := ident_of_nat 35.
     141definition id_search_tab := ident_of_nat 36.
     142definition id_search_size := ident_of_nat 37.
     143definition id_search_to_find := ident_of_nat 38.
     144definition C_cost16 := costlabel_of_nat 30.
     145definition C_cost14 := costlabel_of_nat 29.
     146definition C_cost12 := costlabel_of_nat 28.
     147definition C_cost13 := costlabel_of_nat 27.
     148definition C_cost10 := costlabel_of_nat 26.
     149definition C_cost11 := costlabel_of_nat 25.
     150definition C_cost8 := costlabel_of_nat 24.
     151definition C_cost9 := costlabel_of_nat 23.
     152definition C_cost15 := costlabel_of_nat 22.
     153definition f_search := Internal ? (mk_internal_function
     154  (Some ? (ASTint I8 Unsigned))
     155  [pair ?? id_search_tab (ASTptr Any); pair ?? id_search_size (ASTint I8 Unsigned); pair ?? id_search_to_find (ASTint I8 Unsigned)]
     156  [pair ?? id_search__tmp4 (ASTint I32 Signed); pair ?? id_search_high (ASTint I8 Unsigned); pair ?? id_search_i (ASTint I8 Unsigned); pair ?? id_search_low (ASTint I8 Unsigned); pair ?? id_search__tmp_1 (ASTint I32 Signed)]
     157  0 (
     158  St_cost C_cost16 (
     159  St_seq (
     160    St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     161  ) (
     162  St_seq (
     163    St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_size)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
     164  ) (
     165  St_seq (
     166    St_seq (
     167      St_block (
     168        St_loop (
     169          St_seq (
     170            St_ifthenelse I32 Signed (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onotbool (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cge) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_low)))) (
     171              St_exit 0
     172            ) (
     173              St_skip            )
     174          ) (
     175          St_block (
     176            St_cost C_cost14 (
     177            St_seq (
     178              St_seq (
     179                St_call (Some ? id_search__tmp_1) (Cst ? (Oaddrsymbol id__div32s 0)) [dp ?? (ASTint I32 Signed) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_high)) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_low))); dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))))]
     180              ) (
     181              St_assign (ASTint I32 Signed) id_search__tmp4 (Id (ASTint I32 Signed) id_search__tmp_1)
     182              )
     183            ) (
     184            St_seq (
     185              St_assign (ASTint I8 Unsigned) id_search_i (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Id (ASTint I32 Signed) id_search__tmp4))
     186            ) (
     187            St_seq (
     188              St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Ceq) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_to_find))) (
     189                St_cost C_cost12 (
    52190                St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Id (ASTint I8 Unsigned) id_search_i)))
    53191                )
    54192              ) (
    55                 St_cost C_cost5 (
     193                St_cost C_cost13 (
    56194                St_skip                )
    57195              )
    58196            ) (
    59197            St_seq (
    60               St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Cgt) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
    61                 St_cost C_cost2 (
    62                 St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Osub (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))
     198              St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_to_find))) (
     199                St_cost C_cost10 (
     200                St_assign (ASTint I8 Unsigned) id_search_high (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Osub (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    63201                )
    64202              ) (
    65                 St_cost C_cost3 (
     203                St_cost C_cost11 (
    66204                St_skip                )
    67205              )
    68206            ) (
    69             St_ifthenelse I8 Unsigned (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocmpu Clt) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))) (Id (ASTint I8 Unsigned) id_search_to_find)) (
    70               St_cost C_cost0 (
    71               St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (Ocastint Unsigned I8) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Oadd (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1)))))
     207            St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Clt) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Mem (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Unsigned) (ASTptr Any) Oaddp (Id (ASTptr Any) id_search_tab) (Op2 (ASTint I8 Unsigned) (ASTint I8 Unsigned) (ASTint I8 Unsigned) Omul (Id (ASTint I8 Unsigned) id_search_i) (Cst (ASTint I8 Unsigned) (Ointconst I8 (repr ? 1))))))) (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_to_find))) (
     208              St_cost C_cost8 (
     209              St_assign (ASTint I8 Unsigned) id_search_low (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Oadd (Op1 (ASTint I8 Unsigned) (ASTint I32 Signed) (Ocastint Unsigned I32) (Id (ASTint I8 Unsigned) id_search_i)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    72210              )
    73211            ) (
    74               St_cost C_cost1 (
     212              St_cost C_cost9 (
    75213              St_skip              )
     214            )
    76215            )
    77216            )
     
    84223      )
    85224    ) (
    86     St_cost C_cost7 (
     225    St_cost C_cost15 (
    87226    St_skip    )
    88227    )
    89228  ) (
    90   St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op1 (ASTint I8 Signed) (ASTint I8 Signed) Onegint (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))))
     229  St_return (Some ? (dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I32 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Op1 (ASTint I32 Signed) (ASTint I32 Signed) Onegint (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))))
    91230  )
    92231  )
     
    96235)).
    97236
    98 definition id_main := ident_of_nat 16.
    99 definition id_main_res := ident_of_nat 18.
    100 definition id_main__tmp0 := ident_of_nat 19.
    101 definition C_cost9 := costlabel_of_nat 17.
     237definition id_main := ident_of_nat 39.
     238definition id_main_res := ident_of_nat 41.
     239definition id_main__tmp_2 := ident_of_nat 42.
     240definition C_cost17 := costlabel_of_nat 40.
    102241definition f_main := Internal ? (mk_internal_function
    103242  (Some ? (ASTint I32 Signed))
    104243  []
    105   [pair ?? id_main_res (ASTint I8 Unsigned); pair ?? id_main__tmp0 (ASTint I8 Unsigned)]
     244  [pair ?? id_main_res (ASTint I8 Unsigned); pair ?? id_main__tmp_2 (ASTint I8 Unsigned)]
    106245  5 (
    107   St_cost C_cost9 (
    108   St_seq (
    109     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    110   ) (
    111   St_seq (
    112     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 18))))
    113   ) (
    114   St_seq (
    115     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 2))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 23))))
    116   ) (
    117   St_seq (
    118     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 3))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))
    119   ) (
    120   St_seq (
    121     St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 4))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 120))))
     246  St_cost C_cost17 (
     247  St_seq (
     248    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     249  ) (
     250  St_seq (
     251    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 18))))
     252  ) (
     253  St_seq (
     254    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 2))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 23))))
     255  ) (
     256  St_seq (
     257    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 3))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))
     258  ) (
     259  St_seq (
     260    St_store (ASTint I8 Unsigned) Any Mint8unsigned (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 4))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1))))) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 120))))
    122261  ) (
    123262  St_seq (
    124263    St_seq (
    125       St_call (Some ? id_main__tmp0) (Cst ? (Oaddrsymbol id_search 0)) [dp ?? (ASTptr Any) (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 5)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))]
    126     ) (
    127     St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp0)
     264      St_call (Some ? id_main__tmp_2) (Cst ? (Oaddrsymbol id_search 0)) [dp ?? (ASTptr Any) (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 5)))); dp ?? (ASTint I8 Unsigned) (Op1 (ASTint I8 Signed) (ASTint I8 Unsigned) (Ocastint Signed I8) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 57))))]
     265    ) (
     266    St_assign (ASTint I8 Unsigned) id_main_res (Id (ASTint I8 Unsigned) id_main__tmp_2)
    128267    )
    129268  ) (
     
    143282definition myprog : Cminor_program :=
    144283mk_program ?? [
     284  (pair ?? id__div32u f__div32u);
     285  (pair ?? id__div32s f__div32s);
    145286  (pair ?? id_search f_search);
    146287  (pair ?? id_main f_main)
     
    157298include "RTLabs/semantics.ma".
    158299
    159 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
     300example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    160301normalize  (* you can examine the result here *)
    161302@refl
    162303qed.
    163304
     305
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

    r1153 r1197  
    11include "ASM/I8051.ma".
     2include "joint/Joint.ma".
    23include "utilities/BitVectorTrieSet.ma".
    34include "utilities/IdentifierTools.ma".
     
    89definition registers ≝ list register.
    910
    10 inductive ertl_statement: Type[0] ≝
    11   | ertl_st_skip: label → ertl_statement
    12   | ertl_st_comment: String → label → ertl_statement
    13   | ertl_st_cost: costlabel → label → ertl_statement
    14   | ertl_st_get_hdw: register → Register → label → ertl_statement
    15   | ertl_st_set_hdw: Register → register → label → ertl_statement
    16   | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
    17   | ertl_st_new_frame: label → ertl_statement
    18   | ertl_st_del_frame: label → ertl_statement
    19   | ertl_st_frame_size: register → label → ertl_statement
    20   | ertl_st_pop: register → label → ertl_statement
    21   | ertl_st_push: register → label → ertl_statement
    22   | ertl_st_addr: register → register → ident → label → ertl_statement
    23 (* XXX: changed from O'Caml
    24   | ertl_st_addr_h: register → ident → label → ertl_statement
    25   | ertl_st_addr_l: register → ident → label → ertl_statement
    26 *)
    27   | ertl_st_int: register → Byte → label → ertl_statement
    28   | ertl_st_move: register → register → label → ertl_statement
    29   | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    30 (* XXX: changed from O'Caml
    31   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    32   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    33 *)
    34   | ertl_st_op1: Op1 → register → register → label → ertl_statement
    35   | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    36   | ertl_st_clear_carry: label → ertl_statement
    37   | ertl_st_set_carry: label → ertl_statement
    38   | ertl_st_load: register → register → register → label → ertl_statement
    39   | ertl_st_store: register → register → register → label → ertl_statement
    40   | ertl_st_call_id: ident → nat → label → ertl_statement
    41   | ertl_st_cond: register → label → label → ertl_statement
    42   | ertl_st_return: ertl_statement.
     11inductive move_registers: Type[0] ≝
     12  | pseudo: register → move_registers
     13  | hardware: Register → move_registers.
     14                 
     15inductive ertl_statement_extension: Type[0] ≝
     16  | ertl_st_ext_new_frame: label → ertl_statement_extension
     17  | ertl_st_ext_del_frame: label → ertl_statement_extension
     18  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    4319
    44 definition ertl_statement_graph ≝ graph ertl_statement.
     20definition ertl_params: params ≝
     21 mk_params
     22   register register register register
     23     (move_registers × move_registers) register
     24       ertl_statement_extension unit (list register) nat.
    4525
    46 record ertl_internal_function: Type[0] ≝
     26definition ertl_statement ≝ joint_statement ertl_params.
     27
     28definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
     29
     30record ertl_internal_function (globals: list ident): Type[0] ≝
    4731{
    4832  ertl_if_luniverse: universe LabelTag;
     
    5135  ertl_if_locals: registers;
    5236  ertl_if_stacksize: nat;
    53   ertl_if_graph: ertl_statement_graph;
     37  ertl_if_graph: ertl_statement_graph globals;
    5438  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    5539  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    5640}.
    5741
    58 definition ertl_function ≝ fundef ertl_internal_function.
     42definition set_luniverse ≝
     43  λglobals  : list ident.
     44  λint_fun  : ertl_internal_function globals.
     45  λluniverse: universe LabelTag.
     46  let runiverse ≝ ertl_if_runiverse globals int_fun in
     47  let params    ≝ ertl_if_params globals int_fun in
     48  let locals    ≝ ertl_if_locals globals int_fun in
     49  let stacksize ≝ ertl_if_stacksize globals int_fun in
     50  let graph     ≝ ertl_if_graph globals int_fun in
     51  let entry     ≝ ertl_if_entry globals int_fun in
     52  let exit      ≝ ertl_if_exit globals int_fun in
     53    mk_ertl_internal_function globals
     54      luniverse runiverse params locals
     55      stacksize graph entry exit.
     56
     57definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    5958 
    60 record ertl_program: Type[0] ≝
     59record ertl_program (globals: list ident): Type[0] ≝
    6160{
    6261  ertl_pr_vars: list (ident × nat);
    63   ertl_pr_funcs: list (ident × ertl_function);
     62  ertl_pr_funcs: list (ident × (ertl_function globals));
    6463  ertl_pr_main: option ident
    6564}.
     65
     66
     67(* XXX: changed from O'Caml
     68  | ertl_st_addr_h: register → ident → label → ertl_statement
     69  | ertl_st_addr_l: register → ident → label → ertl_statement
     70*)
     71
     72(* XXX: changed from O'Caml
     73  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     74  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     75*)
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

    r1153 r1197  
    11include "ERTL/ERTL.ma".
    2 include "ERTL/ERTLToLTLI.ma".
    32include "LTL/LTL.ma".
    43include "ERTL/spill.ma".
     4include "ERTL/build.ma".
     5include "utilities/Interference.ma".
     6include "ASM/Arithmetic.ma".
     7
     8(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
     9
     10inductive decision: Type[0] ≝
     11  | decision_spill: Byte → decision
     12  | decision_colour: Register → decision.
     13 
     14definition interference_lookup ≝
     15  λglobals.
     16  λint_fun.
     17  λr.
     18  let 〈liveafter, graph〉 ≝ build globals int_fun in
     19  let lkup ≝ ig_lookup graph r in
     20    vm_find lkup colour_colouring.
     21 
     22definition lookup: register → decision ≝
     23  λr.
     24  match ? r with
     25  [ colour_spill
     26 
     27axiom lookup: register → decision.
     28
     29definition fresh_label ≝
     30  λglobals: list ident.
     31  λluniv.
     32    fresh LabelTag luniv.
     33
     34definition add_graph ≝
     35  λglobals.
     36  λlabel.
     37  λstmt: ltl_statement globals.
     38  λgraph: ltl_statement_graph globals.
     39    add LabelTag ? graph label stmt.
     40
     41definition generate ≝
     42  λglobals: list ident.
     43  λluniv.
     44  λgraph: ltl_statement_graph globals.
     45  λstmt: ltl_statement globals.
     46  let 〈l, luniv〉 ≝ fresh_label globals luniv in
     47  let graph ≝ add_graph globals l stmt graph in
     48    〈l, graph, luniv〉.
     49
     50definition num_locals ≝
     51  λglobals.
     52  λint_fun.
     53    colour_locals + (ertl_if_stacksize globals int_fun).
     54
     55definition stacksize ≝
     56  λglobals.
     57  λint_fun.
     58    colour_locals + (ertl_if_stacksize globals int_fun).
     59
     60definition adjust_off ≝
     61  λglobals.
     62  λint_fun.
     63  λoff.
     64  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
     65  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
     66    sub.
     67
     68definition get_stack:
     69 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
     70  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
     71
     72  λglobals: list ident.
     73  λint_fun.
     74  λgraph: graph (ltl_statement (globals)).
     75  λr.
     76  λoff.
     77  λl.
     78    let off ≝ adjust_off globals int_fun off in
     79    let luniv ≝ ertl_if_luniverse globals int_fun in
     80    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
     81    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     82    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     83    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     84    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     85    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     86    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     87      〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     88
     89definition set_stack:
     90  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
     91    → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝
     92  λglobals: list ident.
     93  λint_fun.
     94  λgraph: graph (ltl_statement (globals)).
     95  λoff.
     96  λr.
     97  λl.
     98  let off ≝ adjust_off globals int_fun off in
     99  let luniv ≝ ertl_if_luniverse globals int_fun in
     100  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
     101  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
     102  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     103  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     104  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     105  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     106  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     107    〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     108
     109definition write:
     110  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
     111    ? ≝
     112  λglobals: list ident.
     113  λint_fun.
     114  λgraph.
     115  λr.
     116  λl.
     117  match lookup r with
     118  [ decision_spill off ⇒
     119    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
     120    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
     121      〈RegisterSST, l, graph, luniv〉
     122  | decision_colour hwr ⇒
     123    let luniv ≝ ertl_if_luniverse globals int_fun in
     124      〈hwr, l, graph, luniv〉
     125  ].
     126
     127definition read:
     128  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
     129    → (Register → ltl_statement globals) → ? ≝
     130  λglobals.
     131  λint_fun.
     132  λgraph.
     133  λr.
     134  λstmt.
     135  match lookup r with
     136  [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
     137  | decision_spill off ⇒
     138    let temphwr ≝ RegisterSST in
     139    let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
     140    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
     141      generate globals luniv graph stmt
     142  ].
     143
     144definition move ≝
     145  λglobals: list ident.
     146  λint_fun.
     147  λgraph: graph (ltl_statement globals).
     148  λdest: decision.
     149  λsrc: decision.
     150  λl: label.
     151  match dest with
     152  [ decision_colour dest_hwr ⇒
     153    match src with
     154    [ decision_colour src_hwr ⇒
     155      let luniv ≝ ertl_if_luniverse globals int_fun in
     156      if eq_Register dest_hwr src_hwr then
     157        〈joint_st_goto … globals l, graph, luniv〉
     158      else
     159        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
     160          〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
     161    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
     162    ]
     163  | decision_spill dest_off ⇒
     164    match src with
     165    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
     166    | decision_spill src_off ⇒
     167      let luniv ≝ ertl_if_luniverse globals int_fun in
     168      if eq_bv ? dest_off src_off then
     169        〈joint_st_goto … globals l, graph, luniv〉
     170      else
     171        let temp_hwr ≝ RegisterSST in
     172        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
     173        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
     174          get_stack globals int_fun graph temp_hwr src_off l
     175    ]
     176  ].
     177
     178definition newframe ≝
     179  λglobals: list ident.
     180  λint_fun: ertl_internal_function globals.
     181  λgraph: ltl_statement_graph globals.
     182  λl: label.
     183  if eq_nat (stacksize globals int_fun) 0 then
     184    〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
     185  else
     186    let luniv ≝ ertl_if_luniverse globals int_fun in
     187    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     188    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     189    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
     190    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
     191    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
     194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     195      〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
     196
     197definition delframe ≝
     198  λglobals.
     199  λint_fun.
     200  λgraph: graph (ltl_statement globals).
     201  λl.
     202  if eq_nat (stacksize globals int_fun) 0 then
     203    〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
     204  else
     205    let luniv ≝ ertl_if_luniverse globals int_fun in
     206    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     207    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     208    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     209    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     210    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     211      〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     212
     213definition translate_statement ≝
     214  λglobals: list ident.
     215  λint_fun.
     216  λgraph: ltl_statement_graph globals.
     217  λstmt: ertl_statement globals.
     218  match stmt with
     219  [ joint_st_sequential seq l ⇒
     220    let luniv ≝ ertl_if_luniverse globals int_fun in
     221    match seq with
     222    [ joint_instr_comment c ⇒
     223      〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
     224    | joint_instr_cost_label cost_lbl ⇒
     225      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     226    | joint_instr_pop r ⇒
     227      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     228      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     229        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
     230    | joint_instr_push r ⇒
     231      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
     232      let int_fun ≝ set_luniverse globals int_fun luniv in
     233      let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     234        〈joint_st_goto ltl_params globals l, graph, luniv〉
     235    | joint_instr_cond srcr lbl_true ⇒
     236      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
     237      let int_fun ≝ set_luniverse globals int_fun luniv in
     238      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     239        〈joint_st_goto ltl_params globals l, graph, luniv〉
     240    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
     241    | joint_instr_store addr1 addr2 srcr ⇒
     242      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
     243      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
     244      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     245      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
     246      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     247      let int_fun ≝ set_luniverse globals int_fun luniv in
     248      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     249      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
     250      let int_fun ≝ set_luniverse globals int_fun luniv in
     251      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     252      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
     253      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     254        〈joint_st_goto ltl_params globals l, graph, luniv〉
     255    | joint_instr_load destr addr1 addr2 ⇒
     256      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     258      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     259      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     260      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
     261      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     262      let int_fun ≝ set_luniverse globals int_fun luniv in
     263      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     264      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
     265      let int_fun ≝ set_luniverse globals int_fun luniv in
     266      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     267        〈joint_st_goto ltl_params globals l, graph, luniv〉
     268    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
     269    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
     270    | joint_instr_op2 op2 destr srcr ⇒
     271      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
     274      let luniv ≝ set_luniverse globals int_fun luniv in
     275      let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     276      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     277      let luniv ≝ set_luniverse globals int_fun luniv in
     278      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     279        〈joint_st_goto ltl_params globals l, graph, luniv〉
     280    | joint_instr_op1 op1 acc_a ⇒
     281      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
     282      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     283      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
     284      let int_fun ≝ set_luniverse globals int_fun luniv in
     285      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     286        〈joint_st_goto ltl_params globals l, graph, luniv〉
     287    | joint_instr_int r i ⇒
     288      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     289        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     290    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
     291      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
     292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
     294      let luniv ≝ set_luniverse globals int_fun luniv in
     295      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     296      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     297      let luniv ≝ set_luniverse globals int_fun luniv in
     298      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     299      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
     300      let luniv ≝ set_luniverse globals int_fun luniv in
     301      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
     302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     303      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
     304      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
     305      let luniv ≝ set_luniverse globals int_fun luniv in
     306      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     307      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     308      let luniv ≝ set_luniverse globals int_fun luniv in
     309      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     310        〈joint_st_goto ltl_params globals l, graph, luniv〉
     311    | joint_instr_move pair_regs ⇒
     312      let regl ≝ \fst pair_regs in
     313      let regr ≝ \snd pair_regs in
     314      match regl with
     315      [ pseudo p1  ⇒
     316        match regr with
     317        [ pseudo p2  ⇒ move globals int_fun graph (lookup p1) (lookup p2) l
     318        | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l
     319        ]
     320      | hardware h1 ⇒
     321        match regr with
     322        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l
     323        | hardware h2 ⇒
     324          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
     325            〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉
     326        ]
     327      ]
     328    | joint_instr_address lbl prf dpl dph ⇒
     329      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in
     330      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
     331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
     332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
     333      let int_fun ≝ set_luniverse globals int_fun luniv in
     334      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in
     335      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
     336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
     337        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     338    ]
     339  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
     340  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     341  | joint_st_extension ext ⇒
     342    match ext with
     343    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
     344    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
     345    | ertl_st_ext_frame_size r l ⇒
     346      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     347        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     348    ]
     349  ].
    5350
    6351definition translate_internal ≝
     352  λglobals: list ident.
    7353  λf.
    8354  λint_fun: ertl_internal_function.
    9 
    10   let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in
    11 
    12   let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in
    13 
    14   let generate stmt =
    15     let l = fresh_label () in
    16     add_graph l stmt ;
    17     l in
    18 
    19   (* Build an interference graph for this function, and color
    20      it. Define a function that allows consulting the coloring. *)
    21 
    22   let module G = struct
    23     let liveafter, graph = Build.build int_fun
    24     let uses = Uses.examine_internal int_fun
    25     let verbose = false
    26     let () =
    27       if verbose then
    28         Printf.printf "Starting hardware register allocation for %s.\n" f
    29   end in
    30 
    31   let module C = Coloring.Color (G) in
    32 
    33   let lookup r =
    34     Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
    35   in
    36 
    37   (* Restrict the interference graph to concern spilled vertices only,
    38      and color it again, this time using stack slots as colors. *)
    39 
    40   let module H = struct
    41     let graph = Interference.droph (Interference.restrict G.graph (fun v ->
    42       match Interference.Vertex.Map.find v C.coloring with
    43       | Coloring.Spill ->
    44           true
    45       | Coloring.Color _ ->
    46           false
    47     ))
    48     let verbose = false
    49     let () =
    50       if verbose then
    51         Printf.printf "Starting stack slot allocation for %s.\n" f
    52   end in
    53 
    54   let module S = Spill.Color (H) in
    55 
    56   (* Define a new function that consults both colorings at once. *)
    57 
    58   let lookup r =
     355  let lookup ≝ λr.
    59356    match lookup r with
    60     | Coloring.Spill ->
     357    | colour_spill ->
    61358        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    62     | Coloring.Color color ->
     359    | colour_colour color ->
    63360        ERTLToLTLI.Color color
    64361  in
    65 
    66   (* We are now ready to instantiate the functor that deals with the
    67      translation of instructions. The reason why we make this a
    68      separate functor is purely pedagogical. Smaller modules are
    69      easier to understand. *)
    70 
    71   (* We add the additional stack size required for spilled register to the stack
    72      size previously required for the function: this is the final stack size
    73      required for the locals. *)
    74 
    75   let locals = S.locals + int_fun.ERTL.f_stacksize in
    76 
    77   (* The full stack size is then the size of the locals in the stack plus the
    78      size of the formal parameters of the function. *)
    79 
    80   let stacksize = int_fun.ERTL.f_params + locals in
    81 
    82   let module I = ERTLToLTLI.Make (struct
    83     let lookup = lookup
    84     let generate = generate
    85     let fresh_label = fresh_label
    86     let add_graph = add_graph
    87     let locals = locals
    88     let stacksize = stacksize
    89   end) in
    90 
    91   (* Translate the instructions in the existing control flow graph.
    92      Pure instructions whose destination pseudo-register is dead are
    93      eliminated on the fly. *)
     362  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
     363  let stacksize ≝ (ertl_if_params int_fun) + locals in
     364    mk_ltl_internal_function
     365      globals
     366      (ertl_if_luniverse int_fun)
     367      (ertl_if_runiverse int_fun)
     368      stacksize.
    94369
    95370  let () =
     
    106381  in
    107382
    108   (* Build a [LTL] function. *)
    109 
    110   {
    111     LTL.f_luniverse = int_fun.ERTL.f_luniverse;
    112     LTL.f_stacksize = stacksize ;
    113     LTL.f_entry = int_fun.ERTL.f_entry;
    114     LTL.f_exit = int_fun.ERTL.f_exit;
    115     LTL.f_graph = !graph
    116   }
    117 
    118383definition translate_funct ≝
    119384  λname_def.
  • Deliverables/D3.3/id-lookup-branch/ERTL/build.ma

    r1153 r1197  
    33
    44definition build ≝
    5   λint_fun: ertl_internal_function.
    6   let liveafter ≝ analyse int_fun in
    7   let graph ≝ ig_create (ertl_if_locals int_fun) in
    8   let graph ≝ ig_mkiph graph (ertl_if_locals int_fun) forbidden_registers in
     5  λglobals: list ident.
     6  λint_fun: ertl_internal_function globals.
     7  let liveafter ≝ analyse globals int_fun in
     8  let graph ≝ ig_create (ertl_if_locals globals int_fun) in
     9  let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in
    910  let graph ≝
    1011    foldi ? ? ? (λlabel. λstmt. λgraph.
    1112      let live ≝ liveafter label in
    12       match eliminable live stmt with
     13      match eliminable globals live stmt with
    1314      [ Some _ ⇒ graph
    1415      | None   ⇒
    15         let defined ≝ defined stmt in
     16        let defined ≝ defined globals stmt in
    1617        let exceptions ≝
    1718          match stmt with
    18           [ ertl_st_move _ sr _    ⇒ lattice_psingleton sr
    19           | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr
    20           | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr
    21           | _                      ⇒ ?
     19          [ joint_st_sequential seq l ⇒
     20            match seq with
     21            [ joint_instr_move pair_reg ⇒
     22              let reg_r ≝ \snd pair_reg in
     23              match reg_r with
     24              [ hardware hw ⇒ lattice_hsingleton hw
     25              | pseudo   ps ⇒ lattice_psingleton ps
     26              ]
     27            | _                         ⇒ ?
     28            ]
     29          | _ ⇒ ?
    2230          ]
    2331        in
     
    2533        let graph ≝
    2634          match stmt with
    27           [ ertl_st_move r1 r2 _    ⇒ ig_mkppp graph r1 r2
    28           | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr
    29           | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr
    30           | _                       ⇒ graph
     35          [ joint_st_sequential seq l ⇒
     36            match seq with
     37            [ joint_instr_move pair_reg ⇒
     38              let reg_l ≝ \fst pair_reg in
     39              let reg_r ≝ \snd pair_reg in
     40              match reg_l with
     41              [ pseudo ps1 ⇒
     42                match reg_r with
     43                [ pseudo ps2  ⇒ ig_mkppp graph ps1 ps2
     44                | hardware hw ⇒ ig_mkpph graph ps1 hw
     45                ]
     46              | hardware hw1 ⇒
     47                match reg_r with
     48                [ pseudo ps    ⇒ ig_mkpph graph ps hw1
     49                | hardware hw2 ⇒ graph
     50                ]
     51              ]
     52            | _ ⇒ graph
     53            ]
     54          | _ ⇒ graph
    3155          ]
    3256        in graph
    33       ]) (ertl_if_graph int_fun) graph
     57      ]) (ertl_if_graph globals int_fun) graph
    3458  in
    3559    〈liveafter, graph〉.
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1153 r1197  
    3535
    3636definition statement_successors ≝
    37   λs: ertl_statement.
     37  λglobals: list ident.
     38  λs: ertl_statement globals.
    3839  match s with
    39   [ ertl_st_return ⇒ [ ]
    40   | ertl_st_skip l ⇒ [ l ]
    41   | ertl_st_comment c l ⇒ [ l ]
    42   | ertl_st_cost c l ⇒ [ l ]
    43   | ertl_st_set_hdw _ _ l ⇒ [ l ]
    44   | ertl_st_get_hdw _ _ l ⇒ [ l ]
    45   | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
    46   | ertl_st_new_frame l ⇒ [ l ]
    47   | ertl_st_del_frame l ⇒ [ l ]
    48   | ertl_st_frame_size _ l ⇒ [ l ]
    49   | ertl_st_push _ l ⇒ [ l ]
    50   | ertl_st_pop _ l ⇒ [ l ]
    51   | ertl_st_addr _ _ _ l ⇒ [ l ]
    52   | ertl_st_int _ _ l ⇒ [ l ]
    53   | ertl_st_move _ _ l ⇒ [ l ]
    54   | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    55   | ertl_st_op1 _ _ _ l ⇒ [ l ]
    56   | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
    57   | ertl_st_clear_carry l ⇒ [ l ]
    58   | ertl_st_set_carry l ⇒ [ l ]
    59   | ertl_st_load _ _ _ l ⇒ [ l ]
    60   | ertl_st_store _ _ _ l ⇒ [ l ]
    61   | ertl_st_call_id _ _ l ⇒ [ l ]
    62   | ertl_st_cond _ l1 l2 ⇒
    63       list_set_add ? (eq_identifier ?) l1 [ l2 ]
     40  [ joint_st_sequential seq l ⇒
     41    match seq with
     42    [ joint_instr_cond acc_a_reg lbl_true ⇒
     43        list_set_add ? (eq_identifier ?) lbl_true [ l ]
     44    | _ ⇒ [ l ]
     45    ]
     46  | joint_st_extension ext ⇒
     47    match ext with
     48    [ ertl_st_ext_new_frame l ⇒ [ l ]
     49    | ertl_st_ext_del_frame l ⇒ [ l ]
     50    | ertl_st_ext_frame_size r l ⇒ [ l ]
     51    ]
     52  | joint_st_goto l ⇒ [ l ]
     53  | joint_st_return ⇒ [ ]
    6454  ].
    6555
     
    122112    lattice_is_maximal.
    123113
    124 definition defined: ertl_statement → register_lattice ≝
    125   λs.
     114definition defined ≝
     115  λglobals: list ident.
     116  λs: ertl_statement globals.
    126117  match s with
    127   [ ertl_st_skip _ ⇒ lattice_bottom
    128   | ertl_st_comment _ _ ⇒ lattice_bottom
    129   | ertl_st_cost _ _ ⇒ lattice_bottom
    130   | ertl_st_push _ _⇒ lattice_bottom
    131   | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    132   | ertl_st_cond _ _ _ ⇒ lattice_bottom
    133   | ertl_st_return ⇒ lattice_bottom
    134   | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    135   | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
    136   | ertl_st_op2 op2 r _ _ _ ⇒
    137     match op2 with
    138     [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    139     | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    140     | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    141     | _ ⇒ lattice_psingleton r
    142     ]
    143   | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
    144   | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
    145   | ertl_st_frame_size r _ ⇒ lattice_psingleton r
    146   | ertl_st_pop r _ ⇒ lattice_psingleton r
    147   | ertl_st_int r _ _ ⇒ lattice_psingleton r
    148   | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    149   | ertl_st_move r _ _ ⇒ lattice_psingleton r
    150   (* XXX: change from o'caml *)
    151   | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    152   | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    153   | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
    154   | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
    155   (* Potentially destroys all caller-save hardware registers. *)
    156   | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
    157   | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    158   | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     118  [ joint_st_sequential seq l ⇒
     119    match seq with
     120    [ joint_instr_op2 op2 r _ ⇒
     121      match op2 with
     122      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     123      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     124      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     125      | _ ⇒ lattice_psingleton r
     126      ]
     127    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
     128    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
     129    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     130    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     131    | joint_instr_pop r ⇒ lattice_psingleton r
     132    | joint_instr_int r _ ⇒ lattice_psingleton r
     133    | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     134    | joint_instr_load r _ _ ⇒ lattice_psingleton r
     135    (* Potentially destroys all caller-save hardware registers. *)
     136    | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     137    | joint_instr_comment c ⇒ lattice_bottom
     138    | joint_instr_cond r lbl_true ⇒ lattice_bottom
     139    | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
     140    | joint_instr_cost_label clabel ⇒ lattice_bottom
     141    | joint_instr_push r ⇒ lattice_bottom
     142    | joint_instr_move pair_reg ⇒
     143      (* first register relevant only *)
     144      let r1 ≝ \fst pair_reg in
     145      match r1 with
     146      [ pseudo p ⇒ lattice_psingleton p
     147      | hardware h ⇒ lattice_hsingleton h
     148      ]
     149    ]
     150  | joint_st_return ⇒ lattice_bottom
     151  | joint_st_extension ext ⇒
     152    match ext with
     153    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     154    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     155    | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
     156    ]
     157  | joint_st_goto l ⇒ lattice_bottom
    159158  ].
    160159
     
    169168definition ret_regs ≝ list_set_of_list RegisterRets.
    170169
    171 definition used: ertl_statement → register_lattice ≝
    172   λstmt.
    173   match stmt with
    174   [ ertl_st_skip _ ⇒ lattice_bottom
    175   | ertl_st_cost _ _ ⇒ lattice_bottom
    176   | ertl_st_comment _ _ ⇒ lattice_bottom
    177   | ertl_st_frame_size _ _ ⇒ lattice_bottom
    178   | ertl_st_pop _ _ ⇒ lattice_bottom
    179   | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    180   | ertl_st_int _ _ _ ⇒ lattice_bottom
    181   | ertl_st_clear_carry _ ⇒ lattice_bottom
    182   | ertl_st_set_carry _ ⇒ lattice_bottom
     170definition used ≝
     171  λglobals: list ident.
     172  λs: ertl_statement globals.
     173  match s with
     174  [ joint_st_sequential seq l ⇒
     175    match seq with
     176    [ joint_instr_op2 op2 acc_a r ⇒
     177      match op2 with
     178      [ Addc ⇒
     179        lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
     180      | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
     181      ]
     182    | joint_instr_clear_carry ⇒ lattice_bottom
     183    | joint_instr_set_carry ⇒ lattice_bottom
     184    (* acc_a and acc_b *)
     185    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     186    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     187    | joint_instr_pop r ⇒ lattice_bottom
     188    | joint_instr_int r _ ⇒ lattice_bottom
     189    | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
     190    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    183191    (* Reads the hardware registers that are used to pass parameters. *)
    184   | ertl_st_call_id _ nparams _ ⇒
    185     〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    186   | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    187   | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
    188   | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
    189   | ertl_st_push r _ ⇒ lattice_psingleton r
    190   | ertl_st_move _ r _ ⇒ lattice_psingleton r
    191   | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
    192   | ertl_st_cond r _ _ ⇒ lattice_psingleton r
    193   | ertl_st_op2 op2 _ r1 r2 _ ⇒
    194     match op2 with
    195     [ Addc ⇒
    196       lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
    197     | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    198     ]
    199   | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    200   | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    201   | ertl_st_store r1 r2 r3 _ ⇒
    202     lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
    203   | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    204   | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    205   | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    206   ].
    207 
    208 definition eliminable: register_lattice → ertl_statement → option label ≝
    209   λl.
    210   λstmt.
     192    | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉
     193    | joint_instr_comment c ⇒ lattice_bottom
     194    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
     195    | joint_instr_store acc_a dpl dph ⇒
     196      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
     197    | joint_instr_cost_label clabel ⇒ lattice_bottom
     198    | joint_instr_push r ⇒ lattice_psingleton r
     199    | joint_instr_move pair_reg ⇒
     200      (* only second reg in pair relevant *)
     201      let r2 ≝ \snd pair_reg in
     202      match r2 with
     203      [ pseudo p ⇒ lattice_psingleton p
     204      | hardware h ⇒ lattice_hsingleton h
     205      ]
     206    ]
     207  | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     208  | joint_st_goto l ⇒ lattice_bottom
     209  | joint_st_extension ext ⇒
     210    match ext with
     211    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     212    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     213    | ertl_st_ext_frame_size r l ⇒ lattice_bottom
     214    ]
     215  ].
     216
     217definition eliminable ≝
     218  λglobals: list ident.
     219  λl: register_lattice.
     220  λs: ertl_statement globals.
    211221  let 〈pliveafter, hliveafter〉 ≝ l in
    212   match stmt with
    213   [ ertl_st_skip _ ⇒ None ?
    214   | ertl_st_comment _ _ ⇒ None ?
    215   | ertl_st_cost _ _ ⇒ None ?
    216   | ertl_st_new_frame _ ⇒ None ?
    217   | ertl_st_del_frame _ ⇒ None ?
    218   | ertl_st_pop _ _ ⇒ None ?
    219   | ertl_st_push _ _ ⇒ None ?
    220   | ertl_st_clear_carry _  ⇒ None ?
    221   | ertl_st_set_carry _  ⇒ None ?
    222   | ertl_st_store _ _ _ _ ⇒ None ?
    223   | ertl_st_call_id _ _ _ ⇒ None ?
    224   | ertl_st_cond _ _ _ ⇒ None ?
    225   | ertl_st_return ⇒ None ?
    226   | ertl_st_get_hdw r _ l ⇒
    227     if list_set_member register (eq_identifier ?) r pliveafter ∨
    228        list_set_member Register eq_Register RegisterCarry hliveafter then
    229       None ?
    230     else
    231       Some ? l
    232   | ertl_st_frame_size r l ⇒
    233     if list_set_member register (eq_identifier ?) r pliveafter ∨
    234        list_set_member Register eq_Register RegisterCarry hliveafter then
    235       None ?
    236     else
    237       Some ? l
    238   | ertl_st_int r _ l ⇒
    239     if list_set_member register (eq_identifier ?) r pliveafter ∨
    240        list_set_member Register eq_Register RegisterCarry hliveafter then
    241       None ?
    242     else
    243       Some ? l
    244   | ertl_st_addr r1 r2 _ l ⇒
    245     if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    246        list_set_member register (eq_identifier ?) r2 pliveafter ∨
    247        list_set_member Register eq_Register RegisterCarry hliveafter then
    248       None ?
    249     else
    250       Some ? l
    251   | ertl_st_move r _ l ⇒
    252     if list_set_member register (eq_identifier ?) r pliveafter ∨
    253        list_set_member Register eq_Register RegisterCarry hliveafter then
    254       None ?
    255     else
    256       Some ? l
    257   | ertl_st_opaccs _ d1 d2 _ _ l ⇒
    258     if list_set_member register (eq_identifier ?) d1 pliveafter ∨
    259        list_set_member register (eq_identifier ?) d2 pliveafter ∨
    260        list_set_member Register eq_Register RegisterCarry hliveafter then
    261       None ?
    262     else
    263       Some ? l
    264   | ertl_st_op1 _ r _ l ⇒
    265     if list_set_member register (eq_identifier ?) r pliveafter ∨
    266        list_set_member Register eq_Register RegisterCarry hliveafter then
    267       None ?
    268     else
    269       Some ? l
    270   | ertl_st_op2 _ r _ _ l ⇒
    271     if list_set_member register (eq_identifier ?) r pliveafter ∨
    272        list_set_member Register eq_Register RegisterCarry hliveafter then
    273       None ?
    274     else
    275       Some ? l
    276   | ertl_st_load r _ _ l ⇒
    277     if list_set_member register (eq_identifier ?) r pliveafter ∨
    278        list_set_member Register eq_Register RegisterCarry hliveafter then
    279       None ?
    280     else
    281       Some ? l
    282   | ertl_st_set_hdw r _ l ⇒
    283     if list_set_member Register eq_Register r hliveafter then
    284       None ?
    285     else
    286       Some ? l
    287   | ertl_st_hdw_to_hdw r _ l ⇒
    288     if list_set_member Register eq_Register r hliveafter then
    289       None ?
    290     else
    291       Some ? l
    292   ].
    293 
    294 definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
     222  match s with
     223  [ joint_st_sequential seq l ⇒
     224    match seq with
     225    [ joint_instr_op2 op2 acc_a r ⇒
     226      if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
     227         list_set_member Register eq_Register RegisterCarry hliveafter then
     228        None ?
     229      else
     230        Some ? l
     231    | joint_instr_clear_carry ⇒ None ?
     232    | joint_instr_set_carry ⇒ None ?
     233    | joint_instr_opaccs opaccs r1 r2 ⇒
     234      if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     235         list_set_member register (eq_identifier ?) r2 pliveafter ∨
     236         list_set_member Register eq_Register RegisterCarry hliveafter then
     237        None ?
     238      else
     239        Some ? l
     240    | joint_instr_op1 op1 r ⇒
     241      if list_set_member register (eq_identifier ?) r pliveafter ∨
     242         list_set_member Register eq_Register RegisterCarry hliveafter then
     243        None ?
     244      else
     245        Some ? l
     246    | joint_instr_pop r ⇒ None ?
     247    | joint_instr_int r _ ⇒
     248      if list_set_member register (eq_identifier ?) r pliveafter ∨
     249         list_set_member Register eq_Register RegisterCarry hliveafter then
     250        None ?
     251      else
     252        Some ? l
     253    | joint_instr_address _ _ r1 r2 ⇒
     254      if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     255         list_set_member register (eq_identifier ?) r2 pliveafter ∨
     256         list_set_member Register eq_Register RegisterCarry hliveafter then
     257        None ?
     258      else
     259        Some ? l
     260    | joint_instr_load acc_a dpl dph ⇒
     261      if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
     262         list_set_member Register eq_Register RegisterCarry hliveafter then
     263        None ?
     264      else
     265        Some ? l
     266    | joint_instr_call_id _ nparams ⇒ None ?
     267    | joint_instr_comment c ⇒ None ?
     268    | joint_instr_cond r lbl_true ⇒ None ?
     269    | joint_instr_store acc_a dpl dph ⇒ None ?
     270    | joint_instr_cost_label clabel ⇒ None ?
     271    | joint_instr_push r ⇒ None ?
     272    | joint_instr_move pair_reg ⇒
     273      let r1 ≝ \fst pair_reg in
     274      let r2 ≝ \snd pair_reg in
     275      match r1 with
     276      [ pseudo p1 ⇒
     277        if list_set_member register (eq_identifier ?) p1 pliveafter ∨
     278           list_set_member Register eq_Register RegisterCarry hliveafter then
     279          None ?
     280        else
     281          Some ? l
     282      | hardware h1 ⇒
     283        if list_set_member Register eq_Register h1 hliveafter then
     284          None ?
     285        else
     286          Some ? l
     287      ]
     288    ]
     289  | joint_st_goto l ⇒ None ?
     290  | joint_st_return ⇒ None ?
     291  | joint_st_extension ext ⇒
     292    match ext with
     293    [ ertl_st_ext_new_frame l ⇒ None ?
     294    | ertl_st_ext_del_frame l ⇒ None ?
     295    | ertl_st_ext_frame_size r l ⇒
     296      if list_set_member register (eq_identifier ?) r pliveafter ∨
     297        list_set_member Register eq_Register RegisterCarry hliveafter then
     298        None ?
     299      else
     300        Some ? l
     301    ]
     302  ].
     303
     304definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
     305  λglobals.
    295306  λstmt.
    296307  λliveafter.
    297   match eliminable liveafter stmt with
    298   [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
     308  match eliminable globals liveafter stmt with
     309  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
    299310  | Some l ⇒ liveafter
    300311  ].
     
    307318
    308319definition livebefore ≝
     320  λglobals: list ident.
    309321  λint_fun.
    310322  λlabel.
    311323  λliveafter: valuation.
    312   match lookup ? ? (ertl_if_graph int_fun) label with
     324  match lookup ? ? (ertl_if_graph globals int_fun) label with
    313325  [ None      ⇒ ?
    314   | Some stmt ⇒ statement_semantics stmt (liveafter label)
     326  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
    315327  ].
    316328  cases not_implemented (* XXX *)
     
    318330
    319331definition liveafter ≝
     332  λglobals.
    320333  λint_fun.
    321334  λlivebefore.
    322335  λlabel.
    323336  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph int_fun) label with
     337  match lookup … (ertl_if_graph globals int_fun) label with
    325338  [ None      ⇒ ?
    326   | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     339  | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
    327340      lattice_join (livebefore successor liveafter) accu)
    328       lattice_bottom (statement_successors stmt)
     341      lattice_bottom (statement_successors globals stmt)
    329342  ].
    330343  cases not_implemented (* XXX *)
    331344qed.
    332345
    333 definition analyse: ertl_internal_function → valuation ≝
     346definition analyse ≝
     347  λglobals.
    334348  λint_fun.
    335     fix_lfp (liveafter int_fun (livebefore int_fun)).
     349    fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).
  • Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

    r1153 r1197  
    2121(* CSC: ???????????? *)
    2222axiom smerge: val → val → res val.
    23 (*
    2423(* CSC: ???????????? In OCaml: IntValue.Int32.merge
    2524   Note also that the translation can fail; so it should be a res int! *)
    2625axiom smerge2: list val → int.
    27 *)
    2826(* CSC: I have a byte, I need a value, but it is complex to do so *)
    2927axiom val_of_Byte: Byte → val.
    3028axiom Byte_of_val: val → res Byte.
     29axiom val_of_nat: nat → val.
    3130(* Map from the front-end memory model to the back-end memory model *)
    3231axiom represent_block: block → val × val.
     
    3837axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    3938axiom address_of_val: val → address. (* CSC: only to shift the sp *)
     39axiom addr_sub: address → nat → address.
     40axiom addr_add: address → nat → address.
    4041(* CSC: ??? *)
    4142axiom address_of_label: mem → label → address.
     
    4344axiom label_of_address_chunks: Byte → Byte → label.
    4445axiom address_of_address_chunks: Byte → Byte → address.
     46axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    4547axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    4648axiom hwreg_retrieve : mRegisterMap → Register → res val.
    4749axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    4850
    49 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
    5052
    5153(* CSC: frame reduced to this *)
    5254definition frame: Type[0] ≝ register_env val.
    5355
     56(* CSC: exit not put in the state, like in OCaml. It is constant througout
     57   execution *)
    5458record state : Type[0] ≝
    5559 { st_frms: list frame
    5660 ; pc: address
    5761 ; sp: address
    58 (* ; exit: address *)
    5962 ; locals: register_env val
    6063 ; carry: val
     
    134137
    135138(*CSC: To be implemented *)
    136 axiom fetch_statement: state → res ertl_statement.
     139
     140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
     141axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
    137142
    138143definition init_locals : list register → register_env val ≝
     
    142147λreg,v,locals. update RegisterTag val locals reg v.
    143148
    144 (*
    145 axiom WrongNumberOfParameters : String.
    146 
    147 (* CSC: modified to take in input a list of registers (untyped) *)
    148 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    149 match rs with
    150 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    151 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    152   let locals' ≝ add RegisterTag val locals r v in
    153   params_store rst vst locals'
    154 ] ].
    155 *)
    156 
    157149axiom BadRegister : String.
    158150
     
    160152λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    161153
    162 (*
    163 axiom FailedOp : String.
    164 *)
    165154axiom MissingSymbol : String.
    166 (*
    167 axiom MissingStatement : String.
    168 axiom FailedConstant : String. *)
    169155axiom FailedLoad : String.
    170156axiom BadFunction : String.
    171 (*axiom BadJumpTable : String.
    172 axiom BadJumpValue : String.
    173 axiom FinalState : String.
    174 axiom ReturnMismatch : String.
    175 *)
    176157
    177158(*CSC: to be implemented *)
     
    200181  (λregs.OK ? (set_regs regs st)).
    201182
    202 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    203 λge,st.
    204   ! s ← fetch_statement st;
     183definition fetch_result: state → nat → res (list val) ≝
     184 λst,registersno.
     185  let retregs ≝ prefix … registersno RegisterRets in
     186  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
     187
     188definition framesize: list ident → state → res nat ≝
     189  λglobals: list ident.
     190  λst.
     191  (* CSC: monadic notation missing here *)
     192    bind ?? (fetch_function globals st) (λf.
     193    OK ? (ertl_if_stacksize globals f)).
     194
     195definition get_hwsp : state → res address ≝
     196 λst.
     197  (* CSC: monadic notation missing here *)
     198  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
     199  (* CSC: monadic notation missing here *)
     200  bind ?? (Byte_of_val spl) (λspl.
     201  (* CSC: monadic notation missing here *)
     202  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
     203  (* CSC: monadic notation missing here *)
     204  bind ?? (Byte_of_val sph) (λsph.
     205  OK ? (address_of_address_chunks spl sph))))).
     206
     207definition set_hwsp : address → state → res state ≝
     208 λsp,st.
     209  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
     210  (* CSC: monadic notation missing here *) 
     211  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
     212  (* CSC: monadic notation missing here *) 
     213  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
     214  OK ? (set_regs regs st))).
     215
     216definition retrieve: state → move_registers → res val ≝
     217  λst.
     218  λr.
     219  match r with
     220  [ pseudo   src ⇒ reg_retrieve (locals st) src
     221  | hardware src ⇒ hwreg_retrieve (regs st) src
     222  ].
     223
     224definition store ≝
     225  λst.
     226  λv.
     227  λr.
     228  match r with
     229  [ pseudo   dst ⇒
     230    ! locals ← reg_store dst v (locals st);
     231      ret ? (set_locals locals st)
     232  | hardware dst ⇒
     233    ! regs ← hwreg_store dst v (regs st);
     234      ret ? (set_regs regs st)
     235  ].
     236
     237definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
     238  λglobals. λge,st.
     239  ! s ← fetch_statement globals st;
    205240  match s with
    206   [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
    207   | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
    208   | ertl_st_int dest v l ⇒
    209      ! locals ← reg_store dest (val_of_Byte v) (locals st);
    210      ret ? 〈E0, goto l (set_locals locals st)〉
    211   | ertl_st_load addrl addrh dst l ⇒
    212       ! vaddrh ← reg_retrieve (locals st) addrh;
    213       ! vaddrl ← reg_retrieve (locals st) addrl;
    214       ! vaddr ← smerge vaddrl vaddrh;
    215       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    216       ! locals ← reg_store dst v (locals st);
     241  [ ertl_st_lift_pre pre ⇒
     242    match pre with
     243    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
     244    | joint_st_sequential seq l ⇒
     245      match seq with
     246      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
     247      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
     248      | joint_instr_int dest v ⇒
     249        ! locals ← reg_store dest (val_of_Byte v) (locals st);
     250          ret ? 〈E0, goto l (set_locals locals st)〉
     251      | joint_instr_load addrl addrh dst ⇒
     252        ! vaddrh ← reg_retrieve (locals st) addrh;
     253        ! vaddrl ← reg_retrieve (locals st) addrl;
     254        ! vaddr ← smerge vaddrl vaddrh;
     255        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
     256        ! locals ← reg_store dst v (locals st);
     257          ret ? 〈E0, goto l (set_locals locals st)〉
     258      | joint_instr_store addrl addrh src ⇒
     259        ! vaddrh ← reg_retrieve (locals st) addrh;
     260        ! vaddrl ← reg_retrieve (locals st) addrl;
     261        ! vaddr ← smerge vaddrl vaddrh;
     262        ! v ← reg_retrieve (locals st) src;
     263        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
     264          ret ? 〈E0, goto l (set_m m' st)〉
     265      | joint_instr_cond src ltrue ⇒
     266        ! v ← reg_retrieve (locals st) src;
     267        ! b ← eval_bool_of_val v;
     268          ret ? 〈E0, goto (if b then ltrue else l) st〉
     269      | joint_instr_address ident prf ldest hdest ⇒
     270        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     271          let 〈laddr,haddr〉 ≝ represent_block addr in
     272        ! locals ← reg_store ldest laddr (locals st);
     273        ! locals ← reg_store hdest haddr locals;
     274          ret ? 〈E0, goto l (set_locals locals st)〉
     275      | joint_instr_op1 op acc_a ⇒
     276        ! v ← reg_retrieve (locals st) acc_a;
     277        ! v ← Byte_of_val v;
     278          let v' ≝ val_of_Byte (op1 eval op v) in
     279        ! locals ← reg_store acc_a v' (locals st);
     280          ret ? 〈E0, goto l (set_locals locals st)〉
     281      | joint_instr_op2 op acc_a_reg dest ⇒
     282        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     283        ! v1 ← Byte_of_val v1;
     284        ! v2 ← reg_retrieve (locals st) acc_a_reg;
     285        ! v2 ← Byte_of_val v2;
     286        ! carry ← eval_bool_of_val (carry st);
     287          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     288          let v' ≝ val_of_Byte v' in
     289          let carry ≝ of_bool carry in
     290        ! locals ← reg_store dest v' (locals st);
     291          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
     292      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
     293      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
     294      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
     295        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     296        ! v1 ← Byte_of_val v1;
     297        ! v2 ← reg_retrieve (locals st) acc_b_reg;
     298        ! v2 ← Byte_of_val v2;
     299          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     300          let v1' ≝ val_of_Byte v1' in
     301          let v2' ≝ val_of_Byte v2' in
     302        ! locals ← reg_store acc_a_reg v1' (locals st);
     303        ! locals ← reg_store acc_b_reg v2' locals;
     304          ret ? 〈E0, goto l (set_locals locals st)〉
     305      | joint_instr_pop dst ⇒
     306        ! 〈st,v〉 ← pop st;
     307        ! locals ← reg_store dst (val_of_Byte v) (locals st);
     308          ret ? 〈E0, goto l (set_locals locals st)〉
     309      | joint_instr_push src ⇒
     310        ! v ← reg_retrieve (locals st) src;
     311        ! v ← Byte_of_val v;
     312        ! st ← push st v;
     313          ret ? 〈E0, goto l st〉
     314      | joint_instr_move dst_src ⇒
     315        let 〈dst, src〉 ≝ dst_src in
     316        ! v ← retrieve st src;
     317        ! st ← store st v dst;
     318          ret ? 〈E0, goto l st〉
     319      (* CSC: changed, where the meat is *)
     320      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     321        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     322        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     323          match fd with
     324          [ Internal fn ⇒
     325            ! st ← save_ra st l;
     326              let st ≝ save_frame st in
     327              let locals ≝ init_locals (ertl_if_locals globals fn) in
     328              let l' ≝ ertl_if_entry globals fn in
     329              ret ? 〈 E0, goto l' (set_locals locals st)〉
     330          | External fn ⇒
     331            ! params ← fetch_external_args fn st;
     332            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     333            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     334            (* CSC: XXX bug here; I think I should split it into Byte-long
     335               components; instead I am making a singleton out of it *)
     336              let vs ≝ [mk_val ? evres] in
     337            ! st ← set_result vs st;
     338              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     339          ]
     340      ]
     341    (* CSC: changed, where the meat is *)
     342    | joint_st_return ⇒
     343      ! st ← pop_frame st;
     344      ! 〈st,pch〉 ← pop st;
     345      ! 〈st,pcl〉 ← pop st;
     346        let pc ≝ address_of_address_chunks pcl pch in
     347        ret ? 〈E0,set_pc pc st〉
     348    | _ ⇒ ?
     349    ]
     350  | ertl_st_new_frame l ⇒
     351    ! v ← framesize globals st;
     352    ! sp ← get_hwsp st;
     353      let newsp ≝ addr_sub sp v in
     354    ! st ← set_hwsp newsp st;
     355      ret ? 〈E0,goto l st〉
     356  | ertl_st_del_frame l ⇒
     357    ! v ← framesize globals st;
     358    ! sp ← get_hwsp st;
     359      let newsp ≝ addr_add sp v in
     360    ! st ← set_hwsp newsp st;
     361      ret ? 〈E0,goto l st〉
     362  | ertl_st_frame_size dst l ⇒
     363    ! v ← framesize globals st;
     364    ! locals ← reg_store dst (val_of_nat v) (locals st);
    217365      ret ? 〈E0, goto l (set_locals locals st)〉
    218   | ertl_st_store addrl addrh src l ⇒
    219       ! vaddrh ← reg_retrieve (locals st) addrh;
    220       ! vaddrl ← reg_retrieve (locals st) addrl;
    221       ! vaddr ← smerge vaddrl vaddrh;
    222       ! v ← reg_retrieve (locals st) src;
    223       ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    224       ret ? 〈E0, goto l (set_m m' st)〉
    225   | ertl_st_cond src ltrue lfalse ⇒
    226       ! v ← reg_retrieve (locals st) src;
    227       ! b ← eval_bool_of_val v;
    228       ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
    229   | ertl_st_addr ldest hdest id l ⇒
    230      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    231      let 〈laddr,haddr〉 ≝ represent_block addr in
    232      ! locals ← reg_store ldest laddr (locals st);
    233      ! locals ← reg_store hdest haddr locals;
    234      ret ? 〈E0, goto l (set_locals locals st)〉
    235   | ertl_st_op1 op dst src l ⇒
    236      ! v ← reg_retrieve (locals st) src;
    237      ! v ← Byte_of_val v;
    238      let v' ≝ val_of_Byte (op1 eval op v) in
    239      ! locals ← reg_store dst v' (locals st);
    240      ret ? 〈E0, goto l (set_locals locals st)〉
    241   | ertl_st_op2 op dst src1 src2 l ⇒
    242      ! v1 ← reg_retrieve (locals st) src1;
    243      ! v1 ← Byte_of_val v1;
    244      ! v2 ← reg_retrieve (locals st) src2;
    245      ! v2 ← Byte_of_val v2;
    246      ! carry ← eval_bool_of_val (carry st);
    247      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    248      let v' ≝ val_of_Byte v' in
    249      let carry ≝ of_bool carry in
    250      ! locals ← reg_store dst v' (locals st);
    251      ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    252   | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    253      ! v1 ← reg_retrieve (locals st) sacc;
    254      ! v1 ← Byte_of_val v1;
    255      ! v2 ← reg_retrieve (locals st) sbacc;
    256      ! v2 ← Byte_of_val v2;
    257      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    258      let v1' ≝ val_of_Byte v1' in
    259      let v2' ≝ val_of_Byte v2' in
    260      ! locals ← reg_store dacc v1' (locals st);
    261      ! locals ← reg_store dbacc v2' locals;
    262      ret ? 〈E0, goto l (set_locals locals st)〉
    263   | ertl_st_clear_carry l ⇒
    264     ret ? 〈E0, goto l (set_carry Vfalse st)〉
    265   | ertl_st_set_carry l ⇒
    266     ret ? 〈E0, goto l (set_carry Vtrue st)〉
    267      
    268   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    269          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    270          be more than enough... *)
    271   | ertl_st_move dst src l ⇒
    272      ! v ← reg_retrieve (locals st) src;
    273      ! locals ← reg_store dst v (locals st);
    274      ret ? 〈E0, goto l (set_locals locals st)〉
    275   | ertl_st_hdw_to_hdw dst src l ⇒
    276      ! v ← hwreg_retrieve (regs st) src;
    277      ! regs ← hwreg_store dst v (regs st);
    278      ret ? 〈E0, goto l (set_regs regs st)〉
    279   | ertl_st_get_hdw dst src l ⇒
    280      ! v ← hwreg_retrieve (regs st) src;
    281      ! locals ← reg_store dst v (locals st);
    282      ret ? 〈E0, goto l (set_locals locals st)〉
    283   | ertl_st_set_hdw dst src l ⇒
    284      ! v ← reg_retrieve (locals st) src;
    285      ! regs ← hwreg_store dst v (regs st);
    286      ret ? 〈E0, goto l (set_regs regs st)〉
    287 
    288366  (* CSC: Dropped:
    289367      - rtl_st_stackaddr (becomes two get_hdw)
    290368      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    291369      - rtl_st_call_ptr (unimplemented ATM) *)
     370  ].
    292371     
    293   (* CSC: changed, where the meat is *)
    294   | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
    295       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    296       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    297       match fd with
    298       [ Internal fn ⇒
    299         ! st ← save_ra st l;
    300         let st ≝ save_frame st in
    301         let locals ≝ init_locals (ertl_if_locals fn) in
    302         let l' ≝ ertl_if_entry fn in
    303          ret ? 〈 E0, goto l' (set_locals locals st)〉
    304       | External fn ⇒
    305         ! params ← fetch_external_args fn st;
    306         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    307         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    308         (* CSC: XXX bug here; I think I should split it into Byte-long
    309            components; instead I am making a singleton out of it *)
    310         let vs ≝ [mk_val ? evres] in
    311         ! st ← set_result vs st;
    312         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     372axiom WrongReturnValueType: String.
     373
     374definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
     375  λglobals: list ident.
     376  λexit.
     377  λregistersno.
     378  λst.
     379 (* CSC: monadic notation missing here *)
     380  match fetch_statement globals st with
     381  [ Error _ ⇒ None ?
     382  | OK s ⇒
     383    match s with
     384    [ ertl_st_lift_pre pre ⇒
     385      match pre with
     386      [ joint_st_return ⇒
     387        match fetch_ra st with
     388         [ Error _ ⇒ None ?
     389         | OK st_l ⇒
     390           let 〈st,l〉 ≝ st_l in
     391           match label_eq l exit with
     392           [ inl _ ⇒
     393             (* CSC: monadic notation missing here *)
     394             match fetch_result st registersno with
     395             [ Error _ ⇒ None ?
     396             | OK vals ⇒ Some ? (smerge2 vals)
     397             ]
     398           | inr _ ⇒ None ?
     399           ]
     400         ]
     401      | _ ⇒ None ?
    313402      ]
    314   | ertl_st_return ⇒
    315       ! st ← pop_frame st;
    316       ! 〈st,pch〉 ← pop st;
    317       ! 〈st,pcl〉 ← pop st;
    318       let pc ≝ address_of_address_chunks pcl pch in
    319       ret ? 〈E0,set_pc pc st〉
    320  
    321   (* CSC: new stuff *)
    322   | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    323   | ertl_st_new_frame _ ⇒ ?
    324   | ertl_st_del_frame _ ⇒ ?
    325   | ertl_st_frame_size _ _ ⇒ ?
    326   | ertl_st_pop dst l ⇒
    327      ! 〈st,v〉 ← pop st;
    328      ! locals ← reg_store dst (val_of_Byte v) (locals st);
    329      ret ? 〈E0, goto l (set_locals locals st)〉
    330   | ertl_st_push src l ⇒
    331      ! v ← reg_retrieve (locals st) src;
    332      ! v ← Byte_of_val v;
    333      ! st ← push st v;
    334      ret ? 〈E0, goto l st〉
     403    | _ ⇒ None ?
     404    ]
    335405  ].
    336406
    337 axiom WrongReturnValueType: String.
    338 
    339 definition is_final : state → option ((*CSC: why not res*) int) ≝
    340 λs. match s with
    341 [ State _ _ _ ⇒ None ?
    342 | Callstate _ _ _ _ _ ⇒ None ?
    343 | Returnstate v _ fs _ ⇒
    344     match fs with
    345      [ nil ⇒ Some ? (smerge2 v)
    346      | _ ⇒ None ? ]].
    347 
    348 definition RTL_exec : execstep io_out io_in ≝
    349   mk_execstep … ? is_final mem_of_state eval_statement.
     407definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
     408  λglobals.
     409  λexit.
     410  λregistersno.
     411  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
    350412
    351413(* CSC: XXX the program type does not fit with the globalenv and init_mem
  • Deliverables/D3.3/id-lookup-branch/ERTL/uses.ma

    r1153 r1197  
    1818  λr.
    1919    assoc_list_find register nat (eq_identifier ?) uses 0 r.
    20 
    21 definition count ≝
    22   λr.
    23   λuses.
    24     (r,
    25 
    26 let count r uses = Register.Map.add r (lookup uses r + 1) uses
  • Deliverables/D3.3/id-lookup-branch/LIN/LIN.ma

    r878 r1197  
    1 include "LIN/JointLTLLIN.ma".
    2  
    3 definition pre_lin_statement ≝ joint_statement unit.
     1include "joint/Joint.ma".
     2
     3definition lin_params: params ≝
     4 mk_params
     5   unit unit unit unit registers_move Register
     6     unit unit unit unit.
     7
     8definition pre_lin_statement ≝
     9 λglobals: list ident. joint_statement lin_params globals.
    410
    511definition lin_statement ≝
  • Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma

    r1153 r1197  
    3535      match instr' with
    3636      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3838      | _ ⇒ set_empty ?
    3939      ]
    4040    | joint_st_return ⇒ set_empty ?
    4141    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     42    | joint_st_extension _ ⇒ set_empty ?
    4243    ]
    4344  in
     
    9091  match statement with
    9192  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     93  | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)
    9294  | joint_st_return ⇒ Instruction (RET ?)
    9395  | joint_st_sequential instr _ ⇒
  • Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma

    r1091 r1197  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 include "LIN/LIN.ma".
     3include "joint/Joint.ma".
    44
    5 definition ltl_statement ≝ joint_statement label.
     5definition ltl_params: params ≝
     6 mk_params
     7   unit unit unit unit registers_move Register
     8     unit unit unit unit.
     9
     10definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
    611 
    712definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  • Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma

    r1153 r1197  
    99  λglobals: list ident.
    1010  λs: ltl_statement globals.
    11     match s with
    12     [ joint_st_return ⇒ joint_st_return ? globals
    13     | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
    14     | joint_st_goto l ⇒ joint_st_goto ? globals l
    15     ].
     11  match s with
     12  [ joint_st_return ⇒ joint_st_return lin_params globals
     13  | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
     14  | joint_st_goto l ⇒ joint_st_goto lin_params globals l
     15  | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
     16  ].
    1617   
    1718definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     
    5657    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    5758  if marked l2 visited then
    58     〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
     59    〈require l2 required, (joint_st_goto globals l2) :: generated〉
    5960  else
    6061   visit globals g required visited generated l2 n.
     
    8081      [ joint_st_sequential instr l2 ⇒
    8182        match instr with
    82         [ joint_instr_cond_acc l1 ⇒
     83        [ joint_instr_cond acc_a_reg l1 ⇒
    8384              let required' ≝
    8485                if marked l2 visited' then
     
    104105                required in
    105106            if marked l2 visited' then
    106               〈required', joint_st_goto ? globals l2 :: generated''〉
     107              〈required', joint_st_goto globals l2 :: generated''〉
    107108            else
    108109              visit globals g required' visited' generated'' l2 n'
    109110          ]
    110         | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     111    | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    111112    | joint_st_goto l ⇒
    112        let required' ≝
    113          if marked l visited' then
    114            require l required
    115          else
    116            required
    117        in
    118          if marked l visited' then
    119            〈required', joint_st_goto ? globals l :: generated''〉
    120          else
    121            visit globals g required' visited' generated'' l n'
     113      let required' ≝
     114        if marked l visited' then
     115         require l required
     116        else
     117         required
     118      in
     119        if marked l visited' then
     120          〈required', joint_st_goto … globals l :: generated''〉
     121        else
     122          visit globals g required' visited' generated'' l n'
     123    | joint_st_extension ext ⇒ 〈required, generated〉
    122124    ]
    123125  ]
  • Deliverables/D3.3/id-lookup-branch/RTLabs/RTLabsMatitaPrinter.ml

    r967 r1197  
    1616
    1717let print_global (x, size) =
    18   Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x
     18  Printf.sprintf "pair ?? (pair ?? id_%s Any) %d" x
    1919    (Driver.RTLabsMemory.concrete_size size)
    2020
     
    2525    (MiscPottier.string_of_list (";\n"^n_spaces n) print_global globs)
    2626
     27let print_label l = "lbl_" ^ l
    2728
    2829let rec print_args args =
     
    130131let rec print_table = function
    131132  | [] -> ""
    132   | [lbl] -> lbl
    133   | lbl :: tbl -> lbl ^ "; " ^ (print_table tbl)
     133  | [lbl] -> print_label lbl
     134  | lbl :: tbl -> (print_label lbl) ^ "; " ^ (print_table tbl)
    134135
    135136
    136137let print_statement lookup_type = function
    137   | RTLabs.St_skip lbl -> "make_St_skip " ^ lbl
     138  | RTLabs.St_skip lbl -> "make_St_skip " ^ (print_label lbl)
    138139  | RTLabs.St_cost (cost_lbl, lbl) ->
    139       Printf.sprintf "make_St_cost C%s %s" cost_lbl lbl
     140      Printf.sprintf "make_St_cost C%s %s" cost_lbl (print_label lbl)
    140141  | RTLabs.St_cst (dests, cst, lbl) ->
    141142      Printf.sprintf "make_St_const %s (%s) %s"
    142143        (Register.print dests)
    143144        (print_constant (lookup_type dests) cst)
    144         lbl
     145        (print_label lbl)
    145146  | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
    146147      Printf.sprintf "make_St_op1 %s %s %s %s"
     
    148149        (Register.print dests)
    149150        (Register.print srcs)
    150         lbl
     151        (print_label lbl)
    151152  | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
    152153      Printf.sprintf "make_St_op2 %s %s %s %s %s"
     
    155156        (Register.print srcs1)
    156157        (Register.print srcs2)
    157         lbl
     158        (print_label lbl)
    158159  | RTLabs.St_load (chunk, addr, dests, lbl) ->
    159160      Printf.sprintf "make_St_load %s %s %s %s"
     
    161162        (Register.print addr)
    162163        (Register.print dests)
    163         lbl
     164        (print_label lbl)
    164165  | RTLabs.St_store (chunk, addr, srcs, lbl) ->
    165166      Printf.sprintf "make_St_store %s %s %s %s"
     
    167168        (Register.print addr)
    168169        (Register.print srcs)
    169         lbl
     170        (print_label lbl)
    170171  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    171172      Printf.sprintf "make_St_call_id id_%s %s (%s) %s"
     
    173174        (print_params args)
    174175        (match res with None -> "None ?" | Some res -> "Some ? " ^ Register.print res)
    175         lbl
     176        (print_label lbl)
    176177  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    177178      Printf.sprintf "make_St_call_ptr %s %s (%s) %s"
     
    179180        (print_params args)
    180181        (match res with None -> "None ?" | Some res -> "Some ? " ^ (Register.print res))
    181         lbl
     182        (print_label lbl)
    182183  | RTLabs.St_tailcall_id (f, args, sg) ->
    183184      Printf.sprintf "make_St_tailcall_id id_%s %s"
     
    191192      Printf.sprintf "make_St_cond %s %s %s"
    192193        (Register.print srcs)
    193         lbl_true
    194         lbl_false
     194        (print_label lbl_true)
     195        (print_label lbl_false)
    195196  | RTLabs.St_jumptable (rs, tbl) ->
    196197      Printf.sprintf "make_St_jumptable %s [%s]"
     
    218219    Printf.sprintf "%sdefinition %s := %d.\n%s"
    219220      (n_spaces n)
    220       lbl
     221      (print_label lbl)
    221222      i
    222223      s
     
    228229    Printf.sprintf "%s(pair ?? %s (%s))%s\n%s"
    229230      (n_spaces n)
    230       lbl
     231      (print_label lbl)
    231232      (print_statement lookup_type stmt)
    232233      (if s = "" then "\n]" else ";")
     
    259260    (print_graph (n+2) lookup_type def.RTLabs.f_graph)
    260261    (n_spaces (n+2))
    261     def.RTLabs.f_entry
    262     (n_spaces (n+2))
    263     def.RTLabs.f_exit
     262    (print_label def.RTLabs.f_entry)
     263    (n_spaces (n+2))
     264    (print_label def.RTLabs.f_exit)
    264265
    265266
  • Deliverables/D3.3/id-lookup-branch/RTLabs/test/search.RTLabs.ma

    r967 r1197  
    55
    66
    7   definition id_search := ident_of_nat 0.
    8   definition search9 := 50.
    9   definition search8 := 49.
    10   definition search7 := 48.
    11   definition search6 := 47.
    12   definition search50 := 46.
    13   definition search5 := 45.
    14   definition search49 := 44.
    15   definition search48 := 43.
    16   definition search47 := 42.
    17   definition search46 := 41.
    18   definition search45 := 40.
    19   definition search44 := 39.
    20   definition search43 := 38.
    21   definition search42 := 37.
    22   definition search41 := 36.
    23   definition search40 := 35.
    24   definition search4 := 34.
    25   definition search39 := 33.
    26   definition search38 := 32.
    27   definition search37 := 31.
    28   definition search36 := 30.
    29   definition search35 := 29.
    30   definition search34 := 28.
    31   definition search33 := 27.
    32   definition search32 := 26.
    33   definition search31 := 25.
    34   definition search30 := 24.
    35   definition search3 := 23.
    36   definition search29 := 22.
    37   definition search28 := 21.
    38   definition search27 := 20.
    39   definition search26 := 19.
    40   definition search25 := 18.
    41   definition search24 := 17.
    42   definition search23 := 16.
    43   definition search22 := 15.
    44   definition search21 := 14.
    45   definition search20 := 13.
    46   definition search2 := 12.
    47   definition search19 := 11.
    48   definition search18 := 10.
    49   definition search17 := 9.
    50   definition search16 := 8.
    51   definition search15 := 7.
    52   definition search14 := 6.
    53   definition search13 := 5.
    54   definition search12 := 4.
    55   definition search11 := 3.
    56   definition search10 := 2.
    57   definition search1 := 1.
    58   definition search0 := 0.
    59   definition C_cost1 := costlabel_of_nat 8.
    60   definition C_cost8 := costlabel_of_nat 7.
    61   definition C_cost6 := costlabel_of_nat 6.
    62   definition C_cost7 := costlabel_of_nat 5.
    63   definition C_cost4 := costlabel_of_nat 4.
    64   definition C_cost5 := costlabel_of_nat 3.
    65   definition C_cost2 := costlabel_of_nat 2.
    66   definition C_cost3 := costlabel_of_nat 1.
    67   definition C_cost0 := costlabel_of_nat 0.
    68 
    69 
    70   definition pre_search := mk_pre_internal_function
    71     (Some ? (pair ?? 6 (ASTint I8 Unsigned)))
    72     [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
    73     [(pair ?? 3 (ASTint I8 Unsigned)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTint I8 Signed)); (pair ?? 9 (ASTint I8 Unsigned)); (pair ?? 10 (ASTint I8 Unsigned)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Unsigned)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Unsigned)); (pair ?? 15 (ASTint I8 Unsigned)); (pair ?? 16 (ASTint I8 Unsigned)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTint I8 Unsigned)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTptr Any)); (pair ?? 21 (ASTint I8 Unsigned)); (pair ?? 22 (ASTint I8 Unsigned)); (pair ?? 23 (ASTint I8 Unsigned)); (pair ?? 24 (ASTint I8 Unsigned)); (pair ?? 25 (ASTptr Any)); (pair ?? 26 (ASTint I8 Unsigned)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTint I8 Unsigned)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I8 Unsigned)); (pair ?? 32 (ASTint I8 Unsigned)); (pair ?? 33 (ASTint I8 Unsigned)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTint I8 Signed))]
     7  definition id__div32u := ident_of_nat 0.
     8  definition lbl__div32u9 := 15.
     9  definition lbl__div32u8 := 14.
     10  definition lbl__div32u7 := 13.
     11  definition lbl__div32u6 := 12.
     12  definition lbl__div32u5 := 11.
     13  definition lbl__div32u4 := 10.
     14  definition lbl__div32u3 := 9.
     15  definition lbl__div32u2 := 8.
     16  definition lbl__div32u15 := 7.
     17  definition lbl__div32u14 := 6.
     18  definition lbl__div32u13 := 5.
     19  definition lbl__div32u12 := 4.
     20  definition lbl__div32u11 := 3.
     21  definition lbl__div32u10 := 2.
     22  definition lbl__div32u1 := 1.
     23  definition lbl__div32u0 := 0.
     24  definition C_cost0 := costlabel_of_nat 2.
     25  definition C_cost1 := costlabel_of_nat 1.
     26  definition C_cost2 := costlabel_of_nat 0.
     27
     28
     29  definition pre__div32u := mk_pre_internal_function
     30    (Some ? (pair ?? 4 (ASTint I32 Unsigned)))
     31    [(pair ?? 0 (ASTint I32 Unsigned)); (pair ?? 1 (ASTint I32 Unsigned))]
     32    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Unsigned)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Signed)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I8 Signed))]
    7433    0
    7534    [
    76     (pair ?? search9 (make_St_const 10 (Ointconst I8 (repr ? 1)) search8));
    77     (pair ?? search8 (make_St_op2 Oadd 9 4 10 search7));
    78     (pair ?? search7 (make_St_op1 (Ocastint Unsigned I8) 5 9 search5));
    79     (pair ?? search6 (make_St_cost C_cost1 search5));
    80     (pair ?? search50 (make_St_cost C_cost8 search49));
    81     (pair ?? search5 (make_St_skip search44));
    82     (pair ?? search49 (make_St_const 35 (Ointconst I8 (repr ? 0)) search48));
    83     (pair ?? search48 (make_St_op1 (Ocastint Signed I8) 5 35 search47));
    84     (pair ?? search47 (make_St_const 34 (Ointconst I8 (repr ? 1)) search46));
    85     (pair ?? search46 (make_St_op2 Osub 33 1 34 search45));
    86     (pair ?? search45 (make_St_op1 (Ocastint Unsigned I8) 3 33 search5));
    87     (pair ?? search44 (make_St_op2 (Ocmpu Cge) 32 3 5 search43));
    88     (pair ?? search43 (make_St_op1 Onotbool 31 32 search42));
    89     (pair ?? search42 (make_St_cond 31 search4 search41));
    90     (pair ?? search41 (make_St_cost C_cost6 search40));
    91     (pair ?? search40 (make_St_op2 Oadd 29 3 5 search39));
    92     (pair ?? search4 (make_St_cost C_cost7 search3));
    93     (pair ?? search39 (make_St_const 30 (Ointconst I8 (repr ? 2)) search38));
    94     (pair ?? search38 (make_St_op2 Odivu 28 29 30 search37));
    95     (pair ?? search37 (make_St_op1 (Ocastint Unsigned I8) 4 28 search36));
    96     (pair ?? search36 (make_St_const 27 (Ointconst I8 (repr ? 1)) search35));
    97     (pair ?? search35 (make_St_op2 Omul 26 4 27 search34));
    98     (pair ?? search34 (make_St_op2 Oaddp 25 0 26 search33));
    99     (pair ?? search33 (make_St_load Mint8unsigned 25 24 search32));
    100     (pair ?? search32 (make_St_op2 (Ocmpu Ceq) 23 24 2 search31));
    101     (pair ?? search31 (make_St_cond 23 search30 search28));
    102     (pair ?? search30 (make_St_cost C_cost4 search29));
    103     (pair ?? search3 (make_St_const 8 (Ointconst I8 (repr ? 1)) search2));
    104     (pair ?? search29 (make_St_op1 Oid 6 4 search0));
    105     (pair ?? search28 (make_St_cost C_cost5 search27));
    106     (pair ?? search27 (make_St_const 22 (Ointconst I8 (repr ? 1)) search26));
    107     (pair ?? search26 (make_St_op2 Omul 21 4 22 search25));
    108     (pair ?? search25 (make_St_op2 Oaddp 20 0 21 search24));
    109     (pair ?? search24 (make_St_load Mint8unsigned 20 19 search23));
    110     (pair ?? search23 (make_St_op2 (Ocmpu Cgt) 18 19 2 search22));
    111     (pair ?? search22 (make_St_cond 18 search21 search17));
    112     (pair ?? search21 (make_St_cost C_cost2 search20));
    113     (pair ?? search20 (make_St_const 17 (Ointconst I8 (repr ? 1)) search19));
    114     (pair ?? search2 (make_St_op1 Onegint 7 8 search1));
    115     (pair ?? search19 (make_St_op2 Osub 16 4 17 search18));
    116     (pair ?? search18 (make_St_op1 (Ocastint Unsigned I8) 3 16 search16));
    117     (pair ?? search17 (make_St_cost C_cost3 search16));
    118     (pair ?? search16 (make_St_const 15 (Ointconst I8 (repr ? 1)) search15));
    119     (pair ?? search15 (make_St_op2 Omul 14 4 15 search14));
    120     (pair ?? search14 (make_St_op2 Oaddp 13 0 14 search13));
    121     (pair ?? search13 (make_St_load Mint8unsigned 13 12 search12));
    122     (pair ?? search12 (make_St_op2 (Ocmpu Clt) 11 12 2 search11));
    123     (pair ?? search11 (make_St_cond 11 search10 search6));
    124     (pair ?? search10 (make_St_cost C_cost0 search9));
    125     (pair ?? search1 (make_St_op1 (Ocastint Signed I8) 6 7 search0));
    126     (pair ?? search0 (make_St_return))
     35    (pair ?? lbl__div32u9 (make_St_cond 7 lbl__div32u2 lbl__div32u8));
     36    (pair ?? lbl__div32u8 (make_St_cost C_cost0 lbl__div32u7));
     37    (pair ?? lbl__div32u7 (make_St_op2 Osub 3 3 1 lbl__div32u6));
     38    (pair ?? lbl__div32u6 (make_St_const 6 (Ointconst I32 (repr ? 1)) lbl__div32u5));
     39    (pair ?? lbl__div32u5 (make_St_op1 (Ocastint Signed I32) 5 6 lbl__div32u4));
     40    (pair ?? lbl__div32u4 (make_St_op2 Oadd 2 2 5 lbl__div32u3));
     41    (pair ?? lbl__div32u3 (make_St_skip lbl__div32u11));
     42    (pair ?? lbl__div32u2 (make_St_cost C_cost1 lbl__div32u1));
     43    (pair ?? lbl__div32u15 (make_St_cost C_cost2 lbl__div32u14));
     44    (pair ?? lbl__div32u14 (make_St_const 9 (Ointconst I8 (repr ? 0)) lbl__div32u13));
     45    (pair ?? lbl__div32u13 (make_St_op1 (Ocastint Signed I32) 2 9 lbl__div32u12));
     46    (pair ?? lbl__div32u12 (make_St_op1 Oid 3 0 lbl__div32u3));
     47    (pair ?? lbl__div32u11 (make_St_op2 (Ocmpu Cge) 8 3 1 lbl__div32u10));
     48    (pair ?? lbl__div32u10 (make_St_op1 Onotbool 7 8 lbl__div32u9));
     49    (pair ?? lbl__div32u1 (make_St_op1 Oid 4 2 lbl__div32u0));
     50    (pair ?? lbl__div32u0 (make_St_return))
    12751]
    12852
    129     search50
    130     search0.
    131 
    132   definition id_main := ident_of_nat 1.
    133   definition main9 := 61.
    134   definition main8 := 60.
    135   definition main7 := 59.
    136   definition main61 := 58.
    137   definition main60 := 57.
    138   definition main6 := 56.
    139   definition main59 := 55.
    140   definition main58 := 54.
    141   definition main57 := 53.
    142   definition main56 := 52.
    143   definition main55 := 51.
    144   definition main54 := 50.
    145   definition main53 := 49.
    146   definition main52 := 48.
    147   definition main51 := 47.
    148   definition main50 := 46.
    149   definition main5 := 45.
    150   definition main49 := 44.
    151   definition main48 := 43.
    152   definition main47 := 42.
    153   definition main46 := 41.
    154   definition main45 := 40.
    155   definition main44 := 39.
    156   definition main43 := 38.
    157   definition main42 := 37.
    158   definition main41 := 36.
    159   definition main40 := 35.
    160   definition main4 := 34.
    161   definition main39 := 33.
    162   definition main38 := 32.
    163   definition main37 := 31.
    164   definition main36 := 30.
    165   definition main35 := 29.
    166   definition main34 := 28.
    167   definition main33 := 27.
    168   definition main32 := 26.
    169   definition main31 := 25.
    170   definition main30 := 24.
    171   definition main3 := 23.
    172   definition main29 := 22.
    173   definition main28 := 21.
    174   definition main27 := 20.
    175   definition main26 := 19.
    176   definition main25 := 18.
    177   definition main24 := 17.
    178   definition main23 := 16.
    179   definition main22 := 15.
    180   definition main21 := 14.
    181   definition main20 := 13.
    182   definition main2 := 12.
    183   definition main19 := 11.
    184   definition main18 := 10.
    185   definition main17 := 9.
    186   definition main16 := 8.
    187   definition main15 := 7.
    188   definition main14 := 6.
    189   definition main13 := 5.
    190   definition main12 := 4.
    191   definition main11 := 3.
    192   definition main10 := 2.
    193   definition main1 := 1.
    194   definition main0 := 0.
    195   definition C_cost9 := costlabel_of_nat 0.
     53    lbl__div32u15
     54    lbl__div32u0.
     55
     56  definition id__div32s := ident_of_nat 1.
     57  definition lbl__div32s9 := 25.
     58  definition lbl__div32s8 := 24.
     59  definition lbl__div32s7 := 23.
     60  definition lbl__div32s6 := 22.
     61  definition lbl__div32s5 := 21.
     62  definition lbl__div32s4 := 20.
     63  definition lbl__div32s3 := 19.
     64  definition lbl__div32s25 := 18.
     65  definition lbl__div32s24 := 17.
     66  definition lbl__div32s23 := 16.
     67  definition lbl__div32s22 := 15.
     68  definition lbl__div32s21 := 14.
     69  definition lbl__div32s20 := 13.
     70  definition lbl__div32s2 := 12.
     71  definition lbl__div32s19 := 11.
     72  definition lbl__div32s18 := 10.
     73  definition lbl__div32s17 := 9.
     74  definition lbl__div32s16 := 8.
     75  definition lbl__div32s15 := 7.
     76  definition lbl__div32s14 := 6.
     77  definition lbl__div32s13 := 5.
     78  definition lbl__div32s12 := 4.
     79  definition lbl__div32s11 := 3.
     80  definition lbl__div32s10 := 2.
     81  definition lbl__div32s1 := 1.
     82  definition lbl__div32s0 := 0.
     83  definition C_cost3 := costlabel_of_nat 4.
     84  definition C_cost4 := costlabel_of_nat 3.
     85  definition C_cost7 := costlabel_of_nat 2.
     86  definition C_cost5 := costlabel_of_nat 1.
     87  definition C_cost6 := costlabel_of_nat 0.
     88
     89
     90  definition pre__div32s := mk_pre_internal_function
     91    (Some ? (pair ?? 7 (ASTint I32 Signed)))
     92    [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I32 Signed))]
     93    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I8 Signed))]
     94    0
     95    [
     96    (pair ?? lbl__div32s9 (make_St_cost C_cost3 lbl__div32s8));
     97    (pair ?? lbl__div32s8 (make_St_op1 Onegint 9 1 lbl__div32s7));
     98    (pair ?? lbl__div32s7 (make_St_op1 (Ocastint Signed I32) 5 9 lbl__div32s6));
     99    (pair ?? lbl__div32s6 (make_St_op1 Onegint 3 3 lbl__div32s4));
     100    (pair ?? lbl__div32s5 (make_St_cost C_cost4 lbl__div32s4));
     101    (pair ?? lbl__div32s4 (make_St_call_id id__div32u [4; 5] (Some ? 6) lbl__div32s3));
     102    (pair ?? lbl__div32s3 (make_St_op1 Oid 2 6 lbl__div32s2));
     103    (pair ?? lbl__div32s25 (make_St_cost C_cost7 lbl__div32s24));
     104    (pair ?? lbl__div32s24 (make_St_op1 (Ocastint Signed I32) 4 0 lbl__div32s23));
     105    (pair ?? lbl__div32s23 (make_St_op1 (Ocastint Signed I32) 5 1 lbl__div32s22));
     106    (pair ?? lbl__div32s22 (make_St_const 15 (Ointconst I8 (repr ? 1)) lbl__div32s21));
     107    (pair ?? lbl__div32s21 (make_St_op1 (Ocastint Signed I32) 3 15 lbl__div32s20));
     108    (pair ?? lbl__div32s20 (make_St_const 14 (Ointconst I32 (repr ? 0)) lbl__div32s19));
     109    (pair ?? lbl__div32s2 (make_St_op1 (Ocastint Unsigned I32) 8 2 lbl__div32s1));
     110    (pair ?? lbl__div32s19 (make_St_op2 (Ocmp Clt) 13 0 14 lbl__div32s18));
     111    (pair ?? lbl__div32s18 (make_St_cond 13 lbl__div32s17 lbl__div32s13));
     112    (pair ?? lbl__div32s17 (make_St_cost C_cost5 lbl__div32s16));
     113    (pair ?? lbl__div32s16 (make_St_op1 Onegint 12 0 lbl__div32s15));
     114    (pair ?? lbl__div32s15 (make_St_op1 (Ocastint Signed I32) 4 12 lbl__div32s14));
     115    (pair ?? lbl__div32s14 (make_St_op1 Onegint 3 3 lbl__div32s12));
     116    (pair ?? lbl__div32s13 (make_St_cost C_cost6 lbl__div32s12));
     117    (pair ?? lbl__div32s12 (make_St_const 11 (Ointconst I32 (repr ? 0)) lbl__div32s11));
     118    (pair ?? lbl__div32s11 (make_St_op2 (Ocmp Clt) 10 1 11 lbl__div32s10));
     119    (pair ?? lbl__div32s10 (make_St_cond 10 lbl__div32s9 lbl__div32s5));
     120    (pair ?? lbl__div32s1 (make_St_op2 Omul 7 3 8 lbl__div32s0));
     121    (pair ?? lbl__div32s0 (make_St_return))
     122]
     123
     124    lbl__div32s25
     125    lbl__div32s0.
     126
     127  definition id_search := ident_of_nat 2.
     128  definition lbl_search9 := 65.
     129  definition lbl_search8 := 64.
     130  definition lbl_search7 := 63.
     131  definition lbl_search65 := 62.
     132  definition lbl_search64 := 61.
     133  definition lbl_search63 := 60.
     134  definition lbl_search62 := 59.
     135  definition lbl_search61 := 58.
     136  definition lbl_search60 := 57.
     137  definition lbl_search6 := 56.
     138  definition lbl_search59 := 55.
     139  definition lbl_search58 := 54.
     140  definition lbl_search57 := 53.
     141  definition lbl_search56 := 52.
     142  definition lbl_search55 := 51.
     143  definition lbl_search54 := 50.
     144  definition lbl_search53 := 49.
     145  definition lbl_search52 := 48.
     146  definition lbl_search51 := 47.
     147  definition lbl_search50 := 46.
     148  definition lbl_search5 := 45.
     149  definition lbl_search49 := 44.
     150  definition lbl_search48 := 43.
     151  definition lbl_search47 := 42.
     152  definition lbl_search46 := 41.
     153  definition lbl_search45 := 40.
     154  definition lbl_search44 := 39.
     155  definition lbl_search43 := 38.
     156  definition lbl_search42 := 37.
     157  definition lbl_search41 := 36.
     158  definition lbl_search40 := 35.
     159  definition lbl_search4 := 34.
     160  definition lbl_search39 := 33.
     161  definition lbl_search38 := 32.
     162  definition lbl_search37 := 31.
     163  definition lbl_search36 := 30.
     164  definition lbl_search35 := 29.
     165  definition lbl_search34 := 28.
     166  definition lbl_search33 := 27.
     167  definition lbl_search32 := 26.
     168  definition lbl_search31 := 25.
     169  definition lbl_search30 := 24.
     170  definition lbl_search3 := 23.
     171  definition lbl_search29 := 22.
     172  definition lbl_search28 := 21.
     173  definition lbl_search27 := 20.
     174  definition lbl_search26 := 19.
     175  definition lbl_search25 := 18.
     176  definition lbl_search24 := 17.
     177  definition lbl_search23 := 16.
     178  definition lbl_search22 := 15.
     179  definition lbl_search21 := 14.
     180  definition lbl_search20 := 13.
     181  definition lbl_search2 := 12.
     182  definition lbl_search19 := 11.
     183  definition lbl_search18 := 10.
     184  definition lbl_search17 := 9.
     185  definition lbl_search16 := 8.
     186  definition lbl_search15 := 7.
     187  definition lbl_search14 := 6.
     188  definition lbl_search13 := 5.
     189  definition lbl_search12 := 4.
     190  definition lbl_search11 := 3.
     191  definition lbl_search10 := 2.
     192  definition lbl_search1 := 1.
     193  definition lbl_search0 := 0.
     194  definition C_cost16 := costlabel_of_nat 8.
     195  definition C_cost9 := costlabel_of_nat 7.
     196  definition C_cost14 := costlabel_of_nat 6.
     197  definition C_cost15 := costlabel_of_nat 5.
     198  definition C_cost12 := costlabel_of_nat 4.
     199  definition C_cost13 := costlabel_of_nat 3.
     200  definition C_cost10 := costlabel_of_nat 2.
     201  definition C_cost11 := costlabel_of_nat 1.
     202  definition C_cost8 := costlabel_of_nat 0.
     203
     204
     205  definition pre_search := mk_pre_internal_function
     206    (Some ? (pair ?? 8 (ASTint I8 Unsigned)))
     207    [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
     208    [(pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I8 Unsigned)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTptr Any)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I32 Signed)); (pair ?? 22 (ASTint I32 Signed)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTint I32 Signed)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I32 Signed)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTint I8 Unsigned)); (pair ?? 38 (ASTint I32 Signed)); (pair ?? 39 (ASTint I32 Signed)); (pair ?? 40 (ASTint I8 Signed)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTint I32 Signed)); (pair ?? 45 (ASTint I32 Signed)); (pair ?? 46 (ASTint I32 Signed)); (pair ?? 47 (ASTint I32 Signed)); (pair ?? 48 (ASTint I32 Signed)); (pair ?? 49 (ASTint I32 Signed)); (pair ?? 50 (ASTint I8 Signed))]
     209    0
     210    [
     211    (pair ?? lbl_search9 (make_St_const 13 (Ointconst I32 (repr ? 1)) lbl_search8));
     212    (pair ?? lbl_search8 (make_St_op2 Oadd 11 12 13 lbl_search7));
     213    (pair ?? lbl_search7 (make_St_op1 (Ocastint Signed I8) 6 11 lbl_search5));
     214    (pair ?? lbl_search65 (make_St_cost C_cost16 lbl_search64));
     215    (pair ?? lbl_search64 (make_St_const 50 (Ointconst I8 (repr ? 0)) lbl_search63));
     216    (pair ?? lbl_search63 (make_St_op1 (Ocastint Signed I8) 6 50 lbl_search62));
     217    (pair ?? lbl_search62 (make_St_op1 (Ocastint Unsigned I32) 48 1 lbl_search61));
     218    (pair ?? lbl_search61 (make_St_const 49 (Ointconst I32 (repr ? 1)) lbl_search60));
     219    (pair ?? lbl_search60 (make_St_op2 Osub 47 48 49 lbl_search59));
     220    (pair ?? lbl_search6 (make_St_cost C_cost9 lbl_search5));
     221    (pair ?? lbl_search59 (make_St_op1 (Ocastint Signed I8) 4 47 lbl_search5));
     222    (pair ?? lbl_search58 (make_St_op1 (Ocastint Unsigned I32) 45 4 lbl_search57));
     223    (pair ?? lbl_search57 (make_St_op1 (Ocastint Unsigned I32) 46 6 lbl_search56));
     224    (pair ?? lbl_search56 (make_St_op2 (Ocmp Cge) 44 45 46 lbl_search55));
     225    (pair ?? lbl_search55 (make_St_op1 Onotbool 43 44 lbl_search54));
     226    (pair ?? lbl_search54 (make_St_cond 43 lbl_search4 lbl_search53));
     227    (pair ?? lbl_search53 (make_St_cost C_cost14 lbl_search52));
     228    (pair ?? lbl_search52 (make_St_op1 (Ocastint Unsigned I32) 41 4 lbl_search51));
     229    (pair ?? lbl_search51 (make_St_op1 (Ocastint Unsigned I32) 42 6 lbl_search50));
     230    (pair ?? lbl_search50 (make_St_op2 Oadd 38 41 42 lbl_search49));
     231    (pair ?? lbl_search5 (make_St_skip lbl_search58));
     232    (pair ?? lbl_search49 (make_St_const 40 (Ointconst I8 (repr ? 2)) lbl_search48));
     233    (pair ?? lbl_search48 (make_St_op1 (Ocastint Signed I32) 39 40 lbl_search47));
     234    (pair ?? lbl_search47 (make_St_call_id id__div32s [38; 39] (Some ? 7) lbl_search46));
     235    (pair ?? lbl_search46 (make_St_op1 Oid 3 7 lbl_search45));
     236    (pair ?? lbl_search45 (make_St_op1 (Ocastint Signed I8) 5 3 lbl_search44));
     237    (pair ?? lbl_search44 (make_St_const 37 (Ointconst I8 (repr ? 1)) lbl_search43));
     238    (pair ?? lbl_search43 (make_St_op2 Omul 36 5 37 lbl_search42));
     239    (pair ?? lbl_search42 (make_St_op2 Oaddp 35 0 36 lbl_search41));
     240    (pair ?? lbl_search41 (make_St_load Mint8unsigned 35 34 lbl_search40));
     241    (pair ?? lbl_search40 (make_St_op1 (Ocastint Unsigned I32) 32 34 lbl_search39));
     242    (pair ?? lbl_search4 (make_St_cost C_cost15 lbl_search3));
     243    (pair ?? lbl_search39 (make_St_op1 (Ocastint Unsigned I32) 33 2 lbl_search38));
     244    (pair ?? lbl_search38 (make_St_op2 (Ocmp Ceq) 31 32 33 lbl_search37));
     245    (pair ?? lbl_search37 (make_St_cond 31 lbl_search36 lbl_search34));
     246    (pair ?? lbl_search36 (make_St_cost C_cost12 lbl_search35));
     247    (pair ?? lbl_search35 (make_St_op1 Oid 8 5 lbl_search0));
     248    (pair ?? lbl_search34 (make_St_cost C_cost13 lbl_search33));
     249    (pair ?? lbl_search33 (make_St_const 30 (Ointconst I8 (repr ? 1)) lbl_search32));
     250    (pair ?? lbl_search32 (make_St_op2 Omul 29 5 30 lbl_search31));
     251    (pair ?? lbl_search31 (make_St_op2 Oaddp 28 0 29 lbl_search30));
     252    (pair ?? lbl_search30 (make_St_load Mint8unsigned 28 27 lbl_search29));
     253    (pair ?? lbl_search3 (make_St_const 10 (Ointconst I32 (repr ? 1)) lbl_search2));
     254    (pair ?? lbl_search29 (make_St_op1 (Ocastint Unsigned I32) 25 27 lbl_search28));
     255    (pair ?? lbl_search28 (make_St_op1 (Ocastint Unsigned I32) 26 2 lbl_search27));
     256    (pair ?? lbl_search27 (make_St_op2 (Ocmp Cgt) 24 25 26 lbl_search26));
     257    (pair ?? lbl_search26 (make_St_cond 24 lbl_search25 lbl_search20));
     258    (pair ?? lbl_search25 (make_St_cost C_cost10 lbl_search24));
     259    (pair ?? lbl_search24 (make_St_op1 (Ocastint Unsigned I32) 22 5 lbl_search23));
     260    (pair ?? lbl_search23 (make_St_const 23 (Ointconst I32 (repr ? 1)) lbl_search22));
     261    (pair ?? lbl_search22 (make_St_op2 Osub 21 22 23 lbl_search21));
     262    (pair ?? lbl_search21 (make_St_op1 (Ocastint Signed I8) 4 21 lbl_search19));
     263    (pair ?? lbl_search20 (make_St_cost C_cost11 lbl_search19));
     264    (pair ?? lbl_search2 (make_St_op1 Onegint 9 10 lbl_search1));
     265    (pair ?? lbl_search19 (make_St_const 20 (Ointconst I8 (repr ? 1)) lbl_search18));
     266    (pair ?? lbl_search18 (make_St_op2 Omul 19 5 20 lbl_search17));
     267    (pair ?? lbl_search17 (make_St_op2 Oaddp 18 0 19 lbl_search16));
     268    (pair ?? lbl_search16 (make_St_load Mint8unsigned 18 17 lbl_search15));
     269    (pair ?? lbl_search15 (make_St_op1 (Ocastint Unsigned I32) 15 17 lbl_search14));
     270    (pair ?? lbl_search14 (make_St_op1 (Ocastint Unsigned I32) 16 2 lbl_search13));
     271    (pair ?? lbl_search13 (make_St_op2 (Ocmp Clt) 14 15 16 lbl_search12));
     272    (pair ?? lbl_search12 (make_St_cond 14 lbl_search11 lbl_search6));
     273    (pair ?? lbl_search11 (make_St_cost C_cost8 lbl_search10));
     274    (pair ?? lbl_search10 (make_St_op1 (Ocastint Unsigned I32) 12 5 lbl_search9));
     275    (pair ?? lbl_search1 (make_St_op1 (Ocastint Signed I8) 8 9 lbl_search0));
     276    (pair ?? lbl_search0 (make_St_return))
     277]
     278
     279    lbl_search65
     280    lbl_search0.
     281
     282  definition id_main := ident_of_nat 3.
     283  definition lbl_main9 := 61.
     284  definition lbl_main8 := 60.
     285  definition lbl_main7 := 59.
     286  definition lbl_main61 := 58.
     287  definition lbl_main60 := 57.
     288  definition lbl_main6 := 56.
     289  definition lbl_main59 := 55.
     290  definition lbl_main58 := 54.
     291  definition lbl_main57 := 53.
     292  definition lbl_main56 := 52.
     293  definition lbl_main55 := 51.
     294  definition lbl_main54 := 50.
     295  definition lbl_main53 := 49.
     296  definition lbl_main52 := 48.
     297  definition lbl_main51 := 47.
     298  definition lbl_main50 := 46.
     299  definition lbl_main5 := 45.
     300  definition lbl_main49 := 44.
     301  definition lbl_main48 := 43.
     302  definition lbl_main47 := 42.
     303  definition lbl_main46 := 41.
     304  definition lbl_main45 := 40.
     305  definition lbl_main44 := 39.
     306  definition lbl_main43 := 38.
     307  definition lbl_main42 := 37.
     308  definition lbl_main41 := 36.
     309  definition lbl_main40 := 35.
     310  definition lbl_main4 := 34.
     311  definition lbl_main39 := 33.
     312  definition lbl_main38 := 32.
     313  definition lbl_main37 := 31.
     314  definition lbl_main36 := 30.
     315  definition lbl_main35 := 29.
     316  definition lbl_main34 := 28.
     317  definition lbl_main33 := 27.
     318  definition lbl_main32 := 26.
     319  definition lbl_main31 := 25.
     320  definition lbl_main30 := 24.
     321  definition lbl_main3 := 23.
     322  definition lbl_main29 := 22.
     323  definition lbl_main28 := 21.
     324  definition lbl_main27 := 20.
     325  definition lbl_main26 := 19.
     326  definition lbl_main25 := 18.
     327  definition lbl_main24 := 17.
     328  definition lbl_main23 := 16.
     329  definition lbl_main22 := 15.
     330  definition lbl_main21 := 14.
     331  definition lbl_main20 := 13.
     332  definition lbl_main2 := 12.
     333  definition lbl_main19 := 11.
     334  definition lbl_main18 := 10.
     335  definition lbl_main17 := 9.
     336  definition lbl_main16 := 8.
     337  definition lbl_main15 := 7.
     338  definition lbl_main14 := 6.
     339  definition lbl_main13 := 5.
     340  definition lbl_main12 := 4.
     341  definition lbl_main11 := 3.
     342  definition lbl_main10 := 2.
     343  definition lbl_main1 := 1.
     344  definition lbl_main0 := 0.
     345  definition C_cost17 := costlabel_of_nat 0.
    196346
    197347
     
    199349    (Some ? (pair ?? 2 (ASTint I32 Signed)))
    200350    []
    201     [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I8 Signed)); (pair ?? 15 (ASTint I8 Signed)); (pair ?? 16 (ASTint I8 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I8 Signed)); (pair ?? 24 (ASTint I8 Signed)); (pair ?? 25 (ASTint I8 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I8 Signed)); (pair ?? 33 (ASTint I8 Signed)); (pair ?? 34 (ASTint I8 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I8 Signed)); (pair ?? 42 (ASTint I8 Signed)); (pair ?? 43 (ASTint I8 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I8 Signed)); (pair ?? 51 (ASTint I8 Signed)); (pair ?? 52 (ASTint I8 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
     351    [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I32 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I32 Signed)); (pair ?? 51 (ASTint I32 Signed)); (pair ?? 52 (ASTint I32 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
    202352    5
    203353    [
    204     (pair ?? main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) main8));
    205     (pair ?? main8 (make_St_op2 Oaddp 3 8 9 main7));
    206     (pair ?? main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) main6));
    207     (pair ?? main61 (make_St_cost C_cost9 main60));
    208     (pair ?? main60 (make_St_const 53 (Oaddrstack 0) main59));
    209     (pair ?? main6 (make_St_op1 (Ocastint Signed I8) 4 7 main5));
    210     (pair ?? main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) main58));
    211     (pair ?? main58 (make_St_op2 Oaddp 49 53 54 main57));
    212     (pair ?? main57 (make_St_const 51 (Ointconst I8 (repr ? 0)) main56));
    213     (pair ?? main56 (make_St_const 52 (Ointconst I8 (repr ? 1)) main55));
    214     (pair ?? main55 (make_St_op2 Omul 50 51 52 main54));
    215     (pair ?? main54 (make_St_op2 Oaddp 46 49 50 main53));
    216     (pair ?? main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) main52));
    217     (pair ?? main52 (make_St_op1 (Ocastint Signed I8) 47 48 main51));
    218     (pair ?? main51 (make_St_store Mint8unsigned 46 47 main50));
    219     (pair ?? main50 (make_St_const 44 (Oaddrstack 0) main49));
    220     (pair ?? main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) main4));
    221     (pair ?? main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) main48));
    222     (pair ?? main48 (make_St_op2 Oaddp 40 44 45 main47));
    223     (pair ?? main47 (make_St_const 42 (Ointconst I8 (repr ? 1)) main46));
    224     (pair ?? main46 (make_St_const 43 (Ointconst I8 (repr ? 1)) main45));
    225     (pair ?? main45 (make_St_op2 Omul 41 42 43 main44));
    226     (pair ?? main44 (make_St_op2 Oaddp 37 40 41 main43));
    227     (pair ?? main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) main42));
    228     (pair ?? main42 (make_St_op1 (Ocastint Signed I8) 38 39 main41));
    229     (pair ?? main41 (make_St_store Mint8unsigned 37 38 main40));
    230     (pair ?? main40 (make_St_const 35 (Oaddrstack 0) main39));
    231     (pair ?? main4 (make_St_op1 (Ocastint Signed I8) 5 6 main3));
    232     (pair ?? main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) main38));
    233     (pair ?? main38 (make_St_op2 Oaddp 31 35 36 main37));
    234     (pair ?? main37 (make_St_const 33 (Ointconst I8 (repr ? 2)) main36));
    235     (pair ?? main36 (make_St_const 34 (Ointconst I8 (repr ? 1)) main35));
    236     (pair ?? main35 (make_St_op2 Omul 32 33 34 main34));
    237     (pair ?? main34 (make_St_op2 Oaddp 28 31 32 main33));
    238     (pair ?? main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) main32));
    239     (pair ?? main32 (make_St_op1 (Ocastint Signed I8) 29 30 main31));
    240     (pair ?? main31 (make_St_store Mint8unsigned 28 29 main30));
    241     (pair ?? main30 (make_St_const 26 (Oaddrstack 0) main29));
    242     (pair ?? main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main2));
    243     (pair ?? main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) main28));
    244     (pair ?? main28 (make_St_op2 Oaddp 22 26 27 main27));
    245     (pair ?? main27 (make_St_const 24 (Ointconst I8 (repr ? 3)) main26));
    246     (pair ?? main26 (make_St_const 25 (Ointconst I8 (repr ? 1)) main25));
    247     (pair ?? main25 (make_St_op2 Omul 23 24 25 main24));
    248     (pair ?? main24 (make_St_op2 Oaddp 19 22 23 main23));
    249     (pair ?? main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) main22));
    250     (pair ?? main22 (make_St_op1 (Ocastint Signed I8) 20 21 main21));
    251     (pair ?? main21 (make_St_store Mint8unsigned 19 20 main20));
    252     (pair ?? main20 (make_St_const 17 (Oaddrstack 0) main19));
    253     (pair ?? main2 (make_St_op1 Oid 0 1 main1));
    254     (pair ?? main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) main18));
    255     (pair ?? main18 (make_St_op2 Oaddp 13 17 18 main17));
    256     (pair ?? main17 (make_St_const 15 (Ointconst I8 (repr ? 4)) main16));
    257     (pair ?? main16 (make_St_const 16 (Ointconst I8 (repr ? 1)) main15));
    258     (pair ?? main15 (make_St_op2 Omul 14 15 16 main14));
    259     (pair ?? main14 (make_St_op2 Oaddp 10 13 14 main13));
    260     (pair ?? main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) main12));
    261     (pair ?? main12 (make_St_op1 (Ocastint Signed I8) 11 12 main11));
    262     (pair ?? main11 (make_St_store Mint8unsigned 10 11 main10));
    263     (pair ?? main10 (make_St_const 8 (Oaddrstack 0) main9));
    264     (pair ?? main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 main0));
    265     (pair ?? main0 (make_St_return))
     354    (pair ?? lbl_main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) lbl_main8));
     355    (pair ?? lbl_main8 (make_St_op2 Oaddp 3 8 9 lbl_main7));
     356    (pair ?? lbl_main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) lbl_main6));
     357    (pair ?? lbl_main61 (make_St_cost C_cost17 lbl_main60));
     358    (pair ?? lbl_main60 (make_St_const 53 (Oaddrstack 0) lbl_main59));
     359    (pair ?? lbl_main6 (make_St_op1 (Ocastint Signed I8) 4 7 lbl_main5));
     360    (pair ?? lbl_main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) lbl_main58));
     361    (pair ?? lbl_main58 (make_St_op2 Oaddp 49 53 54 lbl_main57));
     362    (pair ?? lbl_main57 (make_St_const 51 (Ointconst I32 (repr ? 0)) lbl_main56));
     363    (pair ?? lbl_main56 (make_St_const 52 (Ointconst I32 (repr ? 1)) lbl_main55));
     364    (pair ?? lbl_main55 (make_St_op2 Omul 50 51 52 lbl_main54));
     365    (pair ?? lbl_main54 (make_St_op2 Oaddp 46 49 50 lbl_main53));
     366    (pair ?? lbl_main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) lbl_main52));
     367    (pair ?? lbl_main52 (make_St_op1 (Ocastint Signed I8) 47 48 lbl_main51));
     368    (pair ?? lbl_main51 (make_St_store Mint8unsigned 46 47 lbl_main50));
     369    (pair ?? lbl_main50 (make_St_const 44 (Oaddrstack 0) lbl_main49));
     370    (pair ?? lbl_main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) lbl_main4));
     371    (pair ?? lbl_main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) lbl_main48));
     372    (pair ?? lbl_main48 (make_St_op2 Oaddp 40 44 45 lbl_main47));
     373    (pair ?? lbl_main47 (make_St_const 42 (Ointconst I32 (repr ? 1)) lbl_main46));
     374    (pair ?? lbl_main46 (make_St_const 43 (Ointconst I32 (repr ? 1)) lbl_main45));
     375    (pair ?? lbl_main45 (make_St_op2 Omul 41 42 43 lbl_main44));
     376    (pair ?? lbl_main44 (make_St_op2 Oaddp 37 40 41 lbl_main43));
     377    (pair ?? lbl_main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) lbl_main42));
     378    (pair ?? lbl_main42 (make_St_op1 (Ocastint Signed I8) 38 39 lbl_main41));
     379    (pair ?? lbl_main41 (make_St_store Mint8unsigned 37 38 lbl_main40));
     380    (pair ?? lbl_main40 (make_St_const 35 (Oaddrstack 0) lbl_main39));
     381    (pair ?? lbl_main4 (make_St_op1 (Ocastint Signed I8) 5 6 lbl_main3));
     382    (pair ?? lbl_main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) lbl_main38));
     383    (pair ?? lbl_main38 (make_St_op2 Oaddp 31 35 36 lbl_main37));
     384    (pair ?? lbl_main37 (make_St_const 33 (Ointconst I32 (repr ? 2)) lbl_main36));
     385    (pair ?? lbl_main36 (make_St_const 34 (Ointconst I32 (repr ? 1)) lbl_main35));
     386    (pair ?? lbl_main35 (make_St_op2 Omul 32 33 34 lbl_main34));
     387    (pair ?? lbl_main34 (make_St_op2 Oaddp 28 31 32 lbl_main33));
     388    (pair ?? lbl_main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) lbl_main32));
     389    (pair ?? lbl_main32 (make_St_op1 (Ocastint Signed I8) 29 30 lbl_main31));
     390    (pair ?? lbl_main31 (make_St_store Mint8unsigned 28 29 lbl_main30));
     391    (pair ?? lbl_main30 (make_St_const 26 (Oaddrstack 0) lbl_main29));
     392    (pair ?? lbl_main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) lbl_main2));
     393    (pair ?? lbl_main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) lbl_main28));
     394    (pair ?? lbl_main28 (make_St_op2 Oaddp 22 26 27 lbl_main27));
     395    (pair ?? lbl_main27 (make_St_const 24 (Ointconst I32 (repr ? 3)) lbl_main26));
     396    (pair ?? lbl_main26 (make_St_const 25 (Ointconst I32 (repr ? 1)) lbl_main25));
     397    (pair ?? lbl_main25 (make_St_op2 Omul 23 24 25 lbl_main24));
     398    (pair ?? lbl_main24 (make_St_op2 Oaddp 19 22 23 lbl_main23));
     399    (pair ?? lbl_main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) lbl_main22));
     400    (pair ?? lbl_main22 (make_St_op1 (Ocastint Signed I8) 20 21 lbl_main21));
     401    (pair ?? lbl_main21 (make_St_store Mint8unsigned 19 20 lbl_main20));
     402    (pair ?? lbl_main20 (make_St_const 17 (Oaddrstack 0) lbl_main19));
     403    (pair ?? lbl_main2 (make_St_op1 Oid 0 1 lbl_main1));
     404    (pair ?? lbl_main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) lbl_main18));
     405    (pair ?? lbl_main18 (make_St_op2 Oaddp 13 17 18 lbl_main17));
     406    (pair ?? lbl_main17 (make_St_const 15 (Ointconst I32 (repr ? 4)) lbl_main16));
     407    (pair ?? lbl_main16 (make_St_const 16 (Ointconst I32 (repr ? 1)) lbl_main15));
     408    (pair ?? lbl_main15 (make_St_op2 Omul 14 15 16 lbl_main14));
     409    (pair ?? lbl_main14 (make_St_op2 Oaddp 10 13 14 lbl_main13));
     410    (pair ?? lbl_main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) lbl_main12));
     411    (pair ?? lbl_main12 (make_St_op1 (Ocastint Signed I8) 11 12 lbl_main11));
     412    (pair ?? lbl_main11 (make_St_store Mint8unsigned 10 11 lbl_main10));
     413    (pair ?? lbl_main10 (make_St_const 8 (Oaddrstack 0) lbl_main9));
     414    (pair ?? lbl_main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 lbl_main0));
     415    (pair ?? lbl_main0 (make_St_return))
    266416]
    267417
    268     main61
    269     main0.
     418    lbl_main61
     419    lbl_main0.
    270420
    271421
     
    274424  do f_main \larr make_internal_function pre_main;
    275425  do f_search \larr make_internal_function pre_search;
     426  do f__div32s \larr make_internal_function pre__div32s;
     427  do f__div32u \larr make_internal_function pre__div32u;
    276428
    277429OK ? (mk_program ??
    278430(  (pair ?? id_main f_main)::
    279431  (pair ?? id_search f_search)::
     432  (pair ?? id__div32s f__div32s)::
     433  (pair ?? id__div32u f__div32u)::
    280434(nil ?))
    281435  id_main
     
    287441   normalize  (* you can examine the result here *)
    288442   @refl qed.
    289 
  • Deliverables/D3.3/id-lookup-branch/common/SmallstepExec.ma

    r797 r1197  
    6161 | e_step tr s e ⇒ e_step ??? tr s e
    6262 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
    63 #o #i #s #e cases e; //; qed.
     63#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
     64 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
     65  here, used reflexivity instead *)
    6466
    6567axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
  • Deliverables/D3.3/id-lookup-branch/utilities/Interference.ma

    r1153 r1197  
    33include "common/Graphs.ma".
    44include "common/Registers.ma".
     5include "utilities/RegisterSet.ma".
     6
     7definition vertex ≝ nat. (* XXX: int in o'caml *)
     8
     9(* vertex sets *)
     10axiom vertex_set: Type[0].
     11axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
     12axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
     13axiom vs_subset: vertex_set → vertex_set → bool.
     14
     15(* vertex maps *)
     16axiom vertex_map: Type[0] → Type[0].
     17axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    518
    619definition interference_graph ≝ graph label.
    7 axiom vertex: Type[0].
    8 axiom vertex_set: Type[0].
    9 axiom vertex_map: Type[0].
    1020
    11 axiom ig_create: list register → interference_graph.
     21definition ig_create: ∀rs. rs_set rs → interference_graph ≝
     22  let 〈ignore_int, regmap, degree〉 ≝
     23    rs_fold rs (λr. λv_regmap_degree.
     24      let 〈v, regmap, degree〉 ≝ v_regmap_degree in
     25        〈v + 1, (r, v)::regmap,
     26
     27
     28
     29
     30let create regs =
     31  let (_ : int), regmap, degree =
     32    Register.Set.fold (fun r (v, regmap, degree) ->
     33      v+1,
     34      RegMap.add r v regmap,
     35      PrioritySet.add v 0 degree
     36    ) regs (0, RegMap.empty, PrioritySet.empty)
     37  in
     38  {
     39    regmap = regmap;
     40    ivv = Vertex.Map.empty;
     41    ivh = Vertex.Map.empty;
     42    pvv = Vertex.Map.empty;
     43    pvh = Vertex.Map.empty;
     44    degree = degree;
     45    nmr = degree
     46  }
     47
     48
    1249axiom ig_mki: interference_graph → (list register) × (list Register) →
    1350  (list register) × (list Register) → interference_graph.
     
    3067  interference_graph → option vertex.
    3168axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    32 axiom ig_ipp: interference_graph → vertex → list vertex.
     69axiom ig_ipp: interference_graph → vertex → vertex_set.
    3370axiom ig_iph: interference_graph → vertex → list Register.
    34 axiom ig_ppp: interference_graph → vertex → list vertex.
     71axiom ig_ppp: interference_graph → vertex → vertex_set.
    3572axiom ig_pph: interference_graph → vertex → list Register.
    3673definition ig_ppedge ≝ vertex × vertex.
  • Deliverables/D3.3/id-lookup-branch/utilities/RegisterSet.ma

    r1075 r1197  
    1111  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
     13  rs_subset: rs_set → rs_set → bool;
    1314  rs_to_list: rs_set → list Register;
    1415  rs_from_list: list Register → rs_set
     
    4546  λs: list Register.
    4647    nub_by ? eq_Register (r @ s).
     48
     49definition rs_list_set_subset ≝
     50  λr: list Register.
     51  λs: list Register.
     52    forall … (λx. member … eq_Register x s) r.
    4753 
    4854definition rs_list_set_from_list ≝
     
    5561                  rs_list_set_insert rs_list_set_exists
    5662                  rs_list_set_union
     63                  rs_list_set_subset
    5764                  (λx. x) rs_list_set_from_list.
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r1105 r1197  
    9797| #h #t #IH #l2 normalize //
    9898] qed.
     99
     100let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
     101match l with
     102[ nil ⇒ None B
     103| cons h t ⇒
     104    match f h with
     105    [ None ⇒ find A B f t
     106    | Some b ⇒ Some B b
     107    ]
     108].
Note: See TracChangeset for help on using the changeset viewer.