Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 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/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
Note: See TracChangeset for help on using the changeset viewer.