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/RTLabs/semantics.ma

    r774 r797  
    5757  update RegisterTag val locals reg v.
    5858
     59axiom WrongNumberOfParameters : String.
     60
    5961let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    6062match rs with
    61 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
    62 | cons r rst ⇒ match vs with [ nil ⇒ Error ? | cons v vst ⇒
     63[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
     64| cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    6365  let locals' ≝ add RegisterTag val locals r v in
    6466  params_store rst vst locals'
    6567] ].
    6668
     69axiom BadRegister : String.
     70
    6771definition reg_retrieve : register_env ? → register → res val ≝
    68 λlocals,reg. opt_to_res … (lookup ?? locals reg).
     72λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
     73
     74axiom FailedOp : String.
     75axiom MissingSymbol : String.
    6976
    7077(* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
     
    7481[ Aindexed i ⇒ λargs.
    7582    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
    76     opt_to_res … (ev_addp v (Vint i))
     83    opt_to_res … (msg FailedOp) (ev_addp v (Vint i))
    7784| Aindexed2 ⇒ λargs.
    7885    do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
    7986    do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
    80     opt_to_res … (ev_addp v1 v2)
     87    opt_to_res … (msg FailedOp) (ev_addp v1 v2)
    8188| Aglobal id off ⇒ λargs.
    82     do loc ← opt_to_res … (find_symbol ?? ge id);
     89    do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    8390    OK ? (Vptr Any loc ? (shift_offset zero_offset off))
    8491| Abased id off ⇒ λargs.
    85     do loc ← opt_to_res … (find_symbol ?? ge id);
     92    do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    8693    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
    87     opt_to_res … (ev_addp (Vptr Any loc ? zero_offset) v)
     94    opt_to_res … (msg FailedOp) (ev_addp (Vptr Any loc ? zero_offset) v)
    8895| Ainstack off ⇒ λargs.
    8996    OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
     
    9299
    93100
     101axiom MissingStatement : String.
     102axiom FailedConstant : String.
     103axiom FailedLoad : String.
     104axiom FailedStore : String.
     105axiom BadFunction : String.
     106axiom BadJumpTable : String.
     107axiom BadJumpValue : String.
     108axiom FinalState : String.
     109axiom ReturnMismatch : String.
    94110
    95111definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
     
    97113match st with
    98114[ State f fs m ⇒
    99   ! s ← lookup ?? (f_graph (func f)) (next f);
     115  ! s ← opt_to_io … [MSG MissingStatement; CTX ? (next f)] (lookup ?? (f_graph (func f)) (next f));
    100116  match s with
    101117  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    102118  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    103119  | St_const r cst l ⇒
    104       ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
     120      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
    105121      ! locals ← reg_store r v (locals f);
    106122      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    107123  | St_op1 op dst src l ⇒
    108124      ! v ← reg_retrieve (locals f) src;
    109       ! v' ← opt_to_res … (eval_unop op v);
     125      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
    110126      ! locals ← reg_store dst v' (locals f);
    111127      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
     
    113129      ! v1 ← reg_retrieve (locals f) src1;
    114130      ! v2 ← reg_retrieve (locals f) src2;
    115       ! v' ← opt_to_res … (eval_binop op v1 v2);
     131      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    116132      ! locals ← reg_store dst v' (locals f);
    117133      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    118134  | St_load chunk mode args dst l ⇒
    119135      ! vaddr ← eval_addr ge f mode args;
    120       ! v ← opt_to_res … (loadv chunk m vaddr);
     136      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    121137      ! locals ← reg_store dst v (locals f);
    122138      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
     
    124140      ! vaddr ← eval_addr ge f mode args;
    125141      ! v ← reg_retrieve (locals f) src;
    126       ! m' ← opt_to_res … (storev chunk m vaddr v);
     142      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    127143      ret ? 〈E0, build_state f fs m' l〉
    128 
    129144  | St_call_id id args dst sig l ⇒ (* XXX: haven't used sig *)
    130       ! b ← opt_to_res … (find_symbol ?? ge id);
    131       ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
     145      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     146      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    132147      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    133148      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    134149  | St_call_ptr frs args dst sig l ⇒  (* XXX: haven't used sig *)
    135150      ! fv ← reg_retrieve (locals f) frs;
    136       ! fd ← opt_to_res … (find_funct ?? ge fv);
     151      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    137152      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    138153      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    139154  | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
    140       ! b ← opt_to_res … (find_symbol ?? ge id);
    141       ! fd ← opt_to_res … (find_funct_ptr ?? ge b);
     155      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     156      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    142157      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    143158      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    144159  | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
    145160      ! fv ← reg_retrieve (locals f) frs;
    146       ! fd ← opt_to_res … (find_funct ?? ge fv);
     161      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    147162      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    148163      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    149164
    150165  | St_condcst cst ltrue lfalse ⇒
    151       ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
     166      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
    152167      ! b ← eval_bool_of_val v;
    153168      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    154169  | St_cond1 op src ltrue lfalse ⇒
    155170      ! v ← reg_retrieve (locals f) src;
    156       ! v' ← opt_to_res … (eval_unop op v);
     171      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
    157172      ! b ← eval_bool_of_val v';
    158173      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
     
    160175      ! v1 ← reg_retrieve (locals f) src1;
    161176      ! v2 ← reg_retrieve (locals f) src2;
    162       ! v' ← opt_to_res … (eval_binop op v1 v2);
     177      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    163178      ! b ← eval_bool_of_val v';
    164179      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
     
    168183      match v with
    169184      [ Vint i ⇒
    170           ! l ← nth_opt ? (nat_of_bitvector ? i) ls;
     185          ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
    171186          ret ? 〈E0, build_state f fs m l〉
    172       | _ ⇒ Wrong ???
     187      | _ ⇒ Wrong ??? (msg BadJumpValue)
    173188      ]
    174189
     
    193208| Returnstate v dst fs m ⇒
    194209    match fs with
    195     [ nil ⇒ Error ? (* Already in final state *)
     210    [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
    196211    | cons f fs' ⇒
    197212        ! locals ← match dst with
    198213                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
    199                                          | _ ⇒ Error ? ]
    200                    | Some d ⇒ match v with [ None ⇒ Error ?
     214                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
     215                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
    201216                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
    202217        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
     
    219234  do ge ← globalenv Genv ?? p;
    220235  do m ← init_mem Genv ?? p;
    221   do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    222   do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     236  let main ≝ prog_main ?? p in
     237  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
     238  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    223239  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
    224240
Note: See TracChangeset for help on using the changeset viewer.