Changeset 797 for src/Clight/Cexec.ma


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (10 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.