Changeset 797 for src/Cminor/toRTLabs.ma


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (10 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r790 r797  
    9393].
    9494
     95axiom UnknownVariable : String.
     96
    9597definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝
    9698λenv,e,ptrs,f.
    9799  match e with
    98100  [ Id i ⇒
    99       do r ← opt_to_res … (lookup … env i);
     101      do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
    100102      OK ? 〈r, f〉
    101103  | _ ⇒
     
    109111                    OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
    110112
     113axiom BadCminorProgram : String.
     114
    111115let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
    112116match e with
    113117[ Id i ⇒
    114     do r ← opt_to_res … (lookup ?? env i);
     118    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    115119    match register_eq r dst with
    116120    [ inl _ ⇒ OK ? f
     
    161165    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
    162166    | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
    163     | _ ⇒ Error ? (* int and float constants are nonsense here *)
     167    | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
    164168    ]
    165169| Op2 op e1 e2 ⇒
     
    193197match e with
    194198[ Id i ⇒
    195     do r ← opt_to_res … (lookup ?? env i);
     199    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    196200    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
    197201| Cst c ⇒
     
    219223λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
    220224
     225(* This shouldn't occur; maybe use vectors? *)
     226axiom WrongNumberOfArguments : String.
     227
    221228let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
    222229match es with
    223 [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ]
     230[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
    224231| cons e et ⇒
    225232    match dsts with
    226     [ nil ⇒ Error ?
     233    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
    227234    | cons r rt ⇒
    228235        do f ← add_exprs env et rt ptrs f;
     
    230237    ]
    231238].
     239
     240axiom UnknownLabel : String.
     241axiom ReturnMismatch : String.
    232242
    233243let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝
     
    235245[ St_skip ⇒ OK ? f
    236246| St_assign x e ⇒
    237     do dst ← opt_to_res … (lookup ?? env x);
     247    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    238248    add_expr env e dst ptrs f
    239249| St_store q e1 e2 ⇒
     
    245255      match return_opt_id with
    246256      [ None ⇒ OK ? (None ?)
    247       | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r)
     257      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
    248258      ];
    249259    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
     
    286296    add_stmt env label_env s ((f_entry f)::exits) ptrs f
    287297| St_exit n ⇒
    288     do l ← opt_to_res … (nth_opt ? n exits);
     298    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    289299    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    290300| St_switch e tab n ⇒
    291301    do 〈r,f〉 ← choose_reg env e ptrs f;
    292     do l_default ← opt_to_res … (nth_opt ? n exits);
     302    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    293303    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
    294304    do f ← foldr ?? (λcs,f.
     
    296306      let 〈i,n〉 ≝ cs in
    297307      do 〈cr,f〉 ← fresh_reg … f;
    298       do l_case ← opt_to_res … (nth_opt ? n exits);
     308      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    299309      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
    300310      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
     
    306316    | Some e ⇒
    307317        match f_result f with
    308         [ None ⇒ Error ?
     318        [ None ⇒ Error ? (msg ReturnMismatch)
    309319        | Some r ⇒ add_expr env e r ptrs f
    310320        ]
     
    312322| St_label l s' ⇒
    313323    do f ← add_stmt env label_env s' exits ptrs f;
    314     do l' ← opt_to_res … (lookup ?? label_env l);
     324    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    315325    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
    316326| St_goto l ⇒
    317     do l' ← opt_to_res … (lookup ?? label_env l);
     327    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    318328    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
    319329| St_cost l s' ⇒
     
    354364      do 〈r,gen〉 ← fresh … reggen2;
    355365      OK ? 〈Some ? r, r::locals0, gen〉 ];
    356 do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f);
     366do ptrs ← mmap ?? (λid. opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id)) (f_ptrs f);
    357367do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
    358368do 〈l,labgen〉 ← fresh … labgen1;
Note: See TracChangeset for help on using the changeset viewer.