Changeset 797


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (8 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
Files:
1 added
22 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r744 r797  
    88(*
    99include "Plogic/russell_support.ma".
    10 *)
     10
    1111definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
    1212  λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].
     
    2626
    2727definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝
    28   λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒
     28  λA,P,a.match a with [ Error m ⇒ Error ? m | OK b ⇒
    2929    match b with [ dp w p ⇒ OK ? w] ].
    3030
     
    3939coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject
    4040  on _c:Sig ? ? to ?.
    41 
     41*)
    4242definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
    43   λA,P,a. match a with [ Error ⇒ True | OK v ⇒ P v ].
     43  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
     44
     45axiom TypeMismatch : String.
     46axiom ValueIsNotABoolean : String.
    4447
    4548definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
     
    4750  [ Vint i ⇒ match ty with
    4851    [ Tint _ _ ⇒ OK ? (¬eq i zero)
    49     | _ ⇒ Error ?
     52    | _ ⇒ Error ? (msg TypeMismatch)
    5053    ]
    5154  | Vfloat f ⇒ match ty with
    5255    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
    53     | _ ⇒ Error ?
     56    | _ ⇒ Error ? (msg TypeMismatch)
    5457    ]
    5558  | Vptr _ _ _ _ ⇒ match ty with
    5659    [ Tpointer _ _ ⇒ OK ? true
    57     | _ ⇒ Error ?
     60    | _ ⇒ Error ? (msg TypeMismatch)
    5861    ]
    5962  | Vnull _ ⇒ match ty with
    6063    [ Tpointer _ _ ⇒ OK ? false
    61     | _ ⇒ Error ?
    62     ]
    63   | _ ⇒ Error ?
     64    | _ ⇒ Error ? (msg TypeMismatch)
     65    ]
     66  | _ ⇒ Error ? (msg ValueIsNotABoolean)
    6467  ].
    6568
     
    7881
    7982lemma bind_OK: ∀A,B,P,e,f.
    80   (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
    81   match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
     83  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
     84  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
    8285#A #B #P #e #f elim e; /2/; qed.
    8386
    8487lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
    85   (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
    86   match bind (Sig A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
     88  (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
     89  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
    8790#A #B #P #P' #e #f elim e;
    8891[ #v0 elim v0; #v #Hv #IH @IH
    89 | #_ @I
     92| #m #_ @I
    9093] qed.
    9194
    9295lemma bind2_OK: ∀A,B,C,P,e,f.
    93   (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
    94   match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
     96  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
     97  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
    9598#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
    9699
    97 lemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (Sig (A×B) P). ∀f:A → B → res C.
    98   (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
    99   match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
    100 #A #B #C #P #P' #e #f elim e; //;
    101 #v0 elim v0; #v elim v; #v1 #v2 #Hv #IH @IH //; qed.
    102 
    103 lemma opt_bind_OK: ∀A,B,P,e,f.
    104   (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
    105   match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
    106 #A #B #P #e #f elim e; normalize; /2/; qed.
    107 (*
    108 lemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
    109   (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
    110   match match eject ?? e with [ pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
    111 #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
    112 [ #H @(False_ind … H)
    113 | #e'' cases e''; #a #b #Pab #H normalize; /2/;
    114 ] qed.
    115 *)
    116 (*
    117 nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
    118 #A #B #e cases e; //; qed.
    119 *)
     100lemma opt_bind_OK: ∀A,B,P,m,e,f.
     101  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
     102  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
     103#A #B #P #m #e #f elim e; normalize; /2/; qed.
     104
     105
     106axiom BadCast : String. (* TODO: refine into more precise errors? *)
    120107
    121108definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
     
    129116    | Tarray r _ _ ⇒ OK ? (Vnull r)
    130117    | Tfunction _ _ ⇒ OK ? (Vnull Code)
    131     | _ ⇒ Error ?
    132     ]
    133   | _ ⇒ Error ?
    134   ]
    135 | false ⇒ Error ?
     118    | _ ⇒ Error ? (msg BadCast)
     119    ]
     120  | _ ⇒ Error ? (msg BadCast)
     121  ]
     122| false ⇒ Error ? (msg BadCast)
    136123].
    137124
     
    148135    | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    149136    | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    150     | _ ⇒ Error ?
     137    | _ ⇒ Error ? (msg BadCast)
    151138    ]
    152139  | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    153140  | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    154141  | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
    155   | _ ⇒ Error ?
     142  | _ ⇒ Error ? (msg TypeMismatch)
    156143  ]
    157144| Vfloat f ⇒
     
    161148    [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
    162149    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
    163     | _ ⇒ Error ?
    164     ]
    165   | _ ⇒ Error ?
     150    | _ ⇒ Error ? (msg BadCast)
     151    ]
     152  | _ ⇒ Error ? (msg TypeMismatch)
    166153  ]
    167154| Vptr r b _ ofs ⇒
    168     do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    169     do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
     155    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
     156    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
    170157    do s' ← match ty' with
    171158         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    172          | _ ⇒ Error ? ];
     159         | _ ⇒ Error ? (msg BadCast)];
    173160    match pointer_compat_dec b s' with
    174161    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
    175     | inr _ ⇒ Error ?
     162    | inr _ ⇒ Error ? (msg BadCast)
    176163    ]
    177164| Vnull r ⇒
    178     do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    179     do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
     165    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
     166    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
    180167    do s' ← match ty' with
    181168         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    182          | _ ⇒ Error ? ];
     169         | _ ⇒ Error ? (msg BadCast) ];
    183170    OK ? (Vnull s')
    184 | _ ⇒ Error ?
     171| _ ⇒ Error ? (msg BadCast)
    185172].
    186173
     
    191178   a structurally smaller value, we break out the surrounding Expr constructor
    192179   and use exec_lvalue'. *)
     180
     181axiom BadlyTypedTerm : String.
     182axiom UnknownIdentifier : String.
     183axiom BadLvalueTerm : String.
     184axiom FailedLoad : String.
     185axiom FailedOp : String.
    193186
    194187let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
     
    200193  | Evar _ ⇒
    201194      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    202       do v ← opt_to_res ? (load_value_of_type' ty m l);
     195      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
    203196      OK ? 〈v,tr〉
    204197  | Ederef _ ⇒
    205198      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    206       do v ← opt_to_res ? (load_value_of_type' ty m l);
     199      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
    207200      OK ? 〈v,tr〉
    208201  | Efield _ _ ⇒
    209202      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    210       do v ← opt_to_res ? (load_value_of_type' ty m l);
     203      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
    211204      OK ? 〈v,tr〉
    212205  | Eaddrof a ⇒
     
    217210          match pointer_compat_dec loc r with
    218211          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
    219           | inr _ ⇒ Error ?
     212          | inr _ ⇒ Error ? (msg TypeMismatch)
    220213          ]
    221214        ]
    222       | _ ⇒ Error ?
     215      | _ ⇒ Error ? (msg BadlyTypedTerm)
    223216      ]
    224217  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
    225218  | Eunop op a ⇒
    226219      do 〈v1,tr〉 ← exec_expr ge en m a;
    227       do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
     220      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
    228221      OK ? 〈v,tr〉
    229222  | Ebinop op a1 a2 ⇒
    230223      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    231224      do 〈v2,tr2〉 ← exec_expr ge en m a2;
    232       do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
     225      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
    233226      OK ? 〈v,tr1⧺tr2〉
    234227  | Econdition a1 a2 a3 ⇒
     
    268261  [ Evar id ⇒
    269262      match (get … id en) with
    270       [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
     263      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
    271264      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
    272265      ]
     
    275268      match v with
    276269      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
    277       | _ ⇒ Error ?
     270      | _ ⇒ Error ? (msg TypeMismatch)
    278271      ]
    279272  | Efield a i ⇒
     
    286279          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    287280          OK ? 〈lofs,tr〉
    288       | _ ⇒ Error ?
    289       ]
    290   | _ ⇒ Error ?
     281      | _ ⇒ Error ? (msg BadlyTypedTerm)
     282      ]
     283  | _ ⇒ Error ? (msg BadLvalueTerm)
    291284  ]
    292285and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
     
    324317]]].
    325318
     319axiom WrongNumberOfParameters : String.
     320axiom FailedStore : String.
     321
    326322(* TODO: can we establish that length params = length vs in advance? *)
    327323let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
    328324  match params with
    329   [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? ]
     325  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
    330326  | cons idty params' ⇒ match idty with [ pair id ty ⇒
    331327      match vs with
    332       [ nil ⇒ Error ?
     328      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    333329      | cons v1 vl ⇒
    334           do b ← opt_to_res ? (get … id e);
    335           do m1 ← opt_to_res ? (store_value_of_type ty m b zero_offset v1);
     330          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (get … id e);
     331          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
    336332          exec_bind_parameters e m1 params' vl
    337333      ]
     
    424420
    425421definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
    426 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
     422λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
    427423
    428424let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
     
    451447  store_value_of_type ty m loc ofs v ].
    452448
     449axiom NonsenseState : String.
     450axiom ReturnMismatch : String.
     451axiom UnknownLabel : String.
     452axiom BadFunctionValue : String.
     453
    453454let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
    454455match st with
     
    458459    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
    459460    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
    460     ! m' ← store_value_of_type' (typeof a1) m l v2;
     461    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
    461462    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
    462463  | Scall lhs a al ⇒
    463464    ! 〈vf,tr2〉 ← exec_expr ge e m a;
    464465    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
    465     ! fd ← find_funct ? ? ge vf;
     466    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
    466467    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
    467468(* requires associativity of IOMonad, so rearrange it below
     
    487488          match fn_return f with
    488489          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
    489           | _ ⇒ Wrong ???
     490          | _ ⇒ Wrong ??? (msg NonsenseState)
    490491          ]
    491492      | Kcall _ _ _ _ ⇒
    492493          match fn_return f with
    493494          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
    494           | _ ⇒ Wrong ???
     495          | _ ⇒ Wrong ??? (msg NonsenseState)
    495496          ]
    496497      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     
    505506      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
    506507      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    507       | _ ⇒ Wrong ???
     508      | _ ⇒ Wrong ??? (msg NonsenseState)
    508509      ]
    509510  | Scontinue ⇒
     
    520521      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
    521522      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
    522       | _ ⇒ Wrong ???
     523      | _ ⇒ Wrong ??? (msg NonsenseState)
    523524      ]
    524525  | Sbreak ⇒
     
    529530      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    530531      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
    531       | _ ⇒ Wrong ???
     532      | _ ⇒ Wrong ??? (msg NonsenseState)
    532533      ]
    533534  | Sifthenelse a s1 s2 ⇒
     
    553554    [ None ⇒ match fn_return f with
    554555      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
    555       | _ ⇒ Wrong ???
     556      | _ ⇒ Wrong ??? (msg ReturnMismatch)
    556557      ]
    557558    | Some a ⇒
    558559        match type_eq_dec (fn_return f) Tvoid with
    559         [ inl _ ⇒ Wrong ???
     560        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
    560561        | inr _ ⇒
    561562          ! 〈v,tr〉 ← exec_expr ge e m a;
     
    566567      ! 〈v,tr〉 ← exec_expr ge e m a;
    567568      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
    568                    | _ ⇒ Wrong ??? ]
     569                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
    569570  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
    570571  | Sgoto lbl ⇒
    571572      match find_label lbl (fn_body f) (call_cont k) with
    572573      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
    573       | None ⇒ Wrong ???
     574      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
    574575      ]
    575576  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
     
    594595    | Some r' ⇒
    595596      match r' with [ pair l ty ⇒
    596        
    597           ! m' ← store_value_of_type' ty m l res;
     597          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
    598598          ret ? 〈E0, (State f Sskip k' e m')〉
    599599      ]
    600600    ]
    601   | _ ⇒ Wrong ???
     601  | _ ⇒ Wrong ??? (msg NonsenseState)
    602602  ]
    603603].
     604
     605axiom MainMissing : String.
    604606
    605607let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    606608  do ge ← globalenv Genv ?? p;
    607609  do m0 ← init_mem Genv ?? p;
    608   do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    609   do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     610  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     611  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    610612  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
    611613
  • src/Clight/CexecComplete.ma

    r726 r797  
    2626[ #a #k #IH #v' #p #H whd in H ⊢ %; elim H; #r #H' %{ r} @IH @H'
    2727| #v #v' #p #H @H
    28 | #a #b *;
     28| #a #b #c *;
    2929] qed.
    3030
    3131lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
    32 #A #a #v' cases a; //; whd in ⊢ (% → ?); *;
     32#A #a #v' cases a; // #m whd in ⊢ (% → ?) *;
    3333qed.
    3434
     
    3636#A #P #e #v cases e;
    3737[ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
    38 | *;
     38| #m *;
    3939] qed.
    4040
     
    7777  ]
    7878| destruct (e3) skip (e13); //
    79 ] qed.
    80 
    81 lemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    82 yields A a v' →
    83 yields_sig A P (err_inject A P (Some ? a) p) v'.
    84 #A #P #a cases a;
    85 [ #v #v' #p #H @H
    86 | #a #b *;
    8779] qed.
    8880
  • src/Clight/CexecEquiv.ma

    r732 r797  
    99| se_stop : trace → int → mem → s_execution
    1010| se_step : trace → state → s_execution → s_execution
    11 | se_wrong : s_execution
     11| se_wrong : errmsg → s_execution
    1212| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.
    1313
     
    1717    single_exec_of e se →
    1818    single_exec_of (e_step ??? tr s e) (se_step tr s se)
    19 | seo_wrong : single_exec_of (e_wrong ???) se_wrong
     19| seo_wrong : ∀msg:errmsg. single_exec_of (e_wrong ??? msg) (se_wrong msg)
    2020| seo_interact : ∀o,k,i,se.
    2121    single_exec_of (k i) se →
     
    6969  [ #r #FINAL | #FINAL ]
    7070  #EXEC whd in EXEC:(??%?); destruct @refl
    71 | #EXEC whd in EXEC:(??%?); destruct
     71| #msg #EXEC whd in EXEC:(??%?); destruct
    7272] qed.
    7373
     
    8282  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
    8383  destruct @refl
    84 | #EXEC whd in EXEC:(??%?); destruct
     84| #msg #EXEC whd in EXEC:(??%?); destruct
    8585] qed.
    8686
     
    9393| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
    9494  @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    95 | #EXEC whd in EXEC:(??%?); destruct
     95| #msg #EXEC whd in EXEC:(??%?); destruct
    9696] qed.
    9797
     
    114114    >(exec_e_step_inv … H2)
    115115    <(exec_e_step … H2) in H1 #H1 % //
    116 | #_ #E destruct
     116| #msg #_ #E destruct
    117117| #o #k #i #se #H1 #H2 #E destruct
    118118] qed.
     
    125125[ #tr #r #m #E1 #E2 destruct
    126126| #tr #s #e #se #H1 #H2 #E destruct (E)
    127 | #_ #E destruct
     127| #msg #_ #E destruct
    128128| #o #k #i #se #H1 #H2 #E destruct (E);
    129129    lapply (exec_step_sound ge s0);
     
    139139            >(exec_e_step_inv … H3)
    140140            #S @S
    141         | #_ #E destruct
     141        | #msg #_ #E destruct
    142142        | #o #k #i #se #H1 #H2 #E destruct
    143143        ]
     
    145145        whd in ⊢ (??%? → ?); @is_final_elim
    146146        [ #r ] #F #E whd in E:(??%?); destruct
    147     | >(exec_inf_aux_unfold …)
     147    | #msg >(exec_inf_aux_unfold …)
    148148        #E' whd in E':(??%?); destruct (E');
    149149    ]
     
    156156[ #tr #r #m #E1 #E2 destruct
    157157| #tr #s #e #se #H1 #H2 #E destruct (E)
    158 | #_ #E destruct
     158| #msg #_ #E destruct
    159159| #o #k #i #se #H1 #H2 #E destruct (E);
    160160    lapply (exec_step_sound ge s0);
     
    177177                | #NF #E whd in E:(??%?); destruct (E)
    178178                ]
    179             | #E whd in E:(??%?); destruct (E)
     179            | #msg #E whd in E:(??%?); destruct (E)
    180180            ]
    181181       | #tr #s #e #e' #H #EXEC #E destruct (E)
    182        | #EXEC #E destruct (E)
     182       | #msg #EXEC #E destruct (E)
    183183       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
    184184       ]
    185185   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    186186       @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E)
    187    | #E whd in E:(??%?); destruct (E)
     187   | #msg #E whd in E:(??%?); destruct (E)
    188188   ]
    189189] qed.
     
    250250
    251251inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
    252 | go_wrong: ∀tr,s,s',e.
    253     execution_isteps tr s e s' se_wrong
     252| go_wrong: ∀tr,s,s',e,msg.
     253    execution_isteps tr s e s' (se_wrong msg)
    254254    execution_goes_wrong tr s (se_step E0 s e) s'.
    255255
     
    283283        @is_final_elim [ #r'' #FINAL | #F ]
    284284        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    285     | #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     285    | #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    286286    ]
    287287    inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2);
    288288    @H
    289289| #tr' #s' #e' #se' #H #EXEC' #E destruct
    290 | #EXEC' #E destruct
     290| #msg #EXEC' #E destruct
    291291| #o #k #i #e #H #EXEC #E destruct
    292292] qed.
     
    304304  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
    305305  ]
    306 | #EXEC whd in EXEC:(??%?); destruct (EXEC);
     306| #msg #EXEC whd in EXEC:(??%?); destruct (EXEC);
    307307] qed.
    308308
     
    355355qed.
    356356
    357 lemma exec_from_wrong: ∀ge,s.
    358   exec_from ge s se_wrong
    359   exec_step ge s = Wrong ???.
    360 #ge #s #H whd in H;
     357lemma exec_from_wrong: ∀ge,s,msg.
     358  exec_from ge s (se_wrong msg)
     359  exec_step ge s = Wrong ??? msg.
     360#ge #s #msg #H whd in H;
    361361inversion H;
    362362[ #tr #r #m #EXEC #E destruct (E)
     
    364364| >(exec_inf_aux_unfold …)
    365365    cases (exec_step ge s);
    366   [ #o #k #EXEC whd in EXEC:(??%?); destruct
    367   | #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim
     366  [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct
     367  | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim
    368368      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    369   | //
     369  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?) destruct @refl
    370370  ]
    371371| #o #k #i #e #H #EXEC #E destruct
     
    383383    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
    384384        [ #r ] #F #E whd in E:(??%?); destruct @F
    385     | #E whd in E:(??%?); destruct
    386     ]
    387 | #EXEC #E destruct
     385    | #msg #E whd in E:(??%?); destruct
     386    ]
     387| #msg #EXEC #E destruct
    388388| #o #k #i #e' #H #EXEC #E destruct
    389389] qed.
     
    397397[ #tr' #r #m #EXEC #E destruct
    398398| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
    399 | #EXEC #E destruct
     399| #msg #EXEC #E destruct
    400400| #o' #k' #i' #e' #H #EXEC #E destruct;
    401401    >(exec_inf_aux_unfold …) in EXEC;
     
    413413                @(absurd ?? F)
    414414                %{ r'} //;
    415             | #E whd in E:(??%?); destruct
     415            | #msg #E whd in E:(??%?); destruct
    416416            ]
    417         | #EXECK #E  whd in E:(??%?); destruct
     417        | #msg #EXECK #E  whd in E:(??%?); destruct
    418418        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
    419419        ]
    420420    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    421421        @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct;
    422     | #E whd in E:(??%?); destruct
     422    | #msg #E whd in E:(??%?); destruct
    423423    ]
    424424] qed.
     
    432432  (¬∃r. final_state s' r).
    433433#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
    434 #tr #s #s' #e #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
     434#tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
    435435cases (several_steps … ESTEPS EXEC);
    436436#STAR #EXEC' %
     
    492492cases e1; //; qed.
    493493
    494 lemma opt_does_not_interact: ∀A,B,P,e1,e2.
     494lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg.
    495495  (∀x:B.interact_prop A P (e2 x)) →
    496   interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
    497 #A #B #P #e1 #e2 #H
     496  interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2).
     497#A #B #P #e1 #e2 #msg #H
    498498cases e1; //; qed.
    499499
     
    609609] qed.
    610610
    611 lemma eno_wrong: execution_not_over se_wrong → False.
    612 #H inversion H;
     611lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False.
     612#msg #H inversion H;
    613613[ #tr #s #e #E destruct
    614614| #o #k #tr #s #e #i #E destruct
     
    641641      ]
    642642  ]
    643 | #_ #_ #_ #ENO elim (eno_wrong … ENO);
     643| #msg #_ #_ #_ #ENO elim (eno_wrong … ENO);
    644644| #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_
    645645    lapply (CONTINUES E0 s o k i e' (isteps_none …));
     
    678678  [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
    679679  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    680   | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
     680  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
    681681  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
    682682  ].
     
    685685[ #tr #r #m whd; % [ % ] //
    686686| #tr #s #e1' #e2' #H' whd; % [ % ] //
    687 | whd; //
     687| #msg whd; //
    688688| #o #k #i #e #H' whd; % [ % ] //
    689689] qed.
     
    711711    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    712712    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
    713     | 3,7: #E destruct
     713    | 3,7: #msg #E destruct
    714714    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
    715715    ]
    716 | #_ #E whd in E:(?%?);
     716| #msg #_ #E whd in E:(?%?);
    717717    inversion E;
    718718    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    719719    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
    720     | 3,7: #E1 #E2 destruct
     720    | 3,7: #msg #E1 #E2 destruct
    721721    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
    722722    ]
     
    874874    | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0
    875875        @NOSTEP //
    876     | #STEPS #NOSTEP
     876    | #msg #STEPS #NOSTEP
    877877        @(ec_wrong ? s s' tr) % //;
    878878    (* The following is stupidly complicated when most of the cases are impossible.
     
    885885        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
    886886            @False_ind @NOSTEP //
    887         | #STEPS #NOSTEP
     887        | #msg #STEPS #NOSTEP
    888888            lapply (exec_step_interaction ge s');
    889889            cases (several_steps … STEPS EXEC); #_
     
    900900                @is_final_elim [ #r ] #F #S whd in S:(?%?);
    901901                cases (se_inv … S);
    902             | #S cases (se_inv … S);
     902            | #msg #S cases (se_inv … S);
    903903            ]
    904904        | #o1 #k1 #i1 #e1 #STEPS #NOSTEP
     
    917917                @is_final_elim [ #r ] #F #S whd in S:(?%?);
    918918                cases (se_inv … S);
    919             | #S cases (se_inv … S);
     919            | #msg #S cases (se_inv … S);
    920920            ]
    921921        ]
     
    937937    execution_goes_wrong tr s e s' →
    938938    execution_matches_behavior e (Goes_wrong tr)
    939 | emb_initially_wrong:
    940     execution_matches_behavior se_wrong (Goes_wrong E0).
     939| emb_initially_wrong: ∀msg.
     940    execution_matches_behavior (se_wrong msg) (Goes_wrong E0).
    941941
    942942lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
     
    960960  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
    961961#tr #tr' #s #s' #s'' #e #H inversion H;
    962 #tr1 #s1 #s2 #e1 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
     962#tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
    963963
    964964lemma behavior_of_execution: ∀s,e.
     
    10211021        %{r} @F
    10221022    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
    1023         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
     1023        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10241024        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    10251025    lapply (behavior_of_execution ??
     
    10601060            lapply (exec_state_wrong … WRONG);
    10611061            #E1 >E1 in WRONG #WRONG
    1062             inversion WRONG; #tr' #s1' #s2' #e'' #GOESWRONG #E4 #E5 #E6 #E7
     1062            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
    10631063            <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
    10641064            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
     
    10671067            @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP)
    10681068            #r % #F @(absurd ?? FINAL) %{r} @F
    1069         | #E destruct (E);
     1069        | #msg #E destruct (E);
    10701070        ]
    10711071   ]
    1072 | whd in ⊢ ((∀_.? → %) → ?);
     1072| #msg whd in ⊢ ((∀_.? → %) → ?);
    10731073    #NOINIT #_ #EXEC
    10741074    %{ (Goes_wrong E0)} %
    10751075    [ whd in EXEC:(?%?);
    10761076        cases e in EXEC;
    1077         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
     1077        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10781078        cases (se_inv … EXEC0);
    10791079        @emb_initially_wrong
  • src/Clight/CexecSound.ma

    r744 r797  
    6464        cases (try_cast_null m i (Tint sz1 si1) t);
    6565        [ 1,3,5: #v'' #H' #e @H' @e
    66         | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
     66        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
    6767        ]
    6868    ]
     
    7474        cases (try_cast_null m i t ty');
    7575        [ 1,3,5: #v'' #H' #e @H' @e
    76         | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
     76        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
    7777        ]
    7878  ]
     
    303303    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
    304304    >H' #H'' @H''
    305 | #_ whd @I
     305| #msg #_ whd @I
    306306] qed.
    307307
     
    351351      @opt_bind_OK #m' #STORE
    352352      lapply (refl ? (exec_bind_parameters en m' ps' vs))
    353       cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #_ %]
     353      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]
    354354      #m'' #BIND
    355355      @(bind_parameters_cons … GET STORE)
     
    394394              [ % // | @(bool_of … Hb) ]
    395395            ]
    396         | #_ //;
     396        | #msg #_ //;
    397397        ]
    398398    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
  • src/Clight/Csyntax.ma

    r747 r797  
    517517Open Local Scope string_scope.
    518518*)
     519axiom UnknownField : String.
     520
    519521let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
    520522                              on fld : res nat ≝
    521523  match fld with
    522   [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
     524  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
    523525  | Fcons id' t fld' ⇒
    524526      match ident_eq id id' with
     
    533535let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
    534536  match fld with
    535   [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
     537  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
    536538  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
    537539  ].
  • src/Clight/test/insertsort.ma

    r781 r797  
    202202  (do s ← exec_up_to clight_fullexec myprog 1000
    203203     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    204    match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? ]) = OK ?
     204   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? [ ] ]) = OK ?
    205205[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    206206 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
     
    221221   do s ← exec_up_to clight_fullexec p 1000
    222222     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    223    match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? ]) = OK ?
     223   match s with [ finished t _ _ ⇒ OK ? (remove_costs t) | _ ⇒ Error ? [ ] ]) = OK ?
    224224[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    225225 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
  • src/Clight/test/io.ma

    r731 r797  
    2323example exec:
    2424 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
    25   match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
     25  match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
    2626 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2727normalize  (* you can examine the result here *)
  • src/Clight/test/io2.ma

    r731 r797  
    3232example exec:
    3333 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
    34    match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
     34   match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
    3535 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
    3636normalize  (* you can examine the result here *)
  • 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;
  • src/RTLabs/debug.ma

    r775 r797  
    77| Ret : ministate
    88| NoInput : ministate
    9 | Fail : ministate
     9| Fail : errmsg → ministate
    1010| MissingStmt : ministate
    1111| Done : int → ministate
     
    2424[ O ⇒ match e with [ e_step tr s _ ⇒ [mk_ministate s]
    2525                   | e_stop tr r m ⇒ [Done r]
    26                    | _ ⇒ [Fail]
     26                   | e_interact o k ⇒ [Fail (msg StoppedMidIO)]
     27                   | e_wrong m ⇒ [Fail m]
    2728                   ]
    2829| S m ⇒ match e with [ e_step tr s e' ⇒ (mk_ministate s)::(debug_up_to_aux m input e')
     
    3334                         | cons h tl ⇒ match get_input o h with
    3435                                       [ OK i ⇒ debug_up_to_aux m tl (k i)
    35                                        | _ ⇒ [Fail]
     36                                       | Error m ⇒ [Fail m]
    3637                                       ]
    3738                         ]
    38                      | e_wrong ⇒ [Fail]
     39                     | e_wrong m ⇒ [Fail m]
    3940                     ]
    4041].
  • src/RTLabs/import.ma

    r765 r797  
    4949                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
    5050
     51axiom MissingRegister : String.
     52axiom MissingLabel : String.
     53
    5154definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
    5255λpre_f.
     
    6366  do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
    6467  let 〈rmap4, rgen4〉 ≝ rmapgen4 in
    65   let rmap ≝ λn. opt_to_res … (rmap4 n) in
     68  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap4 n) in
    6669  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    6770  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
    68   let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
     71  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    6972  do graph ← foldr ?? (λp,g0. do g ← g0;
    7073                              let 〈l,s〉 ≝ p in
  • 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
  • src/common/Animation.ma

    r731 r797  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
    13 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
    14 | ASTptr _ ⇒ Error ?
     12[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     13| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
     14| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
    1515].
    1616
     
    2020| input_exhausted : trace → snapshot state.
    2121
     22axiom StoppedMidIO : String.
     23
    2224let rec up_to_nth_step (n:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (t:trace) : res (snapshot (state ?? ex)) ≝
    2325match n with
    2426[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
    2527                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    26                    | _ ⇒ Error ? ]
     28                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
     29                   | e_wrong m ⇒ Error ? m ]
    2730| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
    2831                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
     
    3336                                       up_to_nth_step m ex tl (k i) t
    3437                         ]
    35                      | e_wrong ⇒ Error ?
     38                     | e_wrong m ⇒ Error ? m
    3639                     ]
    3740].
  • src/common/Errors.ma

    r764 r797  
    1717include "basics/logic.ma".
    1818include "basics/list.ma".
     19include "common/PreIdentifiers.ma".
    1920
    2021(* * Error reporting and the error monad. *)
    21 (*
    22 (** * Representation of error messages. *)
    23 
    24 (** Compile-time errors produce an error message, represented in Coq
     22
     23(* * * Representation of error messages. *)
     24
     25(* * Compile-time errors produce an error message, represented in Coq
    2526  as a list of either substrings or positive numbers encoding
    2627  a source-level identifier (see module AST). *)
    2728
    28 Inductive errcode: Type :=
    29   | MSG: string -> errcode
    30   | CTX: positive -> errcode.
    31 
    32 Definition errmsg: Type := list errcode.
    33 
    34 Definition msg (s: string) : errmsg := MSG s :: nil.
    35 *)
     29inductive errcode: Type[0] :=
     30  | MSG: String → errcode
     31  | CTX: ∀tag:String. identifier tag → errcode.
     32
     33definition errmsg: Type[0] ≝ list errcode.
     34
     35definition msg : String → errmsg ≝ λs. [MSG s].
     36
    3637(* * * The error monad *)
    3738
     
    4243inductive res (A: Type[0]) : Type[0] ≝
    4344| OK: A → res A
    44 | Error: (* FIXME errmsg →*) res A.
     45| Error: errmsg → res A.
    4546
    4647(*Implicit Arguments Error [A].*)
     
    5253  match f with
    5354  [ OK x ⇒ g x
    54   | Error (*msg*) ⇒ Error ? (*msg*)
     55  | Error msg ⇒ Error ? msg
    5556  ].
    5657
     
    5859  match f with
    5960  [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
    60   | Error (*msg*) => Error ? (*msg*)
     61  | Error msg => Error ? msg
    6162  ].
    6263
     
    6465  match f with
    6566  [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]
    66   | Error (*msg*) => Error ? (*msg*)
     67  | Error msg => Error ? msg
    6768  ].
    6869 
     
    103104#A #B #f #g #y cases f;
    104105[ #a #e %{a} whd in e:(??%?); /2/;
    105 | #H whd in H:(??%?); destruct (H);
     106| #m #H whd in H:(??%?); destruct (H);
    106107] qed.
    107108
     
    112113#A #B #C #f #g #z cases f;
    113114[ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
    114 | #H whd in H:(??%?); destruct
     115| #m #H whd in H:(??%?); destruct
    115116] qed.
    116117
     
    207208
    208209
    209 definition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
    210 lemma opt_OK: ∀A,P,e.
     210definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
     211lemma opt_OK: ∀A,m,P,e.
    211212  (∀v. e = Some ? v → P v) →
    212   match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
    213 #A #P #e elim e; /2/;
     213  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
     214#A #m #P #e elim e; /2/;
    214215qed.
  • src/common/Globalenvs.ma

    r758 r797  
    483483(* init *)
    484484
     485axiom InitDataStoreFailed : String.
     486
    485487definition add_globals : ∀F,V:Type[0].
    486488       genv F × mem → list (ident × (list init_data) × region × V) →
     
    495497        match alloc_init_data st init r with [ pair st' b ⇒
    496498          let g' ≝ add_symbol ? id b g in
    497           do st'' ← opt_to_res ? (store_init_data_list F g' st' b OZ init);
     499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    498500            OK ? 〈g', st''〉
    499501        ] ] ] ])
  • src/common/IO.ma

    r731 r797  
    2020#ty cases ty; normalize; // * *; qed.
    2121
     22axiom IllTypedEvent : String.
     23
    2224definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
    2325λev,ty.
    2426match ty with
    25 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
    26 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
    27 | _ ⇒ Error ?
     27[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)]
     28| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)]
     29| _ ⇒ Error ? (msg IllTypedEvent)
    2830].
    2931
     
    3133λv,ty.
    3234match ty with
    33 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    34 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    35 | _ ⇒ Error ?
     35[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ]
     36| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]
     37| _ ⇒ Error ? (msg IllTypedEvent)
    3638].
    3739
    3840let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    3941match vs with
    40 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
     42[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ]
    4143| cons v vt ⇒
    4244  match tys with
    43   [ nil ⇒ Error ?
     45  [ nil ⇒ Error ? (msg IllTypedEvent)
    4446  | cons ty tyt ⇒
    4547    do ev ← check_eventval' v ty;
  • src/common/IOMonad.ma

    r700 r797  
    77| Interact : ∀o:output. (input o → IO output input T) → IO output input T
    88| Value : T → IO output input T
    9 | Wrong : IO output input T.
     9| Wrong : errmsg → IO output input T.
    1010
    1111let rec bindIO (O:Type[0]) (I:O → Type[0]) (T,T':Type[0]) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝
     
    1313[ Interact out k ⇒ (Interact ??? out (λres. bindIO O I T T' (k res) f))
    1414| Value v' ⇒ (f v')
    15 | Wrong ⇒ Wrong O I T'
     15| Wrong m ⇒ Wrong O I T' m
    1616].
    1717
     
    2020[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
    2121| Value v' ⇒ match v' with [ pair v1 v2 ⇒ f v1 v2 ]
    22 | Wrong ⇒ Wrong ?? T'
     22| Wrong m ⇒ Wrong ?? T' m
    2323].
    2424
    2525definition err_to_io : ∀O,I,T. res T → IO O I T ≝
    26 λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error ⇒ Wrong O I T ].
     26λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ].
    2727coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
    2828definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    29 λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error ⇒ Wrong O I (Sig T P) ].
     29λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
    3030(*coercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (Sig A P).IO O I (Sig A P) ≝ err_to_io_sig on _c:res (Sig ??) to IO ?? (Sig ??).*)
    3131
     
    4545let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    4646match v return λ_.Prop with
    47 [ Wrong ⇒ True
     47[ Wrong _ ⇒ True
    4848| Value z ⇒ P z
    4949| Interact out k ⇒ ∀v'.P_io O I A P (k v')
     
    5252let rec P_io' O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    5353match v return λ_.Prop with
    54 [ Wrong ⇒ False
     54[ Wrong _ ⇒ False
    5555| Value z ⇒ P z
    5656| Interact out k ⇒ ∀v'.P_io' O I A P (k v')
     
    6565let rec io_inject_0 O I (A:Type[0]) (P:A → Prop) (a:IO O I A) (p:P_io O I A P a) on a : IO O I (Sig A P) ≝
    6666(match a return λa'.P_io O I A P a' → ? with
    67  [ Wrong ⇒ λ_. Wrong O I ?
     67 [ Wrong m ⇒ λ_. Wrong O I ? m
    6868 | Value c ⇒ λp'. Value ??? (dp A P c p')
    6969 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
     
    8080let rec io_eject O I (A:Type[0]) (P: A → Prop) (a:IO O I (Sig A P)) on a : IO O I A ≝
    8181match a with
    82 [ Wrong ⇒ Wrong ???
     82[ Wrong m ⇒ Wrong ??? m
    8383| Value b ⇒ match b with [ dp w p ⇒ Value ??? w]
    8484| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
     
    9191  on _c:IO ?? (Sig ? ?) to IO ???.
    9292
    93 definition opt_to_io : ∀O,I,T.option T → IO O I T ≝
    94 λO,I,T,v. match v with [ None ⇒ Wrong ?? T | Some v' ⇒ Value ??? v' ].
    95 coercion opt_to_io : ∀O,I,T.∀v:option T. IO O I T ≝ opt_to_io on _v:option ? to IO ???.
     93definition opt_to_io : ∀O,I,T.errmsg → option T → IO O I T ≝
     94λO,I,T,m,v. match v with [ None ⇒ Wrong ?? T m | Some v' ⇒ Value ??? v' ].
    9695
    9796lemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (Sig A P). ∀f:Sig A P → IO O I B.
     
    113112] qed.
    114113
    115 lemma opt_bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
     114lemma opt_bindIO_OK: ∀O,I,A,B,m. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
    116115  (∀v:A. e = Some A v → P_io O I ? P (f v)) →
    117   P_io O I ? P (bindIO O I A B e f).
    118 #I #O #A #B #P #e elim e; //; #v #f #H @H //;
     116  P_io O I ? P (bindIO O I A B (opt_to_io ??? m e) f).
     117#I #O #A #B #m #P #e elim e; //; #v #f #H @H //;
    119118qed.
    120119
    121 lemma opt_bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
     120lemma opt_bindIO2_OK: ∀O,I,A,B,C,m. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
    122121  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
    123   P_io O I ? P (bindIO2 O I A B C e f).
    124 #I #O #A #B #C #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
     122  P_io O I ? P (bindIO2 O I A B C (opt_to_io ??? m e) f).
     123#I #O #A #B #C #m #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
    125124qed.
    126125
     
    185184    @ext @IH
    186185| #v @refl
    187 | @refl
     186| #m @refl
    188187] qed.
    189188
  • src/common/Identifiers.ma

    r782 r797  
    88   provide extra type checking. *)
    99
     10(* in common/PreIdentifiers.ma, via Errors.ma.
    1011inductive identifier (tag:String) : Type[0] ≝
    1112  an_identifier : Word → identifier tag.
    12  
     13*)
     14
    1315record universe (tag:String) : Type[0] ≝
    1416  { next_identifier : Word }.
     
    1719definition new_universe : ∀tag:String. universe tag ≝
    1820  λtag. mk_universe tag (zero ?).
    19  
     21
     22axiom OutOfIdentifiers : String.
     23
    2024definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
    2125λtag,g.
    2226  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
    23     if get_index_v ?? carries 0 ? then Error ? else
     27    if get_index_v ?? carries 0 ? then Error ? (msg OutOfIdentifiers) else
    2428      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
    2529// qed.
     
    7478                                           (match m with [ an_id_map m' ⇒ m' ])).
    7579
     80axiom MissingId : String.
     81
    7682(* Only updates an existing entry; fails with an error otherwise. *)
    7783definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
     
    7985  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
    8086                    (match m with [ an_id_map m' ⇒ m' ]) with
    81   [ None ⇒ Error ? (* missing identifier *)
     87  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
    8288  | Some m' ⇒ OK ? (an_id_map tag A m')
    8389  ].
  • src/common/SmallstepExec.ma

    r751 r797  
    3737| e_stop : trace → int → mem → execution state output input
    3838| e_step : trace → state → execution state output input → execution state output input
    39 | e_wrong : execution state output input
     39| e_wrong : errmsg → execution state output input
    4040| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
    4141
     
    4949                       : execution ??? ≝
    5050match s with
    51 [ Wrong ⇒ e_wrong ???
     51[ Wrong m ⇒ e_wrong ??? m
    5252| Value v ⇒ match v with [ pair t s' ⇒
    5353    match is_final ?? exec s' with
     
    6060 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
    6161 | e_step tr s e ⇒ e_step ??? tr s e
    62  | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
     62 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
    6363#o #i #s #e cases e; //; qed.
    6464
    6565axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
    6666match s with
    67 [ Wrong ⇒ e_wrong ???
     67[ Wrong m ⇒ e_wrong ??? m
    6868| Value v ⇒ match v with [ pair t s' ⇒
    6969    match is_final ?? exec s' with
     
    9191  match make_initial_state ?? fx p with
    9292  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
    93   | _ ⇒ e_wrong ???
     93  | Error m ⇒ e_wrong ??? m
    9494  ].
    9595
  • src/common/Values.ma

    r751 r797  
    156156
    157157notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
    158 
     158(*
    159159let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
    160160match m return λx.res (x = n) with
     
    212212].
    213213   
    214 
     214*)
    215215(*
    216216(** The module [Val] defines a number of arithmetic and logical operations
     
    266266      ∀r. bool_of_val (Vnull r) true.
    267267
     268axiom ValueNotABoolean : String.
     269
    268270definition eval_bool_of_val : val → res bool ≝
    269271λv. match v with
     
    271273| Vnull _ ⇒ OK ? false
    272274| Vptr _ _ _ _ ⇒ OK ? true
    273 | _ ⇒ Error ?
     275| _ ⇒ Error ? (msg ValueNotABoolean)
    274276].
    275277
Note: See TracChangeset for help on using the changeset viewer.