Fix treatment of function pointers at function calls in the CompCert C and Clight semantics

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1680 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 19 insertions, 26 deletions

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 50be039..da8f668 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -433,11 +433,11 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f Sskip k e (PTree.set id v le) m)
 
   | step_call:   forall f optid a al k e le m tyargs tyres vf vargs fd,
-      typeof a = Tfunction tyargs tyres ->
+      classify_fun (typeof a) = fun_case_f tyargs tyres ->
       eval_expr e le m a vf ->
       eval_exprlist e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some fd ->
-      type_of_fundef fd = typeof a ->
+      type_of_fundef fd = Tfunction tyargs tyres ->
       step (State f (Scall optid a al) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
@@ -643,20 +643,20 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
       exec_stmt e le m (Sset id a)
                E0 (PTree.set id v le) m Out_normal      
   | exec_Scall_none:   forall e le m a al tyargs tyres vf vargs f t m' vres,
-      typeof a = Tfunction tyargs tyres ->
+      classify_fun (typeof a) = fun_case_f tyargs tyres ->
       eval_expr e le m a vf ->
       eval_exprlist e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
+      type_of_fundef f = Tfunction tyargs tyres ->
       eval_funcall m f vargs t m' vres ->
       exec_stmt e le m (Scall None a al)
                 t le m' Out_normal
   | exec_Scall_some:   forall e le m id a al tyargs tyres vf vargs f t m' vres,
-      typeof a = Tfunction tyargs tyres ->
+      classify_fun (typeof a) = fun_case_f tyargs tyres ->
       eval_expr e le m a vf ->
       eval_exprlist e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
+      type_of_fundef f = Tfunction tyargs tyres ->
       eval_funcall m f vargs t m' vres ->
       exec_stmt e le m (Scall (Some id) a al)
                 t (PTree.set id vres le) m' Out_normal
@@ -792,19 +792,19 @@ Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
 
 CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop :=
   | execinf_Scall_none:   forall e le m a al vf tyargs tyres vargs f t,
-      typeof a = Tfunction tyargs tyres ->
+      classify_fun (typeof a) = fun_case_f tyargs tyres ->
       eval_expr e le m a vf ->
       eval_exprlist e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
+      type_of_fundef f = Tfunction tyargs tyres ->
       evalinf_funcall m f vargs t ->
       execinf_stmt e le m (Scall None a al) t
   | execinf_Scall_some:   forall e le m id a al vf tyargs tyres vargs f t,
-      typeof a = Tfunction tyargs tyres ->
+      classify_fun (typeof a) = fun_case_f tyargs tyres ->
       eval_expr e le m a vf ->
       eval_exprlist e le m al tyargs vargs ->
       Genv.find_funct ge vf = Some f ->
-      type_of_fundef f = typeof a ->
+      type_of_fundef f = Tfunction tyargs tyres ->
       evalinf_funcall m f vargs t ->
       execinf_stmt e le m (Scall (Some id) a al) t
   | execinf_Sseq_1:   forall e le m s1 s2 t,
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 3a3ba3b..33d8e53 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -722,11 +722,12 @@ Inductive cast_arguments: exprlist -> typelist -> list val -> Prop :=
       cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl).
 
 Inductive callred: expr -> fundef -> list val -> type -> Prop :=
-  | red_Ecall: forall vf tyargs tyres el ty fd vargs,
+  | red_Ecall: forall vf tyf tyargs tyres el ty fd vargs,
       Genv.find_funct ge vf = Some fd ->
       cast_arguments el tyargs vargs ->
       type_of_fundef fd = Tfunction tyargs tyres ->
-      callred (Ecall (Eval vf (Tfunction tyargs tyres)) el ty)
+      classify_fun tyf = fun_case_f tyargs tyres ->
+      callred (Ecall (Eval vf tyf) el ty)
               fd vargs ty.
 
 (** Reduction contexts.  In accordance with C's nondeterministic semantics,
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 457f0d1..49d3ff3 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1525,11 +1525,10 @@ Proof.
   exploit transl_expr_correct; eauto.
   exploit transl_exprlist_correct; eauto.
   eapply transl_fundef_sig1; eauto.
-  rewrite H3. rewrite H. auto.
+  rewrite H3. auto.
   econstructor; eauto.  
   econstructor; eauto.
   simpl. auto.
-  rewrite H3; rewrite H; eauto. 
   eapply eval_exprlist_casted; eauto. 
 
 (* seq *)
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index fc97945..8dbf586 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -288,7 +288,7 @@ Inductive estep: state -> trace -> state -> Prop :=
 
   | step_call: forall f C rf rargs ty k e m targs tres vf vargs fd,
       leftcontext RV RV C ->
-      typeof rf = Tfunction targs tres ->
+      classify_fun (typeof rf) = fun_case_f targs tres ->
       eval_simple_rvalue e m rf vf ->
       eval_simple_list e m rargs targs vargs ->
       Genv.find_funct ge vf = Some fd ->
@@ -490,7 +490,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
   | Ecall (Eval vf tyf) rargs ty =>
       exprlist_all_values rargs ->
       exists tyargs, exists tyres, exists fd, exists vl,
-         tyf = Tfunction tyargs tyres
+         classify_fun tyf = fun_case_f tyargs tyres
       /\ Genv.find_funct ge vf = Some fd
       /\ cast_arguments rargs tyargs vl
       /\ type_of_fundef fd = Tfunction tyargs tyres
@@ -1209,7 +1209,7 @@ Proof.
   econstructor; split.
   eapply step_call with (C := C); eauto. eapply can_eval_simple_list; eauto.
   eapply plus_right. eapply star_trans; eauto. 
-  left. econstructor. rewrite U. econstructor; eauto. 
+  left. econstructor. econstructor; eauto. 
   eapply safe_not_stuck; eauto. apply leftcontext_context; auto.
   traceEq.
 (* rparen *)
@@ -1537,7 +1537,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop :=
       eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' ->
       eval_simple_rvalue ge e m2 rf' vf ->
       eval_simple_list ge e m2 rargs' targs vargs ->
-      typeof rf = Tfunction targs tres ->
+      classify_fun (typeof rf) = fun_case_f targs tres ->
       Genv.find_funct ge vf = Some fd ->
       type_of_fundef fd = Tfunction targs tres ->
       eval_funcall m2 fd vargs t3 m3 vres ->
@@ -1775,7 +1775,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop :=
       eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' ->
       eval_simple_rvalue ge e m2 rf' vf ->
       eval_simple_list ge e m2 rargs' targs vargs ->
-      typeof rf = Tfunction targs tres ->
+      classify_fun (typeof rf) = fun_case_f targs tres ->
       Genv.find_funct ge vf = Some fd ->
       type_of_fundef fd = Tfunction targs tres ->
       evalinf_funcall m2 fd vargs t3 ->
@@ -1971,13 +1971,6 @@ Lemma bigstep_to_steps:
 /\(forall e m s t m' out,
    exec_stmt e m s t m' out ->
    forall f k,
-(*
-   match out with
-   | Out_return None => fn_return f = Tvoid
-   | Out_return (Some(v, ty)) => fn_return f <> Tvoid
-   | _ => True
-   end ->
-*)
    exists S,
    star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S)
 /\(forall m fd args t m' res,