From cbc834b32abcc27993201c015da6cc1d1cd15528 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 22:36:42 +0100 Subject: [PATCH] [ast2C] constants, simple assignations, variables (+ one fix about pre storage) --- src/ast_to_c.ml | 109 +++++++++++++++++++++++++------------- src/cast.ml | 26 +++++++++ src/cprint.ml | 35 ++++++++++++ src/ctranslation.ml | 40 ++++++++++++++ src/intermediate_ast.ml | 20 +++---- src/intermediate_utils.ml | 14 ++--- src/main.ml | 4 +- 7 files changed, 191 insertions(+), 57 deletions(-) create mode 100644 src/cast.ml create mode 100644 src/ctranslation.ml diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 618cb11..5756bdb 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -3,44 +3,45 @@ open Intermediate_ast open Intermediate_utils open Cprint open Utils +open Ctranslation -(** [ast_to_cast] translates a [t_nodelist] into a [i_nodelist] *) -let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist = +(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *) +let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist = let c = ref 1 in - let ast_to_cast_varlist vl = snd vl in - let rec ast_to_cast_expr hloc = function + let ast_to_intermediate_ast_varlist vl = snd vl in + let rec ast_to_intermediate_ast_expr hloc = function | EVar (_, v) -> begin match Hashtbl.find_opt hloc (v, false) with - | None -> IVar (CVInput (name_of_var v)) - | Some (s, i) -> IVar (CVStored (s, i)) + | None -> IEVar (CVInput (name_of_var v)) + | Some (s, i) -> IEVar (CVStored (s, i)) end - | EMonOp (_, op, e) -> IMonOp (op, ast_to_cast_expr hloc e) + | EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e) | EBinOp (_, op, e, e') -> - IBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') | ETriOp (_, op, e, e', e'') -> - ITriOp - (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e', ast_to_cast_expr hloc e'') + IETriOp + (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e', ast_to_intermediate_ast_expr hloc e'') | EComp (_, op, e, e') -> - IComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IEComp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') | EWhen (_, e, e') -> - IWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IEWhen (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') | EReset (_, e, e') -> - IReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') - | EConst (_, c) -> IConst c - | ETuple (_, l) -> ITuple (List.map (ast_to_cast_expr hloc) l) + IEReset (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e') + | EConst (_, c) -> IEConst c + | ETuple (_, l) -> IETuple (List.map (ast_to_intermediate_ast_expr hloc) l) | EApp (_, n, e) -> begin - let e = ast_to_cast_expr hloc e in - let res = IApp (!c, n, e) in + let e = ast_to_intermediate_ast_expr hloc e in + let res = IEApp (!c, n, e) in let () = incr c in res end in - let ast_to_cast_eq hloc (patt, expr) : i_equation = - (ast_to_cast_varlist patt, ast_to_cast_expr hloc expr) in + let ast_to_intermediate_ast_eq hloc (patt, expr) : i_equation = + (ast_to_intermediate_ast_varlist patt, ast_to_intermediate_ast_expr hloc expr) in List.map begin fun node -> @@ -48,10 +49,10 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist = let hloc = (Hashtbl.find h node.n_name).nt_map in { in_name = node.n_name; - in_inputs = ast_to_cast_varlist node.n_inputs; - in_outputs = ast_to_cast_varlist node.n_outputs; - in_local_vars = ast_to_cast_varlist node.n_local_vars; - in_equations = List.map (ast_to_cast_eq hloc) node.n_equations; + in_inputs = ast_to_intermediate_ast_varlist node.n_inputs; + in_outputs = ast_to_intermediate_ast_varlist node.n_outputs; + in_local_vars = ast_to_intermediate_ast_varlist node.n_local_vars; + in_equations = List.map (ast_to_intermediate_ast_eq hloc) node.n_equations; } end nodes @@ -71,8 +72,11 @@ let make_state_types nodes: node_states = let vars = List.filter (fun v -> type_var v = [ty]) (snd (varlist_concat node.n_outputs node.n_local_vars)) in + let all_vars = + List.filter (fun v -> type_var v = [ty]) + (snd (varlist_concat (varlist_concat node.n_inputs node.n_outputs) node.n_local_vars)) in let pre_vars = - List.filter (fun v -> List.mem v pv) vars in + List.filter (fun v -> List.mem v pv) all_vars in let nb = (List.length vars) + (List.length pre_vars) in let tyh = Hashtbl.create nb in let i = @@ -205,10 +209,16 @@ let cp_prevars fmt (node, h) = "\n\t/* Remember the values used in the [pre] construct */\n"; List.iter (fun v -> (** Note that «dst_array = src_array» should hold. *) - let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in - let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in - Format.fprintf fmt "\t%s[%d] = %s[%d];\n" - dst_array dst_idx src_array src_idx) + match Hashtbl.find_opt node_st.nt_map (v, false) with + | Some (src_array, src_idx) -> + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + dst_array dst_idx src_array src_idx + | None -> + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s;\n" + dst_array dst_idx (Utils.name_of_var v) + ) l @@ -241,20 +251,13 @@ let cp_init_aux_nodes fmt (node, h) = -(** The following function prints one equation of the program into a set of - * instruction ending in assignments. *) -let cp_equation fmt (eq, hloc) = - Format.fprintf fmt "\t\t/* TODO! */\n" - - - (** [cp_equations] prints the node equations. *) let rec cp_equations fmt (eqs, hloc) = match eqs with | [] -> () | eq :: eqs -> Format.fprintf fmt "%a%a" - cp_equation (eq, hloc) + cp_expression (equation_to_expression (hloc.nt_map, eq), hloc) cp_equations (eqs, hloc) (** [cp_node] prints a single node *) @@ -276,10 +279,40 @@ let rec cp_nodes fmt (nodes, h) = +let dump_var_locations (st: node_states) = + Hashtbl.iter + (fun n st -> + Format.printf "\n\n\tNODE: %s\n" n; + Hashtbl.iter + (fun ((v: t_var), (ispre: bool)) ((arr: string), (idx: int)) -> + match v, ispre with + | IVar s, true -> Format.printf "PRE Variable (int) %s stored as %s[%d]\n" + s arr idx + | BVar s, true -> Format.printf "PRE Variable (bool) %s stored as %s[%d]\n" + s arr idx + | RVar s, true -> Format.printf "PRE Variable (real) %s stored as %s[%d]\n" + s arr idx + | IVar s, false -> Format.printf "Variable (int) %s stored as %s[%d]\n" + s arr idx + | BVar s, false -> Format.printf "Variable (bool) %s stored as %s[%d]\n" + s arr idx + | RVar s, false -> Format.printf "Variable (real) %s stored as %s[%d]\n" + s arr idx) + st.nt_map) + st; + Format.printf "\n\n" + + + (** main function that prints a C-code from a term of type [t_nodelist]. *) -let ast_to_c prog = +let ast_to_c (debug: bool) prog = let prog_st_types = make_state_types prog in - let prog: i_nodelist = ast_to_cast prog prog_st_types in + let () = + if debug + then dump_var_locations prog_st_types + else () + in + let prog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" cp_includes (Config.c_includes) cp_state_types prog_st_types diff --git a/src/cast.ml b/src/cast.ml new file mode 100644 index 0000000..4bc3282 --- /dev/null +++ b/src/cast.ml @@ -0,0 +1,26 @@ +open Intermediate_ast +open Ast + +(** This file contains a small subset of the syntax of C required for the + * translation. *) + +(** A [c_block] represents a block in C. *) +type c_block = c_expression list + +(** A [c_expresion] represents a C expression, which can need sequences and + * function calls. *) +and c_expression = + | CAssign of c_var * c_value + | CSeq of c_expression * c_expression + | CIf of c_value * c_block * c_block + | CApplication of c_var list * c_expression + +(** A value here is anything that can be inlined into a single C expression + * containing no function call, condition, ... *) +and c_value = + | CVariable of c_var + | CMonOp of monop * c_value + | CBinOp of binop * c_value * c_value + | CComp of compop * c_value * c_value + | CConst of const + diff --git a/src/cprint.ml b/src/cprint.ml index 39da179..b3e8742 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -1,6 +1,7 @@ open Intermediate_utils open Intermediate_ast open Ast +open Cast (** This file contains extrimely simple functions printing C code. *) @@ -76,3 +77,37 @@ let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = cp_prototype (node, h) cp_prototypes (nodes, h) + + +let cp_value fmt value = + match value with + | CVariable (CVInput s) -> Format.fprintf fmt "%s" s + | CVariable (CVStored (arr, idx)) -> + Format.fprintf fmt "%s[%d]" arr idx + | CConst (CInt i) -> Format.fprintf fmt "%d" i + | CConst (CBool true) -> Format.fprintf fmt "true" + | CConst (CBool false) -> Format.fprintf fmt "false" + | CConst (CReal r) -> Format.fprintf fmt "%f" r + (**| CMonOp of monop * c_value + | CBinOp of binop * c_value * c_value + | CComp of compop * c_value * c_value*) + | _ -> failwith "[cprint.ml] TODO!" + + + + +(** The following function prints one transformed equation of the program into a + * set of instruction ending in assignments. *) +let cp_expression fmt (expr, hloc) = + let prefix = "\t" in + match expr with + | CAssign (CVStored (arr, idx), value) -> + begin + Format.fprintf fmt "%s%s[%d] = %a;\n" + prefix arr idx cp_value value + end + | CAssign (CVInput _, _) -> failwith "should not happend." + (*| CSeq of c_expression * c_expression + | CIf of c_value * c_block * c_block + | CApplication of c_var list * c_expression*) + | _ -> failwith "[cprint.ml] TODO!" diff --git a/src/ctranslation.ml b/src/ctranslation.ml new file mode 100644 index 0000000..aab6548 --- /dev/null +++ b/src/ctranslation.ml @@ -0,0 +1,40 @@ +open Ast +open Intermediate_ast +open Cast + +let iexpression_to_cvalue e = () + +let equation_to_expression (hloc, ((vl, expr): i_equation)) : c_expression = + let fetch_unique_var () = + match vl with + | [v] -> + begin + match Hashtbl.find_opt hloc (v, false) with + | None -> CVInput (Utils.name_of_var v) + | Some (arr, idx) -> CVStored (arr, idx) + end + | _ -> failwith "[ctranslation.ml] This should not happened." + in + match expr with + | IEVar vsrc -> + CAssign (fetch_unique_var (), CVariable vsrc) + | IEMonOp (MOp_pre, IEVar v) -> + CAssign (fetch_unique_var (), CVariable v) + | IEConst c -> + CAssign (fetch_unique_var (), CConst c) + (*| IEMonOp (op, e) -> + CMonOp (op, iexpression_to_cvalue e) + | IEBinOp (op, e, e') -> + CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') + | IEComp (op, e, e') -> + CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e') + | IEConst c -> CConst c + TODO! + | IETriOp of triop * i_expression * i_expression * i_expression + | IEWhen of i_expression * i_expression + | IEReset of i_expression * i_expression + | IETuple of (i_expression list) + (** [CApp] below represents the n-th call to an aux node *) + | IEApp of int * t_node * i_expression*) + | _ -> failwith "[ctranslation.ml] TODO!" + diff --git a/src/intermediate_ast.ml b/src/intermediate_ast.ml index 3cc296b..4c520bf 100644 --- a/src/intermediate_ast.ml +++ b/src/intermediate_ast.ml @@ -45,17 +45,17 @@ type c_var = | CVInput of ident type i_expression = - | IVar of c_var - | IMonOp of monop * i_expression - | IBinOp of binop * i_expression * i_expression - | ITriOp of triop * i_expression * i_expression * i_expression - | IComp of compop * i_expression * i_expression - | IWhen of i_expression * i_expression - | IReset of i_expression * i_expression - | IConst of const - | ITuple of (i_expression list) + | IEVar of c_var + | IEMonOp of monop * i_expression + | IEBinOp of binop * i_expression * i_expression + | IETriOp of triop * i_expression * i_expression * i_expression + | IEComp of compop * i_expression * i_expression + | IEWhen of i_expression * i_expression + | IEReset of i_expression * i_expression + | IEConst of const + | IETuple of (i_expression list) (** [CApp] below represents the n-th call to an aux node *) - | IApp of int * t_node * i_expression + | IEApp of int * t_node * i_expression and i_varlist = t_var list diff --git a/src/intermediate_utils.ml b/src/intermediate_utils.ml index 34414d1..26804f8 100644 --- a/src/intermediate_utils.ml +++ b/src/intermediate_utils.ml @@ -2,15 +2,15 @@ open Intermediate_ast let rec find_app_opt eqs i = let rec find_app_expr_opt i = function - | IVar _ | IConst _ -> None - | IMonOp (_, e) -> find_app_expr_opt i e - | IReset (e, e') | IWhen (e, e') | IComp (_, e, e') | IBinOp (_, e, e') -> + | IEVar _ | IEConst _ -> None + | IEMonOp (_, e) -> find_app_expr_opt i e + | IEReset (e, e') | IEWhen (e, e') | IEComp (_, e, e') | IEBinOp (_, e, e') -> begin match find_app_expr_opt i e with | None -> find_app_expr_opt i e' | Some n -> Some n end - | ITriOp (_, e, e', e'') -> + | IETriOp (_, e, e', e'') -> begin match find_app_expr_opt i e with | None -> @@ -21,15 +21,15 @@ let rec find_app_opt eqs i = end | Some n -> Some n end - | ITuple l -> + | IETuple l -> List.fold_left (fun acc e -> match acc, find_app_expr_opt i e with | Some n, _ -> Some n | None, v -> v) None l - (** [IApp] below represents the n-th call to an aux node *) - | IApp (j, n, e) -> + (** [IEApp] below represents the n-th call to an aux node *) + | IEApp (j, n, e) -> if i = j then Some n else find_app_expr_opt i e diff --git a/src/main.ml b/src/main.ml index 80c3678..78e1dc1 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"; "clock_unification"] in + let default_passes = [] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -127,6 +127,6 @@ let _ = else ( if !nopopt then (fun _ -> ()) - else Ast_to_c.ast_to_c) + else Ast_to_c.ast_to_c !debug) end