From 10418197c8393673d8bd5b28fcaf26c48ad11429 Mon Sep 17 00:00:00 2001 From: Adrien Guatto Date: Thu, 28 Apr 2011 15:20:21 +0200 Subject: [PATCH] Initial support for return-less external functions. The compiler still does not support unsafe functions that well. For example, putting an assert()/exit() in an automaton's state does not work correctly. --- compiler/global/clocks.ml | 5 +++-- compiler/heptagon/parsing/hept_parser.mly | 1 + compiler/main/mls2obc.ml | 10 ++++++++-- compiler/obc/c/cgen.ml | 7 ++++++- compiler/obc/java/java.ml | 2 +- compiler/obc/java/java_main.ml | 3 ++- compiler/obc/java/java_printer.ml | 5 ++++- compiler/obc/java/obc2java.ml | 9 +++++---- compiler/obc/obc.ml | 1 + compiler/obc/obc_mapfold.ml | 3 +++ compiler/obc/obc_printer.ml | 2 ++ 11 files changed, 36 insertions(+), 12 deletions(-) diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 5e1a4f3..e818cc5 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -78,8 +78,9 @@ let rec unify_ck ck1 ck2 = let rec unify t1 t2 = if t1 == t2 then () else match (t1, t2) with - | (Ck Cbase, Cprod []) - | (Cprod [], Ck Cbase) -> () + | (Ck (Cbase | Cvar { contents = Cindex _; }), Cprod []) + | (Cprod [], Ck (Cbase | Cvar { contents = Cindex _; })) -> + () | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2 | (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list | _ -> raise Unify diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index e3ad86f..30d2fdc 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -383,6 +383,7 @@ pat: ; ids: + | {[]} | pat COMMA pat {[$1; $3]} | pat COMMA ids {$1 :: $3} ; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 93862f0..411e289 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -431,8 +431,14 @@ and translate_eq_list map call_context act_list = and mk_node_call map call_context app loc name_list args ty = match app.Minils.a_op with | Minils.Efun f when Mls_utils.is_op f -> - let e = mk_exp ty (Eop(f, args)) in - [], [], [], [Aassgn(List.hd name_list, e)] + let act = match name_list with + | [] -> Aop (f, args) + | [name] -> + let e = mk_exp ty (Eop(f, args)) in + Aassgn (name, e) + | _ -> + Misc.unsupported "mls2obc: external function with multiple return values" 1 in + [], [], [], [act] | Minils.Enode f when Itfusion.is_anon_node f -> let add_input env vd = Env.add vd.Minils.v_ident diff --git a/compiler/obc/c/cgen.ml b/compiler/obc/c/cgen.ml index 6c1a231..7dd2028 100644 --- a/compiler/obc/c/cgen.ml +++ b/compiler/obc/c/cgen.ml @@ -487,6 +487,11 @@ let rec cstm_of_act var_env obj_env act = let ce = cexpr_of_exp var_env e in create_affect_stm vn ce ty + (** Our Aop marks an operator invocation that will perform side effects. Just + translate to a simple C statement. *) + | Aop (op_name, args) -> + [Csexpr (cop_of_op var_env op_name args)] + (** Reinitialization of an object variable, extracting the reset function's name from our environment [obj_env]. *) | Acall (name_list, o, Mreset, args) -> @@ -743,7 +748,7 @@ let cfile_list_of_oprog_ty_decls name oprog = let (cty_defs, cty_decls) = List.split cdefs_and_cdecls in let filename_types = name ^ "_types" in let types_h = (filename_types ^ ".h", - Cheader (["stdbool"], List.concat cty_decls)) in + Cheader (["stdbool"; "assert"], List.concat cty_decls)) in let types_c = (filename_types ^ ".c", Csource (concat cty_defs)) in filename_types, [types_h; types_c] diff --git a/compiler/obc/java/java.ml b/compiler/obc/java/java.ml index 93e42b5..7d00a34 100644 --- a/compiler/obc/java/java.ml +++ b/compiler/obc/java/java.ml @@ -66,7 +66,7 @@ and block = { b_locals : var_dec list; and act = Anewvar of var_dec * exp | Aassgn of pattern * exp - | Amethod_call of exp * method_name * exp list + | Aexp of exp | Aswitch of exp * (constructor_name * block) list | Aif of exp * block | Aifelse of exp * block * block diff --git a/compiler/obc/java/java_main.ml b/compiler/obc/java/java_main.ml index d321f5a..d4f128e 100644 --- a/compiler/obc/java/java_main.ml +++ b/compiler/obc/java/java_main.ml @@ -64,7 +64,8 @@ let program p = , mk_block [Aassgn(pat_step, Eval (Pvar id_step_dnb))]); Obc2java.fresh_for (Eval pat_step) (fun i -> - [ Amethod_call(out, "printf", [ Sstring "%d => %s\\n"; Eval (Pvar i); print_ret]) ] + [Aexp (Emethod_call(out, "printf", + [Sstring "%d => %s\\n"; Eval (Pvar i); print_ret]))] ) ] in diff --git a/compiler/obc/java/java_printer.ml b/compiler/obc/java/java_printer.ml index db3e290..0903a1f 100644 --- a/compiler/obc/java/java_printer.ml +++ b/compiler/obc/java/java_printer.ml @@ -117,6 +117,9 @@ and op ff (f, e_l) = | "~-" -> let e = Misc.assert_1 e_l in fprintf ff "-%a" exp e + | "assert" -> + let e = Misc.assert_1 e_l in + fprintf ff "assert(%a)" exp e | s -> fprintf ff "jeptagon.Pervasives.%s%a" s args e_l) (* TODO java deal with this correctly bug when using Pervasives.ggg in the code but works when using ggg directly *) @@ -146,7 +149,7 @@ and switch_hack ff c_b_l = and act ff = function | Anewvar (vd,e) -> fprintf ff "@[<4>%a =@ %a;@]" (var_dec false) vd exp e | Aassgn (p,e) -> fprintf ff "@[<4>%a =@ %a;@]" pattern p exp e - | Amethod_call (o,m,e_l) -> fprintf ff "@[%a.%a%a;@]" exp o method_name m args e_l + | Aexp e -> fprintf ff "@[%a@];" exp e | Aswitch (e, c_b_l) -> let pcb ff (c,b) = fprintf ff "@[case %a:@ %a@ break;@]" bare_constructor_name c block b in diff --git a/compiler/obc/java/obc2java.ml b/compiler/obc/java/obc2java.ml index 8fbc5ed..611adb3 100644 --- a/compiler/obc/java/obc2java.ml +++ b/compiler/obc/java/obc2java.ml @@ -174,9 +174,10 @@ let obj_ref param_env o = match o with let rec act_list param_env act_l acts = let _act act acts = match act with | Obc.Aassgn (p,e) -> (Aassgn (pattern param_env p, exp param_env e))::acts + | Obc.Aop (op,e_l) -> Aexp (Efun (op, exp_list param_env e_l)) :: acts | Obc.Acall ([], obj, Mstep, e_l) -> - let acall = Amethod_call (obj_ref param_env obj, "step", exp_list param_env e_l) in - acall::acts + let acall = Emethod_call (obj_ref param_env obj, "step", exp_list param_env e_l) in + Aexp acall::acts | Obc.Acall ([p], obj, Mstep, e_l) -> let ecall = Emethod_call (obj_ref param_env obj, "step", exp_list param_env e_l) in let assgn = Aassgn (pattern param_env p, ecall) in @@ -201,8 +202,8 @@ let rec act_list param_env act_l acts = let copies = Misc.mapi copy_return_to_var p_l in assgn::(copies@acts) | Obc.Acall (_, obj, Mreset, _) -> - let acall = Amethod_call (obj_ref param_env obj, "reset", []) in - acall::acts + let acall = Emethod_call (obj_ref param_env obj, "reset", []) in + Aexp acall::acts | Obc.Acase (e, c_b_l) when e.e_ty = Types.Tid Initial.pbool -> (match c_b_l with | [] -> acts diff --git a/compiler/obc/obc.ml b/compiler/obc/obc.ml index a0f9703..d532dd0 100644 --- a/compiler/obc/obc.ml +++ b/compiler/obc/obc.ml @@ -67,6 +67,7 @@ type method_name = type act = | Aassgn of pattern * exp + | Aop of op_name * exp list | Acall of pattern list * obj_ref * method_name * exp list | Acase of exp * (constructor_name * block) list | Afor of var_dec * exp * exp * block diff --git a/compiler/obc/obc_mapfold.ml b/compiler/obc/obc_mapfold.ml index 1f49d00..ea36e21 100644 --- a/compiler/obc/obc_mapfold.ml +++ b/compiler/obc/obc_mapfold.ml @@ -92,6 +92,9 @@ and act funs acc a = match a with let lhs, acc = lhs_it funs acc lhs in let e, acc = exp_it funs acc e in Aassgn(lhs, e), acc + | Aop(op_name, args) -> + let args, acc = mapfold (exp_it funs) acc args in + Aop(op_name, args), acc | Acall(lhs_list, obj, n, args) -> let lhs_list, acc = mapfold (lhs_it funs) acc lhs_list in let args, acc = mapfold (exp_it funs) acc args in diff --git a/compiler/obc/obc_printer.ml b/compiler/obc/obc_printer.ml index d068ac9..33852f4 100644 --- a/compiler/obc/obc_printer.ml +++ b/compiler/obc/obc_printer.ml @@ -93,6 +93,8 @@ let rec print_act ff a = print_exp i1 print_exp i2 print_block act_list + | Aop (op, es) -> + print_op ff op es | Acall (var_list, o, meth, es) -> fprintf ff "@[<2>%a%a.%a(%a)@]" print_lhs_tuple var_list