Changeset 797 for src/Clight


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.

Location:
src/Clight
Files:
8 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 *)
Note: See TracChangeset for help on using the changeset viewer.