diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CMparser.mly | 4 | ||||
-rw-r--r-- | backend/Cminor.v | 6 | ||||
-rw-r--r-- | backend/CminorSel.v | 2 | ||||
-rw-r--r-- | backend/LTL.v | 4 | ||||
-rw-r--r-- | backend/Linear.v | 4 | ||||
-rw-r--r-- | backend/Mach.v | 2 | ||||
-rw-r--r-- | backend/PrintCminor.ml | 13 | ||||
-rw-r--r-- | backend/RTL.v | 2 | ||||
-rw-r--r-- | backend/SelectLong.vp | 14 |
9 files changed, 26 insertions, 25 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b28578e1..5d93b84a 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -490,9 +490,9 @@ proc: signature: type_ - { {sig_args = []; sig_res = Some $1} } + { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} } | VOID - { {sig_args = []; sig_res = None} } + { {sig_args = []; sig_res = None; sig_cc = cc_default} } | type_ MINUSGREATER signature { let s = $3 in {s with sig_args = $1 :: s.sig_args} } ; diff --git a/backend/Cminor.v b/backend/Cminor.v index 9f7244b9..c12c6fce 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -532,7 +532,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate f nil Kstop m0). (** A final state is a [Returnstate] with an empty continuation. *) @@ -811,7 +811,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> eval_funcall ge m0 f nil t m (Vint r) -> bigstep_program_terminates p t r. @@ -822,7 +822,7 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index c80f424d..db414a2c 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -390,7 +390,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate f nil Kstop m0). Inductive final_state: state -> int -> Prop := diff --git a/backend/LTL.v b/backend/LTL.v index e60600a2..dd79c8e3 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -295,12 +295,12 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result (mksignature nil (Some Tint)) = r :: nil -> + loc_result signature_main = r :: nil -> rs (R r) = Vint retcode -> final_state (Returnstate nil rs m) retcode. diff --git a/backend/Linear.v b/backend/Linear.v index 3c524368..56d1eb99 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -269,12 +269,12 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result (mksignature nil (Some Tint)) = r :: nil -> + loc_result signature_main = r :: nil -> rs (R r) = Vint retcode -> final_state (Returnstate nil rs m) retcode. diff --git a/backend/Mach.v b/backend/Mach.v index f0fb56ae..ff72a828 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -427,7 +427,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result (mksignature nil (Some Tint)) = r :: nil -> + loc_result signature_main = r :: nil -> rs r = Vint retcode -> final_state (Returnstate nil rs m) retcode. diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 33c38f56..4c53c5ea 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -172,12 +172,13 @@ let name_of_type = function | Tlong -> "long" | Tsingle -> "single" -let rec print_sig p = function - | {sig_args = []; sig_res = None} -> fprintf p "void" - | {sig_args = []; sig_res = Some ty} -> fprintf p "%s" (name_of_type ty) - | {sig_args = t1 :: tl; sig_res = tres} -> - fprintf p "%s ->@ " (name_of_type t1); - print_sig p {sig_args = tl; sig_res = tres} +let print_sig p sg = + List.iter + (fun t -> fprintf p "%s ->@ " (name_of_type t)) + sg.sig_args; + match sg.sig_res with + | None -> fprintf p "void" + | Some ty -> fprintf p "%s" (name_of_type ty) let rec just_skips s = match s with diff --git a/backend/RTL.v b/backend/RTL.v index b2e1e89c..045250da 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -331,7 +331,7 @@ Inductive initial_state (p: program): state -> Prop := Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> - funsig f = mksignature nil (Some Tint) -> + funsig f = signature_main -> initial_state p (Callstate nil f nil m0). (** A final state is a [Returnstate] with an empty call stack. *) diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 76cc79d2..09f29afc 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -46,13 +46,13 @@ Record helper_functions : Type := mk_helper_functions { i64_sar: ident (**r shift right signed *) }. -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong). -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat). -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle). -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong). -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong). -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong). -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong). +Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. Section SELECT. |