diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-10 10:30:16 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-10 10:30:16 +0100 |
commit | e37e366c826a0dc422e449b9ad0afa70be204e12 (patch) | |
tree | 3bcc0c14099862614d19c95fee0edc7b388720b3 | |
parent | 8aae10b50b321cfcbde86582cdd7ce1df8960628 (diff) | |
parent | 3e01154d693e1c457e1e974f5e9ebaa4601050aa (diff) | |
download | compcert-e37e366c826a0dc422e449b9ad0afa70be204e12.tar.gz compcert-e37e366c826a0dc422e449b9ad0afa70be204e12.zip |
Merge branch 'master' into dwarf
33 files changed, 1612 insertions, 606 deletions
@@ -39,6 +39,7 @@ cparser/Parser.v cparser/Lexer.ml cparser/pre_parser.ml cparser/pre_parser.mli +lib/Readconfig.ml lib/Tokenize.ml # Documentation doc/coq2html @@ -174,15 +174,15 @@ doc/coq2html.ml: doc/coq2html.mll ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC) + ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml tools/modorder: tools/modorder.ml - ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC) + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) %.vo: %.v - @rm -f doc/glob/$(*F).glob + @rm -f doc/$(*F).glob @echo "COQC $*.v" @$(COQC) -dump-glob doc/$(*F).glob $*.v diff --git a/Makefile.extr b/Makefile.extr index f5f7e7b4..4e17e904 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -61,7 +61,7 @@ endif OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS) OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS) -OCAMLDEP=ocamldep$(DOTOPT) $(INCLUDES) +OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES) # Compilers used for Camlp4-preprocessed code. Note that we cannot # use the .opt compilers (because ocamlfind doesn't support them). @@ -75,9 +75,11 @@ OCAMLLEX=ocamllex -q MODORDER=tools/modorder .depend.extr PARSERS=backend/CMparser.mly cparser/pre_parser.mly -LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll +LEXERS=backend/CMlexer.mll cparser/Lexer.mll \ + lib/Tokenize.mll lib/Readconfig.mll -LIBS=str.cmxa +LIBS=str.cmxa unix.cmxa +CHECKLINK_LIBS=str.cmxa EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) @@ -90,11 +92,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ccomp: $(CCOMP_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC) + @$(OCAMLOPT) -o $@ $(LIBS) $+ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC) + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ ifeq ($(CCHECKLINK),true) @@ -102,11 +104,11 @@ CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx) cchecklink: $(CCHECKLINK_OBJS) @echo "Linking $@" - @$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+ + @$(OCAMLOPT_P4) -linkpkg -o $@ $(CHECKLINK_LIBS) $+ cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+ + @$(OCAMLC_P4) -linkpkg -o $@ $(CHECKLINK_LIBS:.cmxa=.cma) $+ endif @@ -156,17 +158,14 @@ clean: rm -f $(GENERATED) for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done -cleansource: - rm -f $(EXECUTABLES) - for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done - # Generation of .depend.extr depend: $(GENERATED) @echo "Analyzing OCaml dependencies" - @for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr + @$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) >.depend.extr + @$(OCAMLDEP) $(GENERATED) >> .depend.extr ifneq ($(strip $(DIRS_P4)),) - @for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr + @$(OCAMLDEP_P4) $(foreach d,$(DIRS_P4),$(wildcard $(d)/*.mli $(d)/*.ml)) >>.depend.extr endif diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 952d148d..ed67286f 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -12,6 +12,7 @@ (** Animating the CompCert C semantics *) +Require Import String. Require Import Axioms. Require Import Classical. Require Import Coqlib. @@ -31,6 +32,9 @@ Require Import Csyntax. Require Import Csem. Require Cstrategy. +Local Open Scope string_scope. +Local Open Scope list_scope. + (** Error monad with options or lists *) Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) @@ -661,9 +665,9 @@ Qed. (** * Reduction of expressions *) Inductive reduction: Type := - | Lred (l': expr) (m': mem) - | Rred (r': expr) (m': mem) (t: trace) - | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem) + | Lred (rule: string) (l': expr) (m': mem) + | Rred (rule: string) (r': expr) (m': mem) (t: trace) + | Callred (rule: string) (fd: fundef) (args: list val) (tyres: type) (m': mem) | Stuckred. Section EXPRS. @@ -728,15 +732,15 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match e!x with | Some(b, ty') => check type_eq ty ty'; - topred (Lred (Eloc b Int.zero ty) m) + topred (Lred "red_var_local" (Eloc b Int.zero ty) m) | None => do b <- Genv.find_symbol ge x; - topred (Lred (Eloc b Int.zero ty) m) + topred (Lred "red_var_global" (Eloc b Int.zero ty) m) end | LV, Ederef r ty => match is_val r with | Some(Vptr b ofs, ty') => - topred (Lred (Eloc b ofs ty) m) + topred (Lred "red_deref" (Eloc b ofs ty) m) | Some _ => stuck | None => @@ -750,11 +754,11 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do co <- ge.(genv_cenv)!id; match field_offset ge f (co_members co) with | Error _ => stuck - | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) + | OK delta => topred (Lred "red_field_struct" (Eloc b (Int.add ofs (Int.repr delta)) ty) m) end | Tunion id _ => do co <- ge.(genv_cenv)!id; - topred (Lred (Eloc b ofs ty) m) + topred (Lred "red_field_union" (Eloc b ofs ty) m) | _ => stuck end | Some _ => @@ -769,20 +773,20 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | Some(b, ofs, ty') => check type_eq ty ty'; do w',t,v <- do_deref_loc w ty m b ofs; - topred (Rred (Eval v ty) m t) + topred (Rred "red_rvalof" (Eval v ty) m t) | None => incontext (fun x => Evalof x ty) (step_expr LV l m) end | RV, Eaddrof l ty => match is_loc l with - | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m E0) + | Some(b, ofs, ty') => topred (Rred "red_addrof" (Eval (Vptr b ofs) ty) m E0) | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m) end | RV, Eunop op r1 ty => match is_val r1 with | Some(v1, ty1) => do v <- sem_unary_operation op v1 ty1; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_unop" (Eval v ty) m E0) | None => incontext (fun x => Eunop op x ty) (step_expr RV r1 m) end @@ -790,7 +794,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1, is_val r2 with | Some(v1, ty1), Some(v2, ty2) => do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_binop" (Eval v ty) m E0) | _, _ => incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) (fun x => Ebinop op r1 x ty) (step_expr RV r2 m) @@ -799,7 +803,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do v <- sem_cast v1 ty1 ty; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_cast" (Eval v ty) m E0) | None => incontext (fun x => Ecast x ty) (step_expr RV r1 m) end @@ -807,8 +811,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - if b then topred (Rred (Eparen r2 type_bool ty) m E0) - else topred (Rred (Eval (Vint Int.zero) ty) m E0) + if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0) + else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0) | None => incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m) end @@ -816,8 +820,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - if b then topred (Rred (Eval (Vint Int.one) ty) m E0) - else topred (Rred (Eparen r2 type_bool ty) m E0) + if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0) + else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0) | None => incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m) end @@ -825,21 +829,21 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - topred (Rred (Eparen (if b then r2 else r3) ty ty) m E0) + topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0) | None => incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) end | RV, Esizeof ty' ty => - topred (Rred (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) + topred (Rred "red_sizeof" (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) | RV, Ealignof ty' ty => - topred (Rred (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) + topred (Rred "red_alignof" (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) | RV, Eassign l1 r2 ty => match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => check type_eq ty1 ty; do v <- sem_cast v2 ty2 ty1; do w',t,m' <- do_assign_loc w ty1 m b ofs v; - topred (Rred (Eval v ty) m' t) + topred (Rred "red_assign" (Eval v ty) m' t) | _, _ => incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m) (fun x => Eassign l1 x ty) (step_expr RV r2 m) @@ -851,7 +855,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do w',t,v1 <- do_deref_loc w ty1 m b ofs; let r' := Eassign (Eloc b ofs ty1) (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1 in - topred (Rred r' m t) + topred (Rred "red_assignop" r' m t) | _, _ => incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m) (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m) @@ -867,7 +871,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (incrdecr_type ty)) ty) (Eval v1 ty) ty in - topred (Rred r' m t) + topred (Rred "red_postincr" r' m t) | None => incontext (fun x => Epostincr id x ty) (step_expr LV l m) end @@ -875,7 +879,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some _ => check type_eq (typeof r2) ty; - topred (Rred r2 m E0) + topred (Rred "red_comma" r2 m E0) | None => incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m) end @@ -883,7 +887,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some (v1, ty1) => do v <- sem_cast v1 ty1 tycast; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_paren" (Eval v ty) m E0) | None => incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m) end @@ -895,7 +899,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do fd <- Genv.find_funct ge vf; do vargs <- sem_cast_arguments vtl tyargs; check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv); - topred (Callred fd vargs ty m) + topred (Callred "red_call" fd vargs ty m) | _ => stuck end | _, _ => @@ -908,7 +912,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do vargs <- sem_cast_arguments vtl tyargs; match do_external ef w vargs m with | None => stuck - | Some(w',t,v,m') => topred (Rred (Eval v ty) m' t) + | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t) end | _ => incontext (fun x => Ebuiltin ef tyargs x ty) (step_exprlist rargs m) @@ -956,21 +960,6 @@ Proof. eapply imm_safe_callred; eauto. Qed. -(* -Definition not_stuck (a: expr) (m: mem) := - forall a' k C, context k RV C -> a = C a' -> imm_safe_t k a' m. - -Lemma safe_expr_kind: - forall k C a m, - context k RV C -> - not_stuck (C a) m -> - k = Cstrategy.expr_kind a. -Proof. - intros. - symmetry. eapply Cstrategy.imm_safe_kind. eapply imm_safe_t_imm_safe. eauto. -Qed. -*) - Fixpoint exprlist_all_values (rl: exprlist) : Prop := match rl with | Enil => True @@ -1163,9 +1152,9 @@ Hint Resolve context_compose contextlist_compose. Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop := match k, rd with - | LV, Lred l' m' => lred ge e a m l' m' - | RV, Rred r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' - | RV, Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m + | LV, Lred _ l' m' => lred ge e a m l' m' + | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' + | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m | LV, Stuckred => ~imm_safe_t k a m | RV, Stuckred => ~imm_safe_t k a m | _, _ => False @@ -1521,7 +1510,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (Genv.find_funct ge vf) as [fd|] eqn:?... destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))... - apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. + apply topred_ok; auto. red. split; auto. eapply red_call; eauto. eapply sem_cast_arguments_sound; eauto. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. @@ -1583,73 +1572,77 @@ Qed. Lemma lred_topred: forall l1 m1 l2 m2, lred ge e l1 m1 l2 m2 -> - step_expr LV l1 m1 = topred (Lred l2 m2). + exists rule, step_expr LV l1 m1 = topred (Lred rule l2 m2). Proof. induction 1; simpl. (* var local *) - rewrite H. rewrite dec_eq_true; auto. + rewrite H. rewrite dec_eq_true. econstructor; eauto. (* var global *) - rewrite H; rewrite H0. auto. + rewrite H; rewrite H0. econstructor; eauto. (* deref *) - auto. + econstructor; eauto. (* field struct *) - rewrite H, H0; auto. + rewrite H, H0; econstructor; eauto. (* field union *) - rewrite H; auto. + rewrite H; econstructor; eauto. Qed. Lemma rred_topred: forall w' r1 m1 t r2 m2, rred ge r1 m1 t r2 m2 -> possible_trace w t w' -> - step_expr RV r1 m1 = topred (Rred r2 m2 t). + exists rule, step_expr RV r1 m1 = topred (Rred rule r2 m2 t). Proof. induction 1; simpl; intros. (* valof *) - rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. + rewrite dec_eq_true. + rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). econstructor; eauto. (* addrof *) - inv H. auto. + inv H. econstructor; eauto. (* unop *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* binop *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* cast *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* seqand *) - inv H0. rewrite H; auto. - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. + inv H0. rewrite H; econstructor; eauto. (* seqor *) - inv H0. rewrite H; auto. - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. + inv H0. rewrite H; econstructor; eauto. (* condition *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* sizeof *) - inv H. auto. + inv H. econstructor; eauto. (* alignof *) - inv H. auto. + inv H. econstructor; eauto. (* assign *) - rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto. + rewrite dec_eq_true. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). + econstructor; eauto. (* assignop *) - rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. + rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). + econstructor; eauto. (* postincr *) - rewrite dec_eq_true; auto. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). auto. + rewrite dec_eq_true. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). + econstructor; eauto. (* comma *) - inv H0. rewrite dec_eq_true; auto. + inv H0. rewrite dec_eq_true. econstructor; eauto. (* paren *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* builtin *) exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. exploit do_ef_external_complete; eauto. intros C. - rewrite A. rewrite B. rewrite C. auto. + rewrite A. rewrite B. rewrite C. econstructor; eauto. Qed. Lemma callred_topred: forall a fd args ty m, callred ge a fd args ty -> - step_expr RV a m = topred (Callred fd args ty m). + exists rule, step_expr RV a m = topred (Callred rule fd args ty m). Proof. induction 1; simpl. rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. - rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto. + rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. econstructor; eauto. Qed. Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop := @@ -1956,44 +1949,54 @@ Proof. simpl. auto. Qed. +Inductive transition : Type := TR (rule: string) (t: trace) (S': state). + Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) := match snd C_rd with - | Lred a m => (E0, ExprState f (fst C_rd a) k e m) - | Rred a m t => (t, ExprState f (fst C_rd a) k e m) - | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m) - | Stuck => (E0, Stuckstate) + | Lred rule a m => TR rule E0 (ExprState f (fst C_rd a) k e m) + | Rred rule a m t => TR rule t (ExprState f (fst C_rd a) k e m) + | Callred rule fd vargs ty m => TR rule E0 (Callstate fd vargs (Kcall f e (fst C_rd) ty k) m) + | Stuckred => TR "step_stuck" E0 Stuckstate end. Local Open Scope list_monad_scope. -Definition ret (S: state) : list (trace * state) := (E0, S) :: nil. +Definition ret (rule: string) (S: state) : list transition := + TR rule E0 S :: nil. -Definition do_step (w: world) (s: state) : list (trace * state) := +Definition do_step (w: world) (s: state) : list transition := match s with | ExprState f a k e m => match is_val a with | Some(v, ty) => match k with - | Kdo k => ret (State f Sskip k e m ) + | Kdo k => ret "step_do_2" (State f Sskip k e m ) | Kifthenelse s1 s2 k => - do b <- bool_val v ty; ret (State f (if b then s1 else s2) k e m) + do b <- bool_val v ty; + ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m) | Kwhile1 x s k => do b <- bool_val v ty; - if b then ret (State f s (Kwhile2 x s k) e m) else ret (State f Sskip k e m) + if b + then ret "step_while_true" (State f s (Kwhile2 x s k) e m) + else ret "step_while_false" (State f Sskip k e m) | Kdowhile2 x s k => do b <- bool_val v ty; - if b then ret (State f (Sdowhile x s) k e m) else ret (State f Sskip k e m) + if b + then ret "step_dowhile_true" (State f (Sdowhile x s) k e m) + else ret "step_dowhile_false" (State f Sskip k e m) | Kfor2 a2 a3 s k => do b <- bool_val v ty; - if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m) + if b + then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m) + else ret "step_for_false" (State f Sskip k e m) | Kreturn k => do v' <- sem_cast v ty f.(fn_return); do m' <- Mem.free_list m (blocks_of_env ge e); - ret (Returnstate v' (call_cont k) m') + ret "step_return_2" (Returnstate v' (call_cont k) m') | Kswitch1 sl k => do n <- sem_switch_arg v ty; - ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) + ret "step_expr_switch" (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) | _ => nil end @@ -2001,48 +2004,66 @@ Definition do_step (w: world) (s: state) : list (trace * state) := map (expr_final_state f k e) (step_expr e w RV a m) end - | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m) - - | State f (Ssequence s1 s2) k e m => ret(State f s1 (Kseq s2 k) e m) - | State f Sskip (Kseq s k) e m => ret (State f s k e m) - | State f Scontinue (Kseq s k) e m => ret (State f Scontinue k e m) - | State f Sbreak (Kseq s k) e m => ret (State f Sbreak k e m) - - | State f (Sifthenelse a s1 s2) k e m => ret (ExprState f a (Kifthenelse s1 s2 k) e m) - - | State f (Swhile x s) k e m => ret (ExprState f x (Kwhile1 x s k) e m) - | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => ret (State f (Swhile x s) k e m) - | State f Sbreak (Kwhile2 x s k) e m => ret (State f Sskip k e m) - - | State f (Sdowhile a s) k e m => ret (State f s (Kdowhile1 a s k) e m) - | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => ret (ExprState f x (Kdowhile2 x s k) e m) - | State f Sbreak (Kdowhile1 x s k) e m => ret (State f Sskip k e m) + | State f (Sdo x) k e m => + ret "step_do_1" (ExprState f x (Kdo k) e m) + | State f (Ssequence s1 s2) k e m => + ret "step_seq" (State f s1 (Kseq s2 k) e m) + | State f Sskip (Kseq s k) e m => + ret "step_skip_seq" (State f s k e m) + | State f Scontinue (Kseq s k) e m => + ret "step_continue_seq" (State f Scontinue k e m) + | State f Sbreak (Kseq s k) e m => + ret "step_break_seq" (State f Sbreak k e m) + + | State f (Sifthenelse a s1 s2) k e m => + ret "step_ifthenelse_1" (ExprState f a (Kifthenelse s1 s2 k) e m) + + | State f (Swhile x s) k e m => + ret "step_while" (ExprState f x (Kwhile1 x s k) e m) + | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => + ret "step_skip_or_continue_while" (State f (Swhile x s) k e m) + | State f Sbreak (Kwhile2 x s k) e m => + ret "step_break_while" (State f Sskip k e m) + + | State f (Sdowhile a s) k e m => + ret "step_dowhile" (State f s (Kdowhile1 a s k) e m) + | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => + ret "step_skip_or_continue_dowhile" (ExprState f x (Kdowhile2 x s k) e m) + | State f Sbreak (Kdowhile1 x s k) e m => + ret "step_break_dowhile" (State f Sskip k e m) | State f (Sfor a1 a2 a3 s) k e m => if is_skip a1 - then ret (ExprState f a2 (Kfor2 a2 a3 s k) e m) - else ret (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) - | State f Sskip (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m) - | State f Scontinue (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m) - | State f Sbreak (Kfor3 a2 a3 s k) e m => ret (State f Sskip k e m) - | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m) + then ret "step_for" (ExprState f a2 (Kfor2 a2 a3 s k) e m) + else ret "step_for_start" (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) + | State f (Sskip|Scontinue) (Kfor3 a2 a3 s k) e m => + ret "step_skip_or_continue_for3" (State f a3 (Kfor4 a2 a3 s k) e m) + | State f Sbreak (Kfor3 a2 a3 s k) e m => + ret "step_break_for3" (State f Sskip k e m) + | State f Sskip (Kfor4 a2 a3 s k) e m => + ret "step_skip_for4" (State f (Sfor Sskip a2 a3 s) k e m) | State f (Sreturn None) k e m => do m' <- Mem.free_list m (blocks_of_env ge e); - ret (Returnstate Vundef (call_cont k) m') - | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m) + ret "step_return_0" (Returnstate Vundef (call_cont k) m') + | State f (Sreturn (Some x)) k e m => + ret "step_return_1" (ExprState f x (Kreturn k) e m) | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => do m' <- Mem.free_list m (blocks_of_env ge e); - ret (Returnstate Vundef k m') + ret "step_skip_call" (Returnstate Vundef k m') - | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m) - | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m) - | State f Scontinue (Kswitch2 k) e m => ret (State f Scontinue k e m) + | State f (Sswitch x sl) k e m => + ret "step_switch" (ExprState f x (Kswitch1 sl k) e m) + | State f (Sskip|Sbreak) (Kswitch2 k) e m => + ret "step_skip_break_switch" (State f Sskip k e m) + | State f Scontinue (Kswitch2 k) e m => + ret "step_continue_switch" (State f Scontinue k e m) - | State f (Slabel lbl s) k e m => ret (State f s k e m) + | State f (Slabel lbl s) k e m => + ret "step_label" (State f s k e m) | State f (Sgoto lbl) k e m => match find_label lbl f.(fn_body) (call_cont k) with - | Some(s', k') => ret (State f s' k' e m) + | Some(s', k') => ret "step_goto" (State f s' k' e m) | None => nil end @@ -2050,14 +2071,15 @@ Definition do_step (w: world) (s: state) : list (trace * state) := check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f))); let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs; - ret (State f f.(fn_body) k e m2) + ret "step_internal_function" (State f f.(fn_body) k e m2) | Callstate (External ef _ _ _) vargs k m => match do_external ef w vargs m with | None => nil - | Some(w',t,v,m') => (t, Returnstate v k m') :: nil + | Some(w',t,v,m') => TR "step_external_function" t (Returnstate v k m') :: nil end - | Returnstate v (Kcall f e C ty k) m => ret (ExprState f (C (Eval v ty)) k e m) + | Returnstate v (Kcall f e C ty k) m => + ret "step_returnstate" (ExprState f (C (Eval v ty)) k e m) | _ => nil end. @@ -2065,7 +2087,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) := Ltac myinv := match goal with | [ |- In _ nil -> _ ] => intro X; elim X - | [ |- In _ (ret _) -> _ ] => + | [ |- In _ (ret _ _) -> _ ] => intro X; elim X; clear X; [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] | [ |- In _ (_ :: nil) -> _ ] => @@ -2079,8 +2101,8 @@ Ltac myinv := Hint Extern 3 => exact I. Theorem do_step_sound: - forall w S t S', - In (t, S') (do_step w S) -> + forall w S rule t S', + In (TR rule t S') (do_step w S) -> Csem.step ge S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S). Proof with try (left; right; econstructor; eauto; fail). intros until S'. destruct S; simpl. @@ -2145,45 +2167,52 @@ Proof. Qed. Theorem do_step_complete: - forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S). -Proof with (unfold ret; auto with coqlib). + forall w S t S' w', + possible_trace w t w' -> Csem.step ge S t S' -> exists rule, In (TR rule t S') (do_step w S). +Proof with (unfold ret; eauto with coqlib). intros until w'; intros PT H. destruct H. (* Expression step *) inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL. (* lred *) unfold do_step; rewrite NOTVAL. - change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')). + exploit lred_topred; eauto. instantiate (1 := w). intros (rule & STEP). + exists rule. change (TR rule E0 (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Lred rule a' m')). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. - intro. replace C with (fun x => C x). apply H2. - rewrite (lred_topred _ _ _ _ _ _ H0). unfold topred; auto with coqlib. + intro. replace C with (fun x => C x). apply H2. + rewrite STEP. unfold topred; auto with coqlib. apply extensionality; auto. (* rred *) unfold do_step; rewrite NOTVAL. - change (t, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m' t)). + exploit rred_topred; eauto. instantiate (1 := e). intros (rule & STEP). + exists rule. + change (TR rule t (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Rred rule a' m' t)). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. - intro. replace C with (fun x => C x). apply H2. - rewrite (rred_topred _ _ _ _ _ _ _ _ H0 PT). unfold topred; auto with coqlib. + intro. replace C with (fun x => C x). apply H2. + rewrite STEP; unfold topred; auto with coqlib. apply extensionality; auto. (* callred *) unfold do_step; rewrite NOTVAL. - change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)). + exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e). + intros (rule & STEP). exists rule. + change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. intro. replace C with (fun x => C x). apply H2. - rewrite (callred_topred _ _ _ _ _ _ _ H0). unfold topred; auto with coqlib. + rewrite STEP; unfold topred; auto with coqlib. apply extensionality; auto. (* stuck *) exploit not_imm_safe_stuck_red. eauto. red; intros; elim H1. eapply imm_safe_t_imm_safe. eauto. instantiate (1 := w). intros [C' IN]. - simpl do_step. rewrite NOTVAL. - change (E0, Stuckstate) with (expr_final_state f k e (C', Stuckred)). + simpl do_step. rewrite NOTVAL. + exists "step_stuck". + change (TR "step_stuck" E0 Stuckstate) with (expr_final_state f k e (C', Stuckred)). apply in_map. auto. (* Statement step *) - inv H; simpl... + inv H; simpl; econstructor... rewrite H0... rewrite H0... rewrite H0... diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index e6e3a321..fafbf29f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -317,7 +317,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := (More exactly, identification of function calls that can reduce.) *) Inductive callred: expr -> fundef -> list val -> type -> Prop := - | red_Ecall: forall vf tyf tyargs tyres cconv el ty fd vargs, + | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs, Genv.find_funct ge vf = Some fd -> cast_arguments el tyargs vargs -> type_of_fundef fd = Tfunction tyargs tyres cconv -> diff --git a/cparser/Elab.ml b/cparser/Elab.ml index bad92cf6..612103a6 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -224,16 +224,21 @@ let elab_char_constant loc wide chars = let v = List.fold_left (fun acc d -> - if acc >= max_val then + if acc < 0L || acc >= max_val then error loc "character constant overflows"; - if d >= max_digit then - warning loc "escape sequence is out of range (code 0x%LX)" d; + if d < 0L || d >= max_digit then + error loc "escape sequence is out of range (code 0x%LX)" d; Int64.add (Int64.shift_left acc nbits) d) 0L chars in if not (integer_representable v IInt) then warning loc "character constant cannot be represented at type 'int'"; - (* C99 6.4.4.4 item 10: single character -> represent at type char *) - Ceval.normalize_int v (if List.length chars = 1 then IChar else IInt) + (* C99 6.4.4.4 item 10: single character -> represent at type char + or wchar_t *) + Ceval.normalize_int v + (if List.length chars = 1 then + if wide then wchar_ikind() else IChar + else + IInt) let elab_string_literal loc wide chars = let nbits = if wide then 8 * !config.sizeof_wchar else 8 in @@ -241,14 +246,14 @@ let elab_string_literal loc wide chars = List.iter (fun c -> if c < 0L || c >= char_max - then warning loc "escape sequence is out of range (code 0x%LX)" c) + then error loc "escape sequence is out of range (code 0x%LX)" c) chars; if wide then CWStr chars else begin let res = String.create (List.length chars) in List.iteri - (fun i c -> res.[i] <- Char.chr (Int64.to_int c)) + (fun i c -> res.[i] <- Char.unsafe_chr (Int64.to_int c)) chars; CStr res end diff --git a/driver/Configuration.ml b/driver/Configuration.ml index e73125f7..0012dc0c 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -10,86 +10,87 @@ (* *) (* *********************************************************************) +open Printf -let config_vars: (string, string) Hashtbl.t = Hashtbl.create 10 +(* Locate the .ini file, which is either in the same directory as + the executable or in the directory ../share *) +let ini_file_name = + try + Sys.getenv "COMPCERT_CONFIG" + with Not_found -> + let exe_dir = Filename.dirname Sys.executable_name in + let exe_ini = Filename.concat exe_dir "compcert.ini" in + let share_dir = + Filename.concat (Filename.concat exe_dir Filename.parent_dir_name) + "share" in + let share_ini = Filename.concat share_dir "compcert.ini" in + if Sys.file_exists exe_ini then exe_ini + else if Sys.file_exists share_ini then share_ini + else begin + eprintf "Cannot find compcert.ini configuration file.\n"; + exit 2 + end + +(* Read in the .ini file *) -(* Read in the .ini file, which is either in the same directory or in the directory ../share *) let _ = try - let file = - try - let env_file = Sys.getenv "COMPCERT_CONFIG" in - open_in env_file - with Not_found -> - let dir = Sys.getcwd () - and name = Sys.executable_name in - let dirname = if Filename.is_relative name then - Filename.dirname (Filename.concat dir name) - else - Filename.dirname name - in - let share_dir = Filename.concat (Filename.concat dirname Filename.parent_dir_name) "share" in - try - open_in (Filename.concat dirname "compcert.ini") - with Sys_error _ -> - open_in (Filename.concat share_dir "compcert.ini") - in - (try - let ini_line = Str.regexp "\\([^=]+\\)=\\(.+\\)" in - while true do - let line = input_line file in - if Str.string_match ini_line line 0 then - let key = Str.matched_group 1 line - and value = Str.matched_group 2 line in - Hashtbl.add config_vars key value - else - Printf.eprintf "Wrong value %s in .ini file.\n" line - done - with End_of_file -> close_in file) - with Sys_error msg -> Printf.eprintf "Unable to open .ini file\n" + Readconfig.read_config_file ini_file_name + with + | Readconfig.Error(file, lineno, msg) -> + eprintf "Error reading configuration file %s.\n" ini_file_name; + eprintf "%s:%d:%s\n" file lineno msg; + exit 2 + | Sys_error msg -> + eprintf "Error reading configuration file %s.\n" ini_file_name; + eprintf "%s\n" msg; + exit 2 let get_config key = - try - Hashtbl.find config_vars key - with Not_found -> - Printf.eprintf "Configuration option `%s' is not set\n" key; exit 2 + match Readconfig.key_val key with + | Some v -> v + | None -> eprintf "Configuration option `%s' is not set\n" key; exit 2 -let bad_config key v = - Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 +let bad_config key vl = + eprintf "Invalid value `%s' for configuration option `%s'\n" + (String.concat " " vl) key; + exit 2 -let prepro = get_config "prepro" -let asm = get_config "asm" -let linker = get_config "linker" -let arch = - let v = get_config "arch" in - (match v with - | "powerpc" - | "arm" - | "ia32" -> () - | _ -> bad_config "arch" v); - v +let get_config_string key = + match get_config key with + | [v] -> v + | vl -> bad_config key vl -let model = get_config "model" -let abi = get_config "abi" -let system = get_config "system" +let get_config_list key = + match get_config key with + | [] -> bad_config key [] + | vl -> vl + +let prepro = get_config_list "prepro" +let asm = get_config_list "asm" +let linker = get_config_list "linker" +let arch = + match get_config_string "arch" with + | "powerpc"|"arm"|"ia32" as a -> a + | v -> bad_config "arch" [v] +let model = get_config_string "model" +let abi = get_config_string "abi" +let system = get_config_string "system" let has_runtime_lib = - match get_config "has_runtime_lib" with + match get_config_string "has_runtime_lib" with | "true" -> true | "false" -> false - | v -> bad_config "has_runtime_lib" v - - + | v -> bad_config "has_runtime_lib" [v] let stdlib_path = if has_runtime_lib then - get_config "stdlib_path" + get_config_string "stdlib_path" else "" - let asm_supports_cfi = - match get_config "asm_supports_cfi" with + match get_config_string "asm_supports_cfi" with | "true" -> true | "false" -> false - | v -> bad_config "asm_supports_cfi" v + | v -> bad_config "asm_supports_cfi" [v] -let version = get_config "version" +let version = get_config_string "version" diff --git a/driver/Driver.ml b/driver/Driver.ml index e943e6c9..d8b28285 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -20,17 +20,38 @@ open Timing let stdlib_path = ref Configuration.stdlib_path -let command cmd = +(* Invocation of external tools *) + +let command ?stdout args = if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) - -let quote_arguments args = - String.concat " " (List.map Filename.quote args) + let argv = Array.of_list args in + assert (Array.length argv > 0); + try + let fd_out = + match stdout with + | None -> Unix.stdout + | Some f -> + Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in + let pid = + Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in + let (_, status) = + Unix.waitpid [] pid in + if stdout <> None then Unix.close fd_out; + match status with + | Unix.WEXITED rc -> rc + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 + with Unix.Unix_error(err, fn, param) -> + eprintf "Error executing '%s': %s: %s %s\n" + argv.(0) fn (Unix.error_message err) param; + -1 let safe_remove file = try Sys.remove file with Sys_error _ -> () @@ -68,16 +89,17 @@ let output_filename_default default_file = let preprocess ifile ofile = let output = - if ofile = "-" then "" else sprintf "> %s" ofile in - let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s %s" - Configuration.prepro - (if Configuration.has_runtime_lib - then sprintf "-I%s" !stdlib_path - else "") - (quote_options !prepro_options) - ifile output in - if command cmd <> 0 then begin + if ofile = "-" then None else Some ofile in + let cmd = List.concat [ + Configuration.prepro; + ["-D__COMPCERT__"]; + (if Configuration.has_runtime_lib + then ["-I" ^ !stdlib_path] + else []); + List.rev !prepro_options; + [ifile] + ] in + if command ?stdout:output cmd <> 0 then begin if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 @@ -208,11 +230,13 @@ let compile_cminor_file ifile ofile = (* From asm to object file *) let assemble ifile ofile = - let cmd = - sprintf "%s -o %s %s %s" - Configuration.asm ofile (quote_options !assembler_options) ifile in - let retcode = command cmd in - if retcode <> 0 then begin + let cmd = List.concat [ + Configuration.asm; + ["-o"; ofile]; + List.rev !assembler_options; + [ifile] + ] in + if command cmd <> 0 then begin safe_remove ofile; eprintf "Error during assembling.\n"; exit 2 @@ -221,14 +245,14 @@ let assemble ifile ofile = (* Linking *) let linker exe_name files = - let cmd = - sprintf "%s -o %s %s %s" - Configuration.linker - (Filename.quote exe_name) - (quote_arguments files) - (if Configuration.has_runtime_lib - then sprintf "-L%s -lcompcert" !stdlib_path - else "") in + let cmd = List.concat [ + Configuration.linker; + ["-o"; exe_name]; + files; + (if Configuration.has_runtime_lib + then ["-L" ^ !stdlib_path; "-lcompcert"] + else []) + ] in if command cmd <> 0 then exit 2 (* Processing of a .c file *) diff --git a/driver/Interp.ml b/driver/Interp.ml index ab22cebb..2725dbfe 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -254,28 +254,14 @@ let compare_state s1 s2 = compare (rank_state s1) (rank_state s2) end -(* Sets of states already explored *) +(* Maps of states already explored. *) -module StateSet = - Set.Make(struct - type t = state * Determinism.world - let compare (s1,w1) (s2,w2) = compare_state s1 s2 +module StateMap = + Map.Make(struct + type t = state + let compare = compare_state end) -(* Purging states that will never be reached again based on their memory - next block. All states with nextblock <= the given nextblock are - removed. We take advantage of the fact that StateSets are sorted - by increasing nextblock, cf. the definition of compare_state above. *) - -let rec purge_seen nextblock seen = - let min = try Some(StateSet.min_elt seen) with Not_found -> None in - match min with - | None -> seen - | Some((s, w) as sw) -> - if P.le (mem_state s).Mem.nextblock nextblock - then purge_seen nextblock (StateSet.remove sw seen) - else seen - (* Extract a string from a global pointer *) let extract_string m blk ofs = @@ -435,7 +421,7 @@ and world_vstore ge m chunk id ofs ev = let do_event p ge time w ev = if !trace >= 1 then - fprintf p "@[<hov 2>Time %d: observable event:@ @[<hov 2>%a@]@]@." + fprintf p "@[<hov 2>Time %d: observable event:@ %a@]@." time print_event ev; (* Return new world after external action *) match ev with @@ -497,11 +483,10 @@ let diagnose_stuck_state p ge w = function | ExprState(f,a,k,e,m) -> ignore(diagnose_stuck_expr p ge w f a k e m) | _ -> () -(* Exploration *) +(* Execution of a single step. Return list of triples + (reduction rule, next state, next world). *) -let do_step p prog ge time (s, w) = - if !trace >= 2 then - fprintf p "@[<hov 2>Time %d: %a@]@." time print_state (prog, ge, s); +let do_step p prog ge time s w = match Cexec.at_final_state s with | Some r -> if !trace >= 1 then @@ -513,89 +498,71 @@ let do_step p prog ge time (s, w) = end | None -> let l = Cexec.do_step ge do_external_function do_inline_assembly w s in - if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin + if l = [] + || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l + then begin pp_set_max_boxes p 1000; fprintf p "@[<hov 2>Stuck state: %a@]@." print_state (prog, ge, s); diagnose_stuck_state p ge w s; fprintf p "ERROR: Undefined behavior@."; exit 126 end else begin - List.map (fun (t, s') -> (s', do_events p ge time w t)) l + List.map (fun (Cexec.TR(r, t, s')) -> (r, s', do_events p ge time w t)) l end -let rec explore_one p prog ge time sw = - let succs = do_step p prog ge time sw in +(* Exploration of a single execution. *) + +let rec explore_one p prog ge time s w = + if !trace >= 2 then + fprintf p "@[<hov 2>Time %d:@ %a@]@." time print_state (prog, ge, s); + let succs = do_step p prog ge time s w in if succs <> [] then begin - let sw' = + let (r, s', w') = match !mode with | First -> List.hd succs | Random -> List.nth succs (Random.int (List.length succs)) | All -> assert false in - explore_one p prog ge (time + 1) sw' + if !trace >= 2 then + fprintf p "--[%s]-->@." (camlstring_of_coqstring r); + explore_one p prog ge (time + 1) s' w' end -(* A priority queue structure where the priority is inversely proportional - to the memory nextblock. *) - -module PrioQueue = struct - - type elt = int * StateSet.elt - - type queue = Empty | Node of elt * queue * queue - - let empty = Empty - - let singleton elt = Node(elt, Empty, Empty) - - let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) = - P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock - - let rec insert queue elt = - match queue with - | Empty -> Node(elt, Empty, Empty) - | Node(e, left, right) -> - if higher_prio elt e - then Node(elt, insert right e, left) - else Node(e, insert right elt, left) - - let rec remove_top = function - | Empty -> assert false - | Node(elt, left, Empty) -> left - | Node(elt, Empty, right) -> right - | Node(elt, (Node(lelt, _, _) as left), - (Node(relt, _, _) as right)) -> - if higher_prio lelt relt - then Node(lelt, remove_top left, right) - else Node(relt, left, remove_top right) - - let extract = function - | Empty -> None - | Node(elt, _, _) as queue -> Some(elt, remove_top queue) - - (* Return true if all elements of queue have strictly lower priority - than elt. *) - let dominate elt queue = - match queue with - | Empty -> true - | Node(e, _, _) -> higher_prio elt e -end - -let rec explore_all p prog ge seen queue = - match PrioQueue.extract queue with - | None -> () - | Some((time, sw) as tsw, queue') -> - if StateSet.mem sw seen then - explore_all p prog ge seen queue' - else - let succs = - List.rev_map (fun sw -> (time + 1, sw)) (do_step p prog ge time sw) in - let queue'' = List.fold_left PrioQueue.insert queue' succs in - let seen' = StateSet.add sw seen in - let seen'' = - if PrioQueue.dominate tsw queue'' - then purge_seen (mem_state (fst sw)).Mem.nextblock seen' - else seen' in - explore_all p prog ge seen'' queue'' +(* Exploration of all possible executions. *) + +let rec explore_all p prog ge time states = + if !trace >= 2 then begin + List.iter + (fun (n, s, w) -> + fprintf p "@[<hov 2>State %d.%d: @ %a@]@." + time n print_state (prog, ge, s)) + states + end; + let rec explore_next nextstates seen numseen = function + | [] -> + List.rev nextstates + | (n, s, w) :: states -> + add_reducts nextstates seen numseen states n (do_step p prog ge time s w) + + and add_reducts nextstates seen numseen states n = function + | [] -> + explore_next nextstates seen numseen states + | (r, s', w') :: reducts -> + let (n', nextstates', seen', numseen') = + try + (StateMap.find s' seen, nextstates, seen, numseen) + with Not_found -> + (numseen, + (numseen, s', w') :: nextstates, + StateMap.add s' numseen seen, + numseen + 1) in + if !trace >= 2 then begin + fprintf p "Transition state %d.%d --[%s]--> state %d.%d@." + time n (camlstring_of_coqstring r) (time + 1) n' + end; + add_reducts nextstates' seen' numseen' states n reducts + in + let nextstates = explore_next [] StateMap.empty 1 states in + if nextstates <> [] then explore_all p prog ge (time + 1) nextstates (* The variant of the source program used to build the world for executing events. @@ -680,7 +647,6 @@ let execute prog = | Some(ge, s) -> match !mode with | First | Random -> - explore_one p prog1 ge 0 (s, world wge wm) + explore_one p prog1 ge 0 s (world wge wm) | All -> - explore_all p prog1 ge StateSet.empty - (PrioQueue.singleton (0, (s, world wge wm))) + explore_all p prog1 ge 0 [(1, s, world wge wm)] diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 28d0cc8f..a75c95a5 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -23,6 +23,8 @@ Require Export AST. Require Export Ctypes. Require Export Cop. Require Export Clight. +Require Import Maps. +Require Import Errors. Definition tvoid := Tvoid. Definition tschar := Tint I8 Signed noattr. @@ -50,9 +52,8 @@ Definition tattr (a: attr) (ty: type) := | Tpointer elt _ => Tpointer elt a | Tarray elt sz _ => Tarray elt sz a | Tfunction args res cc => Tfunction args res cc - | Tstruct id fld _ => Tstruct id fld a - | Tunion id fld _ => Tunion id fld a - | Tcomp_ptr id _ => Tcomp_ptr id a + | Tstruct id _ => Tstruct id a + | Tunion id _ => Tunion id a end. Definition tvolatile (ty: type) := tattr volatile_attr ty. @@ -62,3 +63,9 @@ Definition talignas (n: N) (ty: type) := Definition tvolatile_alignas (n: N) (ty: type) := tattr {| attr_volatile := true; attr_alignas := Some n |} ty. + +Definition make_composite_env (comps: list composite_definition): composite_env := + match build_composite_env comps with + | OK e => e + | Error _ => PTree.empty _ + end. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 53eb96fd..c1009b4f 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -14,24 +14,45 @@ (* *********************************************************************) open Printf +open Commandline open Clflags (* Location of the compatibility library *) -let stdlib_path = ref( - try - Sys.getenv "COMPCERT_LIBRARY" - with Not_found -> - Configuration.stdlib_path) +let stdlib_path = ref Configuration.stdlib_path + +(* Invocation of external tools *) -let command cmd = +let command ?stdout args = if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) + let argv = Array.of_list args in + assert (Array.length argv > 0); + try + let fd_out = + match stdout with + | None -> Unix.stdout + | Some f -> + Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in + let pid = + Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in + let (_, status) = + Unix.waitpid [] pid in + if stdout <> None then Unix.close fd_out; + match status with + | Unix.WEXITED rc -> rc + | Unix.WSIGNALED n | Unix.WSTOPPED n -> + eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 + with Unix.Unix_error(err, fn, param) -> + eprintf "Error executing '%s': %s: %s %s\n" + argv.(0) fn (Unix.error_message err) param; + -1 let safe_remove file = try Sys.remove file with Sys_error _ -> () @@ -47,20 +68,32 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' +(* Determine names for output files. We use -o option if specified + and if this is the final destination file (not a dump file). + Otherwise, we generate a file in the current directory. *) + +let output_filename ?(final = false) source_file source_suffix output_suffix = + match !option_o with + | Some file when final -> file + | _ -> + Filename.basename (Filename.chop_suffix source_file source_suffix) + ^ output_suffix + (* From C to preprocessed C *) let preprocess ifile ofile = let output = - if ofile = "-" then "" else sprintf "> %s" ofile in - let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s %s" - Configuration.prepro - (if Configuration.has_runtime_lib - then sprintf "-I%s" !stdlib_path - else "") - (quote_options !prepro_options) - ifile output in - if command cmd <> 0 then begin + if ofile = "-" then None else Some ofile in + let cmd = List.concat [ + Configuration.prepro; + ["-D__COMPCERT__"]; + (if Configuration.has_runtime_lib + then ["-I" ^ !stdlib_path] + else []); + List.rev !prepro_options; + [ifile] + ] in + if command ?stdout:output cmd <> 0 then begin if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 @@ -82,24 +115,22 @@ let parse_c_file sourcename ifile = match Parse.preprocessed_file simplifs sourcename ifile with | None -> exit 2 | Some p -> p in - (* Remove preprocessed file (always a temp file) *) - safe_remove ifile; (* Save C AST if requested *) if !option_dparse then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".parsed.c" in + let ofile = output_filename sourcename ".c" ".parsed.c" in let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc end; (* Conversion to Csyntax *) let csyntax = - match C2C.convertProgram ast with + match Timing.time "CompCert C generation" C2C.convertProgram ast with | None -> exit 2 | Some p -> p in flush stderr; (* Save CompCert C AST if requested *) if !option_dcmedium then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in + let ofile = output_filename sourcename ".c" ".compcert.c" in let oc = open_out ofile in PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc @@ -157,59 +188,6 @@ let explode_comma_option s = | [] -> assert false | hd :: tl -> tl -type action = - | Set of bool ref - | Unset of bool ref - | Self of (string -> unit) - | String of (string -> unit) - | Integer of (int -> unit) - -let rec find_action s = function - | [] -> None - | (re, act) :: rem -> - if Str.string_match re s 0 then Some act else find_action s rem - -let parse_cmdline spec usage = - let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in - let error () = - eprintf "%s" usage; - exit 2 in - let rec parse i = - if i < Array.length Sys.argv then begin - let s = Sys.argv.(i) in - match find_action s acts with - | None -> - if s <> "-help" && s <> "--help" - then eprintf "Unknown argument `%s'\n" s; - error () - | Some(Set r) -> - r := true; parse (i+1) - | Some(Unset r) -> - r := false; parse (i+1) - | Some(Self fn) -> - fn s; parse (i+1) - | Some(String fn) -> - if i + 1 < Array.length Sys.argv then begin - fn Sys.argv.(i+1); parse (i+2) - end else begin - eprintf "Option `%s' expects an argument\n" s; error() - end - | Some(Integer fn) -> - if i + 1 < Array.length Sys.argv then begin - let n = - try - int_of_string Sys.argv.(i+1) - with Failure _ -> - eprintf "Argument to option `%s' must be an integer\n" s; - error() - in - fn n; parse (i+2) - end else begin - eprintf "Option `%s' expects an argument\n" s; error() - end - end - in parse 1 - let usage_string = "The CompCert Clight generator Usage: clightgen [options] <source files> @@ -238,36 +216,63 @@ General options: -v Print external commands before invoking them " +let print_usage_and_exit _ = + printf "%s" usage_string; exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; - option_fstruct_return; option_fvararg_calls; option_fpacked_structs + option_fstruct_return; option_fvararg_calls; option_funprototyped; + option_fpacked_structs; option_finline_asm ] +let set_all opts = List.iter (fun r -> r := true) opts +let unset_all opts = List.iter (fun r -> r := false) opts + let cmdline_actions = let f_opt name ref = - ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in + [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ - "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); - "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); - "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); - "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options); - "-dparse$", Set option_dparse; - "-dc$", Set option_dcmedium; - "-dclight$", Set option_dclight; - "-E$", Set option_E; - ".*\\.c$", Self (fun s -> process_c_file s); - "-Wp,", Self (fun s -> - prepro_options := List.rev_append (explode_comma_option s) !prepro_options); - "-fall$", Self (fun _ -> - List.iter (fun r -> r := true) language_support_options); - "-fnone$", Self (fun _ -> - List.iter (fun r -> r := false) language_support_options); +(* Getting help *) + Exact "-help", Self print_usage_and_exit; + Exact "--help", Self print_usage_and_exit; +(* Processing options *) + Exact "-E", Set option_E; +(* Preprocessing options *) + Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); + Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); + Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); + Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options); + Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); + Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); + Prefix "-Wp,", Self (fun s -> + prepro_options := List.rev_append (explode_comma_option s) !prepro_options); +(* Language support options -- more below *) + Exact "-fall", Self (fun _ -> set_all language_support_options); + Exact "-fnone", Self (fun _ -> unset_all language_support_options); +(* Tracing options *) + Exact "-dparse", Set option_dparse; + Exact "-dc", Set option_dcmedium; + Exact "-dclight", Set option_dclight; +(* General options *) + Exact "-v", Set option_v; + Exact "-stdlib", String(fun s -> stdlib_path := s); ] +(* -f options: come in -f and -fno- variants *) +(* Language support options *) @ f_opt "longdouble" option_flongdouble @ f_opt "struct-return" option_fstruct_return @ f_opt "bitfields" option_fbitfields @ f_opt "vararg-calls" option_fvararg_calls + @ f_opt "unprototyped" option_funprototyped @ f_opt "packed-structs" option_fpacked_structs + @ f_opt "inline-asm" option_finline_asm + @ [ +(* Catch options that are not handled *) + Prefix "-", Self (fun s -> + eprintf "Unknown option `%s'\n" s; exit 2); +(* File arguments *) + Suffix ".c", Self (fun s -> process_c_file s); + ] let _ = Gc.set { (Gc.get()) with @@ -284,4 +289,5 @@ let _ = end; Builtins.set C2C.builtins; CPragmas.initialize(); - parse_cmdline cmdline_actions usage_string + parse_cmdline cmdline_actions + diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index e4d1ce53..51dd0757 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -132,9 +132,20 @@ let coqfloat p n = let coqsingle p n = fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n) -(* Types *) +let coqN p n = + fprintf p "%ld%%N" (N.to_int32 n) + +(* Raw attributes *) -let use_struct_names = ref true +let attribute p a = + if a = noattr then + fprintf p "noattr" + else + fprintf p "{| attr_volatile := %B; attr_alignas := %a |}" + a.attr_volatile + (print_option coqN) a.attr_alignas + +(* Types *) let rec typ p t = match attr_of_type t with @@ -143,9 +154,9 @@ let rec typ p t = | { attr_volatile = true; attr_alignas = None} -> fprintf p "(tvolatile %a)" rtyp t | { attr_volatile = false; attr_alignas = Some n} -> - fprintf p "(talignas %ld%%N %a)" (N.to_int32 n) rtyp t + fprintf p "(talignas %a %a)" coqN n rtyp t | { attr_volatile = true; attr_alignas = Some n} -> - fprintf p "(tvolatile_alignas %ld%%N %a)" (N.to_int32 n) rtyp t + fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t and rtyp p = function | Tvoid -> fprintf p "tvoid" @@ -176,16 +187,10 @@ and rtyp p = function | Tfunction(targs, tres, cc) -> fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]" typlist targs typ tres callconv cc - | Tstruct(id, flds, _) -> - if !use_struct_names - then fprintf p "t%a" ident id - else fprintf p "@[<hov 2>(Tstruct %a@ %a@ noattr)@]" ident id fieldlist flds - | Tunion(id, flds, _) -> - if !use_struct_names - then fprintf p "t%a" ident id - else fprintf p "@[<hov 2>(Tunion %a@ %a@ noattr)@]" ident id fieldlist flds - | Tcomp_ptr(id, _) -> - fprintf p "(Tcomp_ptr %a noattr)" ident id + | Tstruct(id, _) -> + fprintf p "(Tstruct %a noattr)" ident id + | Tunion(id, _) -> + fprintf p "(Tunion %a noattr)" ident id and typlist p = function | Tnil -> @@ -193,12 +198,6 @@ and typlist p = function | Tcons(t, tl) -> fprintf p "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl -and fieldlist p = function - | Fnil -> - fprintf p "Fnil" - | Fcons(id, t, fl) -> - fprintf p "@[<hov 2>(Fcons %a@ %a@ %a)@]" ident id typ t fieldlist fl - and callconv p cc = if cc = cc_default then fprintf p "cc_default" @@ -323,6 +322,10 @@ let rec expr p = function (name_binop op) expr a1 expr a2 typ t | Ecast(a1, t) -> fprintf p "@[<hov 2>(Ecast@ %a@ %a)@]" expr a1 typ t + | Esizeof(t1, t) -> + fprintf p "(Esizeof %a %a)" typ t1 typ t + | Ealignof(t1, t) -> + fprintf p "(Ealignof %a %a)" typ t1 typ t (* Statements *) @@ -420,115 +423,14 @@ let print_ident_globdef p = function | (id, Gvar v) -> fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id) -(* Collecting the names and fields of structs and unions *) - -module TypeSet = Set.Make(struct - type t = coq_type - let compare = Pervasives.compare -end) - -let struct_unions = ref TypeSet.empty - -let register_struct_union ty = - struct_unions := TypeSet.add ty !struct_unions - -let rec collect_type = function - | Tvoid -> () - | Tint _ -> () - | Tlong _ -> () - | Tfloat _ -> () - | Tpointer(t, _) -> collect_type t - | Tarray(t, _, _) -> collect_type t - | Tfunction(args, res, _) -> collect_type_list args; collect_type res - | Tstruct(id, fld, _) -> - register_struct_union (Tstruct(id, fld, noattr)) (*; collect_fields fld*) - | Tunion(id, fld, _) -> - register_struct_union (Tunion(id, fld, noattr)) (*; collect_fields fld*) - | Tcomp_ptr _ -> () - -and collect_type_list = function - | Tnil -> () - | Tcons(hd, tl) -> collect_type hd; collect_type_list tl - -and collect_fields = function - | Fnil -> () - | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl - -let rec collect_expr e = - collect_type (typeof e); - match e with - | Econst_int _ -> () - | Econst_float _ -> () - | Econst_long _ -> () - | Econst_single _ -> () - | Evar _ -> () - | Etempvar _ -> () - | Ederef(r, _) -> collect_expr r - | Efield(l, _, _) -> collect_expr l - | Eaddrof(l, _) -> collect_expr l - | Eunop(_, r, _) -> collect_expr r - | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 - | Ecast(r, _) -> collect_expr r - -let rec collect_exprlist = function - | [] -> () - | r1 :: rl -> collect_expr r1; collect_exprlist rl - -let rec temp_of_expr = function - | Etempvar(tmp, _) -> Some tmp - | Ecast(e, _) -> temp_of_expr e - | _ -> None +(* Composite definitions *) -let rec collect_stmt = function - | Sskip -> () - | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 - | Sset(id, e2) -> - begin match temp_of_expr e2 with - | Some tmp -> name_temporary tmp id - | None -> () - end; - collect_expr e2 - | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el - | Sbuiltin(optid, ef, tyl, el) -> collect_exprlist el - | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sbreak -> () - | Scontinue -> () - | Sswitch(e, cases) -> collect_expr e; collect_cases cases - | Sreturn None -> () - | Sreturn (Some e) -> collect_expr e - | Slabel(lbl, s) -> collect_stmt s - | Sgoto lbl -> () - -and collect_cases = function - | LSnil -> () - | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem - -let collect_function f = - collect_type f.fn_return; - List.iter (fun (id, ty) -> collect_type ty) f.fn_params; - List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; - List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; - collect_stmt f.fn_body - -let collect_globdef (id, gd) = - match gd with - | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res - | Gfun(Internal f) -> collect_function f - | Gvar v -> collect_type v.gvar_info - -let define_struct p ty = - match ty with - | Tstruct(id, _, _) | Tunion(id, _, _) -> - fprintf p "@[<hv 2>Definition t%a :=@ %a.@]@ " ident id typ ty - | _ -> assert false - -let define_structs p prog = - use_struct_names := false; - TypeSet.iter (define_struct p) !struct_unions; - use_struct_names := true; - fprintf p "@ " +let print_composite_definition p (Composite(id, su, m, a)) = + fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]" + ident id + (match su with Struct -> "Struct" | Union -> "Union") + (print_list (print_pair ident typ)) m + attribute a (* Assertion processing *) @@ -605,14 +507,18 @@ let print_program p prog = fprintf p "%s" prologue; Hashtbl.clear temp_names; all_temp_names := StringSet.empty; - struct_unions := TypeSet.empty; - List.iter collect_globdef prog.prog_defs; define_idents p; - define_structs p prog; List.iter (print_globdef p) prog.prog_defs; + fprintf p "Definition composites : list composite_definition :=@ "; + print_list print_composite_definition p prog.prog_types; + fprintf p ".@ @ "; fprintf p "Definition prog : Clight.program := {|@ "; fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.prog_defs; - fprintf p "prog_main := %a@ " ident prog.prog_main; + fprintf p "prog_public :=@ %a;@ " (print_list ident) prog.prog_public; + fprintf p "prog_main := %a;@ " ident prog.prog_main; + fprintf p "prog_types := composites;@ "; + fprintf p "prog_comp_env := make_composite_env composites;@ "; + fprintf p "prog_comp_env_eq := refl_equal _@ "; fprintf p "|}.@ "; print_assertions p; fprintf p "@]@." diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index c77347da..eba416e4 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -81,7 +81,7 @@ module Cygwin_System = fprintf oc "_%s" s let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl @@ -130,9 +130,9 @@ module ELF_System = let raw_symbol oc s = fprintf oc "%s" s - - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + + let symbol oc symb = + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc ".L%d" lbl @@ -188,7 +188,7 @@ module MacOS_System = fprintf oc "_%s" s let symbol oc symb = - fprintf oc "_%s" (extern_atom symb) + raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl @@ -1035,20 +1035,12 @@ let print_globdef oc (name, gdef) = | Gvar v -> print_var oc name v end) -type target = ELF | MacOS | Cygwin - let print_program oc p = - let target = - match Configuration.system with - | "macosx" -> MacOS - | "linux" -> ELF - | "bsd" -> ELF - | "cygwin" -> Cygwin - | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") in - let module Target = (val (match target with - | MacOS -> (module MacOS_System:SYSTEM) - | ELF -> (module ELF_System:SYSTEM) - | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in + let module Target = (val (match Configuration.system with + | "macosx" -> (module MacOS_System:SYSTEM) + | "linux" | "bsd" -> (module ELF_System:SYSTEM) + | "cygwin" -> (module Cygwin_System:SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")):SYSTEM) in let module Printer = AsmPrinter(Target) in PrintAnnot.print_version_and_options oc Printer.comment; PrintAnnot.reset_filenames(); diff --git a/lib/Readconfig.mli b/lib/Readconfig.mli new file mode 100644 index 00000000..c81e7786 --- /dev/null +++ b/lib/Readconfig.mli @@ -0,0 +1,39 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Reading configuration files *) + +(* The format of a configuration file is a list of lines + variable=value + The "value" on the right hand side is a list of whitespace-separated + words. Quoting is honored with the same rules as POSIX shell: + \<newline> for multi-line values + single quotes no escapes within + double quotes \$ \` \<doublequote> \\ \<newline> as escapes + Finally, lines starting with '#' are comments. +*) + +val read_config_file: string -> unit + (** Read (key, value) pairs from the given file name. Raise [Error] + if file is ill-formed. *) + +val key_val: string -> string list option + (** [key_val k] returns the value associated with key [k], if any. + Otherwise, [None] is returned. *) + +exception Error of string * int * string + (** Raised in case of error. + First argument is file name, second argument is line number, + third argument is an explanation of the error. *) diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll new file mode 100644 index 00000000..27ef32cf --- /dev/null +++ b/lib/Readconfig.mll @@ -0,0 +1,111 @@ +{ + +(* Recording key=val bindings *) + +let key_val_tbl : (string, string list) Hashtbl.t = Hashtbl.create 17 + +let key_val key = + try Some(Hashtbl.find key_val_tbl key) with Not_found -> None + +(* Auxiliaries for parsing *) + +let buf = Buffer.create 32 + +let stash inword words = + if inword then begin + let w = Buffer.contents buf in + Buffer.clear buf; + w :: words + end else + words + +(* Error reporting *) + +exception Error of string * int * string + +let error msg lexbuf = + Lexing.(raise (Error(lexbuf.lex_curr_p.pos_fname, + lexbuf.lex_curr_p.pos_lnum, + msg))) + +let ill_formed_line lexbuf = error "Ill-formed line" lexbuf +let unterminated_quote lexbuf = error "Unterminated quote" lexbuf +let lone_backslash lexbuf = error "Lone \\ (backslash) at end of file" lexbuf + +} + +let whitespace = [' ' '\t' '\012' '\r'] +let newline = '\r'* '\n' +let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']* + +rule begline = parse + | '#' [^ '\n']* ('\n' | eof) + { Lexing.new_line lexbuf; begline lexbuf } + | whitespace* (ident as key) whitespace* '=' + { let words = unquoted false [] lexbuf in + Hashtbl.add key_val_tbl key (List.rev words); + begline lexbuf } + | eof + { () } + | _ + { ill_formed_line lexbuf } + +and unquoted inword words = parse + | '\n' | eof { Lexing.new_line lexbuf; stash inword words } + | whitespace+ { unquoted false (stash inword words) lexbuf } + | '\\' newline { Lexing.new_line lexbuf; unquoted inword words lexbuf } + | '\\' (_ as c) { Buffer.add_char buf c; unquoted true words lexbuf } + | '\\' eof { lone_backslash lexbuf } + | '\'' { singlequote lexbuf; unquoted true words lexbuf } + | '\"' { doublequote lexbuf; unquoted true words lexbuf } + | _ as c { Buffer.add_char buf c; unquoted true words lexbuf } + +and singlequote = parse + | eof { unterminated_quote lexbuf } + | '\'' { () } + | newline { Lexing.new_line lexbuf; + Buffer.add_char buf '\n'; singlequote lexbuf } + | _ as c { Buffer.add_char buf c; singlequote lexbuf } + +and doublequote = parse + | eof { unterminated_quote lexbuf } + | '\"' { () } + | '\\' newline { Lexing.new_line lexbuf; doublequote lexbuf } + | '\\' (['$' '`' '\"' '\\'] as c) + { Buffer.add_char buf c; doublequote lexbuf } + | newline { Lexing.new_line lexbuf; + Buffer.add_char buf '\n'; doublequote lexbuf } + | _ as c { Buffer.add_char buf c; doublequote lexbuf } + +{ + +(* The entry point *) + +let read_config_file filename = + let ic = open_in filename in + let lexbuf = Lexing.from_channel ic in + Lexing.(lexbuf.lex_start_p <- {lexbuf.lex_start_p with pos_fname = filename}); + try + Hashtbl.clear key_val_tbl; + begline lexbuf; + close_in ic + with x -> + close_in ic; raise x + +(* Test harness *) +(* +open Printf + +let _ = + Hashtbl.clear key_val_tbl; + begline (Lexing.from_channel stdin); + Hashtbl.iter + (fun key value -> + printf "%s =" key; + List.iter (fun v -> printf " |%s|" v) value; + printf "\n") + key_val_tbl +*) + +} + diff --git a/runtime/Makefile b/runtime/Makefile index 1f0ccf25..9a872427 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -36,7 +36,7 @@ install: endif test/test_int64: test/test_int64.c $(LIB) - $(CC) -o $@ test/test_int64.c $(LIB) + $(CC) -g -o $@ test/test_int64.c $(LIB) clean:: rm -f test/test_int64 diff --git a/runtime/README b/runtime/README new file mode 100644 index 00000000..5d824300 --- /dev/null +++ b/runtime/README @@ -0,0 +1,11 @@ +This is the support library for CompCert-generated code. +It provides helper functions for: +- 64-bit integer arithmetic +- implementing the va_arg macro from <stdarg.h> + +The implementation is written in assembly language in the +arm/ ia32/ powerpc/ directories. + +The c/ directory contains a C implementation of the 64-bit integer functions. +It is provided for reference and as a guide for the asm implementations. + diff --git a/runtime/c/i64.h b/runtime/c/i64.h new file mode 100644 index 00000000..dd584533 --- /dev/null +++ b/runtime/c/i64.h @@ -0,0 +1,43 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +extern unsigned long long __i64_shl(unsigned long long x, int amount); +extern unsigned long long __i64_shr(unsigned long long x, int amount); +extern signed long long __i64_sar(signed long long x, int amount); + +extern unsigned long long __i64_udivmod(unsigned long long n, + unsigned long long d, + unsigned long long * rp); diff --git a/runtime/c/i64_dtos.c b/runtime/c/i64_dtos.c new file mode 100644 index 00000000..d428e744 --- /dev/null +++ b/runtime/c/i64_dtos.c @@ -0,0 +1,74 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Conversion float64 -> signed int64 */ + +long long __i64_dtos(double d) +{ + /* Extract bits of d's representation */ + union { double d; unsigned long long i; } buf; + buf.d = d; + unsigned int h = buf.i >> 32; + /* Extract unbiased exponent */ + int e = ((h & 0x7FF00000) >> 20) - (1023 + 52); + /* Check range of exponent */ + if (e < -52) { + /* |d| is less than 1.0 */ + return 0LL; + } + if (e >= 63 - 52) { + /* |d| is greater or equal to 2^63 */ + if ((int) h < 0) + return -0x8000000000000000LL; /* min signed long long */ + else + return 0x7FFFFFFFFFFFFFFFLL; /* max signed long long */ + } + /* Extract true mantissa */ + unsigned long long m = + (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL; + /* Shift it appropriately */ + if (e >= 0) + m = __i64_shl(m, e); + else + m = __i64_shr(m, -e); + /* Apply sign to result */ + if ((int) h < 0) + return -m; + else + return m; +} diff --git a/runtime/c/i64_dtou.c b/runtime/c/i64_dtou.c new file mode 100644 index 00000000..c5f9df4d --- /dev/null +++ b/runtime/c/i64_dtou.c @@ -0,0 +1,69 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Conversion float64 -> unsigned int64 */ + +unsigned long long __i64_dtou(double d) +{ + /* Extract bits of d's representation */ + union { double d; unsigned long long i; } buf; + buf.d = d; + unsigned int h = buf.i >> 32; + /* Negative FP numbers convert to 0 */ + if ((int) h < 0) return 0ULL; + /* Extract unbiased exponent */ + int e = ((h & 0x7FF00000) >> 20) - (1023 + 52); + /* Check range of exponent */ + if (e < -52) { + /* d is less than 1.0 */ + return 0ULL; + } + if (e >= 64 - 52) { + /* d is greater or equal to 2^64 */ + return 0xFFFFFFFFFFFFFFFFULL; /* max unsigned long long */ + } + /* Extract true mantissa */ + unsigned long long m = + (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL; + /* Shift it appropriately */ + if (e >= 0) + return __i64_shl(m, e); + else + return __i64_shr(m, -e); + +} diff --git a/runtime/c/i64_sar.c b/runtime/c/i64_sar.c new file mode 100644 index 00000000..a5f3364a --- /dev/null +++ b/runtime/c/i64_sar.c @@ -0,0 +1,56 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Shift right signed */ + +signed long long __i64_sar(signed long long x, int amount) +{ + unsigned xl = x; + int xh = x >> 32; + amount = amount & 63; + if (amount == 0) { + return x; + } + else if (amount < 32) { + unsigned rl = (xl >> amount) | (xh << (32 - amount)); + int rh = xh >> amount; + return rl | ((signed long long) rh << 32); + } else { + return (signed long long) (xh >> (amount - 32)); + } +} diff --git a/runtime/c/i64_sdiv.c b/runtime/c/i64_sdiv.c new file mode 100644 index 00000000..3f21d9b7 --- /dev/null +++ b/runtime/c/i64_sdiv.c @@ -0,0 +1,51 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Signed division */ + +signed long long __i64_sdiv(signed long long n, signed long long d) +{ + unsigned long long un, ud, uq, ur; + int nh = n >> 32, dh = d >> 32; + /* Take absolute values of n and d */ + un = nh < 0 ? -n : n; + ud = dh < 0 ? -d : d; + uq = __i64_udivmod(un, ud, &ur); + /* Apply sign to quotient */ + return (nh ^ dh) < 0 ? -uq : uq; +} diff --git a/runtime/c/i64_shl.c b/runtime/c/i64_shl.c new file mode 100644 index 00000000..9b9aae57 --- /dev/null +++ b/runtime/c/i64_shl.c @@ -0,0 +1,55 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Shift left */ + +unsigned long long __i64_shl(unsigned long long x, int amount) +{ + unsigned xl = x, xh = x >> 32; + amount = amount & 63; + if (amount == 0) { + return x; + } + else if (amount < 32) { + unsigned rl = xl << amount; + unsigned rh = (xh << amount) | (xl >> (32 - amount)); + return rl | ((unsigned long long) rh << 32); + } else { + return ((unsigned long long) (xl << (amount - 32))) << 32; + } +} diff --git a/runtime/c/i64_shr.c b/runtime/c/i64_shr.c new file mode 100644 index 00000000..c1db2a5f --- /dev/null +++ b/runtime/c/i64_shr.c @@ -0,0 +1,55 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Shift right unsigned */ + +unsigned long long __i64_shr(unsigned long long x, int amount) +{ + unsigned xl = x, xh = x >> 32; + amount = amount & 63; + if (amount == 0) { + return x; + } + else if (amount < 32) { + unsigned rl = (xl >> amount) | (xh << (32 - amount)); + unsigned rh = xh >> amount; + return rl | ((unsigned long long) rh << 32); + } else { + return (unsigned long long) (xh >> (amount - 32)); + } +} diff --git a/runtime/c/i64_smod.c b/runtime/c/i64_smod.c new file mode 100644 index 00000000..ab15b6e6 --- /dev/null +++ b/runtime/c/i64_smod.c @@ -0,0 +1,51 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Signed remainder */ + +signed long long __i64_smod(signed long long n, signed long long d) +{ + unsigned long long un, ud, ur; + int nh = n >> 32, dh = d >> 32; + /* Take absolute values of n and d */ + un = nh < 0 ? -n : n; + ud = dh < 0 ? -d : d; + (void) __i64_udivmod(un, ud, &ur); + /* Apply sign to remainder */ + return nh < 0 ? -ur : ur; +} diff --git a/runtime/c/i64_stod.c b/runtime/c/i64_stod.c new file mode 100644 index 00000000..158b6892 --- /dev/null +++ b/runtime/c/i64_stod.c @@ -0,0 +1,46 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Conversion from signed int64 to float64 */ + +double __i64_stod(signed long long x) +{ + unsigned xl = x; + signed xh = x >> 32; + return (double) xl + 0x1p+32 * (double) xh; +} diff --git a/runtime/c/i64_stof.c b/runtime/c/i64_stof.c new file mode 100644 index 00000000..8410ba13 --- /dev/null +++ b/runtime/c/i64_stof.c @@ -0,0 +1,56 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Conversion from signed int64 to float32 */ + +float __i64_stof(signed long long x) +{ + if (x < -(1LL << 53) || x >= (1LL << 53)) { + /* x is large enough that double rounding can occur. + Nudge x away from the points where double rounding occurs + (the "round to odd" technique) */ + unsigned delta = ((unsigned) x & 0x7FF) + 0x7FF; + x = (x | delta) & ~0x7FFLL; + } + /* Convert to double */ + unsigned xl = x; + signed xh = x >> 32; + double r = (double) xl + 0x1.0p32 * (double) xh; + /* Round to single */ + return (float) r; +} diff --git a/runtime/c/i64_udiv.c b/runtime/c/i64_udiv.c new file mode 100644 index 00000000..91fbf6e4 --- /dev/null +++ b/runtime/c/i64_udiv.c @@ -0,0 +1,45 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Unsigned division */ + +unsigned long long __i64_udiv(unsigned long long n, unsigned long long d) +{ + unsigned long long r; + return __i64_udivmod(n, d, &r); +} diff --git a/runtime/c/i64_udivmod.c b/runtime/c/i64_udivmod.c new file mode 100644 index 00000000..d8f5073a --- /dev/null +++ b/runtime/c/i64_udivmod.c @@ -0,0 +1,158 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include <stddef.h> +#include "i64.h" + +static unsigned __i64_udiv6432(unsigned u1, unsigned u0, + unsigned v, unsigned *r); +static int __i64_nlz(unsigned x); + +/* Unsigned division and remainder */ + +unsigned long long __i64_udivmod(unsigned long long n, + unsigned long long d, + unsigned long long * rp) +{ + unsigned dh = d >> 32; + if (dh == 0) { + unsigned nh = n >> 32; + if (nh == 0) { + /* Special case 32 / 32 */ + unsigned nl = n; + unsigned dl = d; + *rp = (unsigned long long) (nl % dl); + return (unsigned long long) (nl / dl); + } else { + /* Special case 64 / 32 */ + unsigned nl = n; + unsigned dl = d; + unsigned qh = nh / dl; + unsigned rl; + unsigned ql = __i64_udiv6432(nh % dl, nl, dl, &rl); + *rp = (unsigned long long) rl; /* high word of remainder is 0 */ + return ((unsigned long long) qh) << 32 | ql; + } + } else { + /* General case 64 / 64 */ + unsigned dl = d; + /* Scale N and D down, giving N' and D' such that 2^31 <= D' < 2^32 */ + int s = 32 - __i64_nlz(dh); /* shift amount, between 1 and 32 */ + unsigned long long np = __i64_shr(n, s); + unsigned dp = (unsigned) __i64_shr(d, s); + /* Divide N' by D' to get an approximate quotient Q */ + unsigned q = __i64_udiv6432(np >> 32, np, dp, NULL); + again: ; + /* Tentative quotient Q is either correct or one too high */ + /* Compute Q * D, checking for overflow */ + unsigned long long p1 = (unsigned long long) dl * q; + unsigned long long p2 = (unsigned long long) (dh * q) << 32; + unsigned long long p = p1 + p2; + if (p < p1) { + /* Overflow occurred: adjust Q down by 1 and redo check */ + q = q - 1; goto again; + } + /* Compute remainder R */ + unsigned long long r = n - p; + if (n < p) { + /* Q is one too high, adjust Q down by 1 and R up by D */ + q = q - 1; r = r + d; + } + *rp = r; + return (unsigned long long) q; + } +} + +/* Unsigned division and remainder for 64 bits divided by 32 bits. */ +/* This is algorithm "divlu" from _Hacker's Delight_, fig 9.3 */ + +static unsigned __i64_udiv6432(unsigned u1, unsigned u0, + unsigned v, unsigned *r) +{ + const unsigned b = 65536; // Number base (16 bits). + unsigned un1, un0, // Norm. dividend LSD's. + vn1, vn0, // Norm. divisor digits. + q1, q0, // Quotient digits. + un32, un21, un10,// Divided digit pairs. + rhat; // A remainder. + int s; // Shift amount for norm. + + if (u1 >= v) { // If overflow, + if (r != NULL) *r = 0xFFFFFFFFU; // set rem to an impossible value, + return 0xFFFFFFFFU; // and return largest possible quotient. + } + s = __i64_nlz(v); // 0 <= s <= 31. + v = v << s; // Normalize divisor. + vn1 = v >> 16; // Break divisor up into + vn0 = v & 0xFFFF; // two 16-bit digits. + un32 = (u1 << s) | ((u0 >> (32 - s)) & (-s >> 31)); + un10 = u0 << s; // Shift dividend left. + un1 = un10 >> 16; // Break right half of + un0 = un10 & 0xFFFF; // dividend into two digits. + q1 = un32/vn1; // Compute the first quotient digit, q1. + rhat = un32 - q1*vn1; + again1: + if (q1 >= b || q1*vn0 > b*rhat + un1) { + q1 = q1 - 1; + rhat = rhat + vn1; + if (rhat < b) goto again1; + } + un21 = un32*b + un1 - q1*v; // Multiply and subtract. + q0 = un21/vn1; // Compute the second quotient digit, q0 + rhat = un21 - q0*vn1; +again2: + if (q0 >= b || q0*vn0 > b*rhat + un0) { + q0 = q0 - 1; + rhat = rhat + vn1; + if (rhat < b) goto again2; + } + if (r != NULL) *r = (un21*b + un0 - q0*v) >> s; + return q1*b + q0; +} + +/* Number of leading zeroes */ + +static int __i64_nlz(unsigned x) +{ + if (x == 0) return 32; + int n = 0; + if (x <= 0x0000FFFF) { n += 16; x <<= 16; } + if (x <= 0x00FFFFFF) { n += 8; x <<= 8; } + if (x <= 0x0FFFFFFF) { n += 4; x <<= 4; } + if (x <= 0x3FFFFFFF) { n += 2; x <<= 2; } + if (x <= 0x7FFFFFFF) { n += 1; x <<= 1; } + return n; +} diff --git a/runtime/c/i64_umod.c b/runtime/c/i64_umod.c new file mode 100644 index 00000000..d30e29c4 --- /dev/null +++ b/runtime/c/i64_umod.c @@ -0,0 +1,46 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Unsigned remainder */ + +unsigned long long __i64_umod(unsigned long long n, unsigned long long d) +{ + unsigned long long r; + (void) __i64_udivmod(n, d, &r); + return r; +} diff --git a/runtime/c/i64_utod.c b/runtime/c/i64_utod.c new file mode 100644 index 00000000..e70820a9 --- /dev/null +++ b/runtime/c/i64_utod.c @@ -0,0 +1,45 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Conversion from unsigned int64 to float64 */ + +double __i64_utod(unsigned long long x) +{ + unsigned xl = x, xh = x >> 32; + return (double) xl + 0x1.0p32 * (double) xh; +} diff --git a/runtime/c/i64_utof.c b/runtime/c/i64_utof.c new file mode 100644 index 00000000..87b85bfc --- /dev/null +++ b/runtime/c/i64_utof.c @@ -0,0 +1,55 @@ +/***************************************************************** + * + * The Compcert verified compiler + * + * Xavier Leroy, INRIA Paris-Rocquencourt + * + * Copyright (c) 2013 Institut National de Recherche en Informatique et + * en Automatique. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * * Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * * Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * * Neither the name of the <organization> nor the + * names of its contributors may be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT + * HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + **********************************************************************/ + +/* Helper functions for 64-bit integer arithmetic. Reference C implementation */ + +#include "i64.h" + +/* Conversion from unsigned int64 to float32 */ + +float __i64_utof(unsigned long long x) +{ + if (x >= 1ULL << 53) { + /* x is large enough that double rounding can occur. + Nudge x away from the points where double rounding occurs + (the "round to odd" technique) */ + unsigned delta = ((unsigned) x & 0x7FF) + 0x7FF; + x = (x | delta) & ~0x7FFULL; + } + /* Convert to double */ + unsigned xl = x, xh = x >> 32; + double r = (double) xl + 0x1.0p32 * (double) xh; + /* Round to single */ + return (float) r; +} diff --git a/runtime/test/test_int64.c b/runtime/test/test_int64.c index ab7a231d..58a129b6 100644 --- a/runtime/test/test_int64.c +++ b/runtime/test/test_int64.c @@ -158,17 +158,21 @@ static void test1(u64 x, u64 y) u = __i64_stof(x); v = (float) (s64) x; if (u != v) - error++, printf("(double) %lld (s) = %a, expected %a\n", x, u, v); + error++, printf("(float) %lld (s) = %a, expected %a\n", x, u, v); f = (double) x; - z = __i64_dtou(f); - if (z != (u64) f) - error++, printf("(u64) %a = %llu, expected %llu\n", f, z, (u64) f); + if (f >= 0 && f < 0x1p+64) { + z = __i64_dtou(f); + if (z != (u64) f) + error++, printf("(u64) %a = %llu, expected %llu\n", f, z, (u64) f); + } f = (double) (s64) x; - t = __i64_dtos(f); - if (t != (s64) f) - error++, printf("(s64) %a = %lld, expected %lld\n", f, z, (s64) f); + if (f >= -0x1p+63 && f < 0x1p+63) { + t = __i64_dtos(f); + if (t != (s64) f) + error++, printf("(s64) %a = %lld, expected %lld\n", f, z, (s64) f); + } f = ((double) x) * 0.0001; z = __i64_dtou(f); |