Changeset 797 for src/Cminor


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.

Location:
src/Cminor
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r761 r797  
    4545].
    4646
     47axiom UnknownLocal : String.
     48axiom FailedConstant : String.
     49axiom FailedOp : String.
     50axiom FailedLoad : String.
     51
    4752let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
    4853match e with
    4954[ Id i ⇒
    50     do r ← opt_to_res … (lookup ?? en i);
     55    do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
    5156    OK ? 〈E0, r〉
    5257| Cst c ⇒
    53     do r ← opt_to_res … (eval_constant (find_symbol … ge) sp c);
     58    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    5459    OK ? 〈E0, r〉
    5560| Op1 op e' ⇒
    5661    do 〈tr,v〉 ← eval_expr ge e' en sp m;
    57     do r ← opt_to_res … (eval_unop op v);
     62    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    5863    OK ? 〈tr, r〉
    5964| Op2 op e1 e2 ⇒
    6065    do 〈tr1,v1〉 ← eval_expr ge e1 en sp m;
    6166    do 〈tr2,v2〉 ← eval_expr ge e2 en sp m;
    62     do r ← opt_to_res … (eval_binop op v1 v2);
     67    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    6368    OK ? 〈tr1 ⧺ tr2, r〉
    6469| Mem chunk e ⇒
    6570    do 〈tr,v〉 ← eval_expr ge e en sp m;
    66     do r ← opt_to_res … (loadv chunk m v);
     71    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    6772    OK ? 〈tr, r〉
    6873| Cond e' e1 e2 ⇒
     
    7681].
    7782
     83axiom BadState : String.
     84
    7885let rec k_exit (n:nat) (k:cont) on k : res cont ≝
    7986match k with
    80 [ Kstop ⇒ Error ?
     87[ Kstop ⇒ Error ? (msg BadState)
    8188| Kseq _ k' ⇒ k_exit n k'
    8289| Kblock k' ⇒ match n with [ O ⇒ OK ? k' | S m ⇒ k_exit m k' ]
    83 | Kcall _ _ _ _ _ ⇒ Error ?
     90| Kcall _ _ _ _ _ ⇒ Error ? (msg BadState)
    8491].
    8592
     
    122129].
    123130
     131axiom WrongNumberOfParameters : String.
     132
    124133let rec bind_params (vs:list val) (ids:list ident) : res env ≝
    125134match vs with
    126 [ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? ]
     135[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
    127136| cons v vt ⇒
    128137    match ids with
    129     [ nil ⇒ Error ?
     138    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    130139    | cons id idt ⇒
    131140        do en ← bind_params vt idt;
     
    136145definition init_locals : env → list ident → env ≝
    137146foldr ?? (λid,en. add ?? en id Vundef).
     147
     148axiom FailedStore : String.
     149axiom BadFunctionValue : String.
     150axiom BadSwitchValue : String.
     151axiom UnknownLabel : String.
     152axiom ReturnMismatch : String.
    138153
    139154definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
     
    144159    [ St_skip ⇒
    145160        match k with
    146         [ Kstop ⇒ Wrong ???
     161        [ Kstop ⇒ Wrong ??? (msg BadState)
    147162        | Kseq s' k' ⇒ ret ? 〈E0, State f s' en m sp k'〉
    148163        | Kblock k' ⇒ ret ? 〈E0, State f s en m sp k'〉
     
    157172        ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
    158173        ! 〈tr',v〉 ← eval_expr ge e en sp m;
    159         ! m' ← opt_to_res … (storev chunk m vdst v);
     174        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    160175        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    161176
    162177    | St_call dst ef args sig ⇒ (* XXX sig unused? *)
    163178        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    164         ! fd ← opt_to_res … (find_funct ?? ge vf);
     179        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    165180        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    166181        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    167182    | St_tailcall ef args sig ⇒
    168183        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    169         ! fd ← opt_to_res … (find_funct ?? ge vf);
     184        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    170185        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    171186        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
     
    187202            ! k' ← k_exit (find_case ? i cs default) k;
    188203            ret ? 〈tr, State f St_skip en m sp k'〉
    189         | _ ⇒ Wrong ???
     204        | _ ⇒ Wrong ??? (msg BadSwitchValue)
    190205        ]
    191206    | St_return eo ⇒
     
    198213    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
    199214    | St_goto l ⇒
    200         ! 〈s', k'〉 ← opt_to_res … (find_label l (f_body f) (call_cont k));
     215        ! 〈s', k'〉 ← opt_to_res … [MSG UnknownLabel; CTX ? l] (find_label l (f_body f) (call_cont k));
    201216        ret ? 〈E0, State f s' en m sp k'〉
    202217    | St_cost l s' ⇒
     
    219234    [ Kcall dst f sp en k' ⇒
    220235        ! en' ← match res with
    221                 [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? ]
    222                 | Some v ⇒ match dst with [ None ⇒ Error ?
     236                [ None ⇒ match dst with [ None ⇒ OK ? en | Some _ ⇒ Error ? (msg ReturnMismatch)]
     237                | Some v ⇒ match dst with [ None ⇒ Error ? (msg ReturnMismatch)
    223238                                          | Some id ⇒ update ?? en id v ]
    224239                ];
    225240        ret ? 〈E0, State f St_skip en' m sp k'〉
    226     | _ ⇒ Wrong ???
     241    | _ ⇒ Wrong ??? (msg BadState)
    227242    ]
    228243].
     
    249264  mk_execstep … ? is_final mem_of_state eval_step.
    250265
     266axiom MainMissing : String.
     267
    251268definition make_initial_state : Cminor_program → res (genv × state) ≝
    252269λp.
    253270  do ge ← globalenv Genv ?? p;
    254271  do m ← init_mem Genv ?? p;
    255   do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    256   do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     272  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     273  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    257274  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
    258275
  • src/Cminor/test/sum-bad.ma

    r761 r797  
    7272.
    7373
    74 example exec: exec_up_to Cminor_fullexec myprog 1000 [ ] = Error ?.
    75 normalize  (* you can examine the result here *)
    76 @refl
     74example exec: exec_up_to Cminor_fullexec myprog 1000 [ ] = Error ??.
     75[normalize  (* you can examine the result here *)
     76 @refl
     77|skip
     78]
    7779qed.
    7880
    7981include "Cminor/initialisation.ma".
    8082
    81 example exec2: exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ] = Error ?.
    82 normalize  (* you can examine the result here *)
    83 @refl
     83example exec2: exec_up_to Cminor_fullexec (replace_init myprog) 1000 [ ] = Error ??.
     84[normalize  (* you can examine the result here *)
     85 @refl
     86|skip
     87]
    8488qed.
  • 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.