aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/AsmToJSON.ml2
-rw-r--r--backend/Cminortyping.v47
-rw-r--r--backend/Selectionaux.ml13
-rw-r--r--backend/Selectionproof.v4
-rw-r--r--cparser/Elab.ml8
5 files changed, 65 insertions, 9 deletions
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index dfad6972..6ba3f1bc 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -29,7 +29,7 @@ let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "
"Pfsts"; "Pfsubd"; "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd";
"Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr";
"Ploadsymbol_lbl"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb";
- "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite";
+ "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; "Pfmovite";
"Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Ploadsymbol_imm"; "Pnop"; "Porr";
"Ppush"; "Prev"; "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull";
"Pstr"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv";
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index ddd0f98b..c0b7af78 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -124,11 +124,10 @@ Definition type_assign (e: S.typenv) (id: ident) (a: expr) : res S.typenv :=
S.set e1 id (type_of_chunk chunk)
end.
-Definition opt_set (e: S.typenv) (optid: option ident) (optty: option typ) : res S.typenv :=
- match optid, optty with
- | None, _ => OK e
- | Some id, Some ty => S.set e id ty
- | _, _ => Error (msg "inconsistent call")
+Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv :=
+ match optid with
+ | None => OK e
+ | Some id => S.set e id ty
end.
Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
@@ -140,7 +139,11 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
| Scall optid sg fn args =>
do e1 <- type_expr e fn Tptr;
do e2 <- type_exprlist e1 args sg.(sig_args);
+<<<<<<< HEAD
opt_set e2 optid sg.(sig_res)
+=======
+ opt_set e2 optid (proj_sig_res sg)
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
| Stailcall sg fn args =>
assertion (opt_typ_eq sg.(sig_res) tret);
do e1 <- type_expr e fn Tptr;
@@ -148,7 +151,11 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
| Sbuiltin optid ef args =>
let sg := ef_sig ef in
do e1 <- type_exprlist e args sg.(sig_args);
+<<<<<<< HEAD
opt_set e1 optid sg.(sig_res)
+=======
+ opt_set e1 optid (proj_sig_res sg)
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
| Sseq s1 s2 =>
do e1 <- type_stmt tret e s1; type_stmt tret e1 s2
| Sifthenelse a s1 s2 =>
@@ -164,9 +171,15 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
| Sswitch sz a tbl dfl =>
type_expr e a (if sz then Tlong else Tint)
| Sreturn opta =>
+<<<<<<< HEAD
match tret, opta with
| None, None => OK e
| Some t, Some a => type_expr e a t
+=======
+ match opta, tret with
+ | None, _ => OK e
+ | Some a, Some t => type_expr e a t
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
| _, _ => Error (msg "inconsistent return")
end
| Slabel lbl s1 =>
@@ -207,7 +220,14 @@ Inductive wt_expr: expr -> typ -> Prop :=
wt_expr (Eload chunk a1) (type_of_chunk chunk).
Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop :=
+<<<<<<< HEAD
match optid with Some id => optty = Some (env id) | _ => True end.
+=======
+ match optid with
+ | Some id => match optty with Some ty => ty | None => Tint end = env id
+ | _ => True
+ end.
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
Inductive wt_stmt: stmt -> Prop :=
| wt_Sskip:
@@ -248,7 +268,10 @@ Inductive wt_stmt: stmt -> Prop :=
wt_expr a (if sz then Tlong else Tint) ->
wt_stmt (Sswitch sz a tbl dfl)
| wt_Sreturn_none:
+<<<<<<< HEAD
tret = None ->
+=======
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
wt_stmt (Sreturn None)
| wt_Sreturn_some: forall a t,
tret = Some t -> wt_expr a t ->
@@ -359,12 +382,22 @@ Proof.
Qed.
Hint Resolve opt_set_incr: ty.
+<<<<<<< HEAD
Lemma opt_set_sound: forall te optid optty e e',
opt_set e optid optty = OK e' -> S.satisf te e' -> wt_opt_assign te optid optty.
Proof.
unfold opt_set; intros; red. destruct optid; [destruct optty |]; try (monadInv H).
- erewrite S.set_sound by eauto. auto.
- auto.
+=======
+Lemma opt_set_sound: forall te optid sg e e',
+ opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' ->
+ wt_opt_assign te optid sg.(sig_res).
+Proof.
+ unfold opt_set; intros; red. destruct optid.
+- erewrite S.set_sound by eauto. auto.
+- inv H. auto.
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
Qed.
Lemma type_stmt_incr: forall te tret s e e',
@@ -660,7 +693,11 @@ Proof.
- inv WT_CONT. econstructor; eauto using wt_Sskip. inv H.
- inv WT_CONT. econstructor; eauto using wt_Sexit. inv H.
- econstructor; eauto using wt_Sexit.
+<<<<<<< HEAD
- inv WT_STMT. econstructor; eauto using call_cont_wt. rewrite H0; exact I.
+=======
+- inv WT_STMT. econstructor; eauto using call_cont_wt. exact I.
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
- inv WT_STMT. econstructor; eauto using call_cont_wt.
rewrite H2. eapply wt_eval_expr; eauto.
- inv WT_STMT. econstructor; eauto.
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index b25f1fa1..818660c1 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -96,8 +96,17 @@ If-conversion seems beneficial if:
Intuition: on a modern processor, the "then" and the "else" branches
can generally be computed in parallel, there is enough ILP for that.
So, the bad case is if the most taken branch is much cheaper than the
+<<<<<<< HEAD
other branch. Since our cost estimates are very imprecise, the
bound on the total cost acts as a safety guard,
+=======
+other branch. Another bad case is if both branches are big: since the
+code for one branch precedes entirely the code for the other branch,
+if the first branch contains a lot of instructions,
+dynamic reordering of instructions will not look ahead far enough
+to execute instructions from the other branch in parallel with
+instructions from the first branch.
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
*)
let if_conversion_heuristic cond ifso ifnot ty =
@@ -105,5 +114,9 @@ let if_conversion_heuristic cond ifso ifnot ty =
if !Clflags.option_ffavor_branchless then true else
if not (fast_cmove ty) then false else
let c1 = cost_expr ifso and c2 = cost_expr ifnot in
+<<<<<<< HEAD
c1 + c2 <= 30 && abs (c1 - c2) <= 8
+=======
+ c1 + c2 <= 24 && abs (c1 - c2) <= 8
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 40db5d4b..01635ff1 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1102,7 +1102,11 @@ Proof.
destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ];
intuition. apply IHs2; auto.
(* ifthenelse *)
+<<<<<<< HEAD
- destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC.
+=======
+ destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC.
+>>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a
inv SE. exploit if_conversion_nolabel; eauto. intros (A & B & C).
rewrite A, B, C. auto.
monadInv SE; simpl.
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 9cca930d..10380152 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -836,7 +836,7 @@ and elab_type_declarator ?(fundef = false) loc env ty = function
| Cabs.PROTO(d, (params, vararg)) ->
elab_return_type loc env ty;
let (ty, a) = get_nontype_attrs env ty in
- let (params', env') = elab_parameters env params in
+ let (params', env') = elab_parameters loc env params in
(* For a function declaration (fundef = false), the scope introduced
to treat parameters ends here, so we discard the extended
environment env' returned by elab_parameters.
@@ -862,13 +862,15 @@ and elab_type_declarator ?(fundef = false) loc env ty = function
(* Elaboration of parameters in a prototype *)
-and elab_parameters env params =
+and elab_parameters loc env params =
(* Prototype introduces a new scope *)
let (vars, env) = mmap elab_parameter (Env.new_scope env) params in
(* Catch special case f(t) where t is void or a typedef to void *)
match vars with
| [ ( {C.name=""}, t) ] when is_void_type env t -> [],env
- | _ -> vars,env
+ | _ -> if List.exists (fun (id, t) -> id.C.name = "" && is_void_type env t) vars then
+ error loc "'void' must be the only parameter";
+ (vars, env)
(* Elaboration of a function parameter *)
generated by cgit (git 2.34.1) at 2024-06-02 16:42:27 +0000