Add support for resets

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, ... *)

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";

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"
 
 
 

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);

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).