From 657fe7e6fae3af61899547b55b262e5dcc3cf3b7 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Tue, 20 Dec 2022 03:48:37 +0100 Subject: [PATCH] Add support for `reset`s --- src/cast.ml | 1 + src/cprint.ml | 8 +++ src/ctranslation.ml | 3 +- src/main.ml | 5 +- src/passes.ml | 140 ++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 155 insertions(+), 2 deletions(-) diff --git a/src/cast.ml b/src/cast.ml index 81b0672..d2ead4f 100644 --- a/src/cast.ml +++ b/src/cast.ml @@ -14,6 +14,7 @@ and c_expression = | CSeq of c_expression * c_expression | CIf of c_value * c_block * c_block | CApplication of ident * int * c_var list * c_var list * node_states + | CReset of ident * int * c_value * c_block (** A value here is anything that can be inlined into a single C expression * containing no function call, condition, ... *) diff --git a/src/cprint.ml b/src/cprint.ml index 484f2ca..759c1c2 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -189,6 +189,14 @@ and cp_expression fmt (expr, hloc) = | CVInput _ -> failwith "Impossible!") 0 destl in () end + | CReset (node_name, i, v, b) -> + begin + Format.fprintf fmt "\tif (%a) {\n\t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\t}\n%a\n" + cp_value (v, hloc) + node_name + (i - 1) + cp_block (b, hloc) + end | CIf (v, b1, []) -> let p = prefix in prefix_ := prefix^"\t"; diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 9113c5b..6a2e3d5 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -81,7 +81,8 @@ let rec equation_to_expression (node_st, node_sts, (vl, expr)) = CIf (iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, e))], [equation_to_expression (node_st, node_sts, (vl, e'))]) - | IEReset _ -> failwith "A pass should have removed resets." + | IEReset (IEApp (i, node, b), c) -> CReset (node.n_name, i, iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, IEApp (i, node, b)))]) + | IEReset _ -> failwith "A pass should have turned not function resets into function resets" diff --git a/src/main.ml b/src/main.ml index da6fed1..7699020 100644 --- a/src/main.ml +++ b/src/main.ml @@ -44,8 +44,9 @@ let exec_passes ast verbose debug passes f = let _ = (** Usage and argument parsing. *) let default_passes = - ["remove_if"; + ["linearization_reset"; "remove_if"; "linearization_pre"; "linearization_tuples"; "linearization_app"; + "ensure_assign_val"; "equations_ordering"] in let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in let usage_msg = @@ -87,6 +88,8 @@ let _ = ("linearization_tuples", Passes.pass_linearization_tuples); ("linearization_app", Passes.pass_linearization_app); ("linearization_pre", Passes.pass_linearization_pre); + ("ensure_assign_val", Passes.pass_ensure_assignment_value); + ("linearization_reset", Passes.pass_linearization_reset); ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity); ("automata_translation", Passes.automata_translation_pass); ("automata_validity", Passes.check_automata_validity); diff --git a/src/passes.ml b/src/passes.ml index c409846..669c0ac 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -147,6 +147,73 @@ let pass_if_removal verbose debug = node_pass aux_if_removal +(** [pass_linearization_reset] makes sure that all reset constructs in the program + * are applied to functions. + * This is required, since the reset construct is translated into resetting the + * function state in the final C code. *) +let pass_linearization_reset verbose debug = + (** [node_lin] linearizes a single node. *) + let node_lin (node: t_node): t_node option = + (** [reset_aux_expression] takes an expression and returns: + * - a list of additional equations + * - the new list of local variables + * - an updated version of the original expression *) + let rec reset_aux_expression vars expr: t_eqlist * t_varlist * t_expression = + match expr with + | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + let eqs'', vars, e'' = reset_aux_expression vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = reset_aux_expression vars e in + let eqs', vars, e' = reset_aux_expression vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + ( + match e with + | EApp (t_app, n_app, e_app) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EReset (t, e, e') + | e -> reset_aux_expression vars e + ) + | EConst _ -> [], vars, expr + | ETuple (t, l) -> + let eqs, vars, l = List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = reset_aux_expression vars e in + eqs' @ eqs, vars, (e :: l)) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = reset_aux_expression vars e in + eqs, vars, EApp (t, n, e) + in + (** Applies the previous function to the expressions of every equation. *) + let new_equations, new_locvars = + List.fold_left + (fun (eqs, vars) (patt, expr) -> + let eqs', vars, expr = reset_aux_expression vars expr in + (patt, expr)::eqs' @ eqs, vars) + ([], node.n_local_vars) + node.n_equations + in + Some { node with n_local_vars = new_locvars; n_equations = new_equations } + in + node_pass node_lin + (** [pass_linearization_pre] makes sure that all pre constructs in the program * are applied to variables. @@ -391,6 +458,79 @@ let pass_linearization_app verbose debug = +let pass_ensure_assignment_value verbose debug = + let varcount = ref 0 in + let rec aux_expr should_be_value vars expr = + match expr with + | EConst _ | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + let eqs, vars, e = aux_expr true vars e in + eqs, vars, EMonOp (t, op, e) + | EBinOp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + let eqs'', vars, e'' = aux_expr should_be_value vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = aux_expr true vars e in + let eqs', vars, e' = aux_expr true vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = aux_expr should_be_value vars e in + let eqs', vars, e' = aux_expr should_be_value vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | ETuple (t, l) -> + let eqs, vars, l = + List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = aux_expr true vars e in + eqs' @ eqs, vars, e :: l) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = aux_expr true vars e in + if should_be_value + then + let nvar = Format.sprintf "_assignval%d" !varcount in + incr varcount; + let nvar: t_var = + match t with + | [TBool] -> BVar nvar + | [TReal] -> RVar nvar + | [TInt] -> IVar nvar + | _ -> + failwith "An application occurring here should return a single element." + in + let neq_patt: t_varlist = (t, [nvar]) in + let neq_expr: t_expression = EApp (t, n, e) in + let vars = varlist_concat neq_patt vars in + (neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar) + else + eqs, vars, EApp (t, n, e) + in + let aux_ensure_assign_val node = + let new_equations, vars = + List.fold_left + (fun (eqs, vars) eq -> + let eqs', vars, expr = aux_expr false vars (snd eq) in + (fst eq, expr) :: eqs' @ eqs, vars + ) + ([], node.n_local_vars) node.n_equations + in + Some { node with n_equations = new_equations; n_local_vars = vars } + in + node_pass aux_ensure_assign_val + + + (** [sanity_pass_assignment_unicity] makes sure that there is at most one * equation defining each variable (and that no equation tries to redefine an * input).