working version for stateful contracts

.ocamlformat

-version=0.18.0
+version=0.19.0
 parens-tuple=multi-line-only
 wrap-comments=true
 cases-exp-indent=2

src/automata.ml

@@ -88,7 +88,8 @@ let unless_read reads handler =
   (* Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list
      ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
      Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list
-     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); *)
+     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements
+     res); *)
   res
 
 let until_read reads handler =
@@ -381,7 +382,7 @@ let node_of_assign_until nused used node aut_id aut_state handler =
       node_gencalls = [];
       node_checks = [];
       node_asserts = handler.hand_asserts;
-      node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
+      node_stmts = (until_eq :: new_output_eqs) @ handler.hand_stmts;
       node_dec_stateless = false;
       node_stateless = None;
       node_spec = None;
@@ -544,7 +545,7 @@ let rec expand_decls_rec nused top_decls =
           top_decl.top_decl_owner
           nd
       in
-      top_types' @ top_decl' :: expand_decls_rec nused (top_nodes' @ q)
+      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes' @ q))
     | _ ->
       top_decl :: expand_decls_rec nused q)
 

src/backends/Ada/ada_backend_wrapper.ml

@@ -111,10 +111,9 @@ let pp_main_adb fmt machine =
   let pp_loop fmt =
     let args =
       pp_state_name
-      ::
-      List.map
-        pp_var_name
-        (machine.mstep.step_inputs @ machine.mstep.step_outputs)
+      :: List.map
+           pp_var_name
+           (machine.mstep.step_inputs @ machine.mstep.step_outputs)
     in
     fprintf
       fmt

src/backends/C/c_backend_cmake.ml

@@ -53,12 +53,11 @@ let fprintf_dependencies fmt (dep : dep_t list) =
       (* Format.eprintf "Adding dependency: %s@." s; *)
       fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
     ("${INC}/io_frontend.c"
-     ::
-     (* IO functions when a main function is computed *)
-     List.map
-       (fun (Dep (local, s, _, _)) ->
-         (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
-       compiled_dep)
+    :: (* IO functions when a main function is computed *)
+       List.map
+         (fun (Dep (local, s, _, _)) ->
+           (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
+         compiled_dep)
 
 module type MODIFIERS_MKF = sig
   (* dep was (bool * ident * top_decl list) *)

src/backends/C/c_backend_common.ml

@@ -276,7 +276,8 @@ let pp_basic_c_type ?(pp_c_basic_type_desc = pp_c_basic_type_desc) ?var_opt fmt
   | _ ->
     fprintf fmt "%s" (pp_c_basic_type_desc t)
 
-let pp_c_type ?(var_is_contract=false) ?pp_c_basic_type_desc ?var_opt var_id fmt t =
+let pp_c_type ?(var_is_contract = false) ?pp_c_basic_type_desc ?var_opt var_id
+    fmt t =
   let rec aux t pp_suffix =
     if is_basic_c_type t then
       fprintf
@@ -439,7 +440,12 @@ let pp_c_decl_input_var fmt id =
    the case for generics *)
 let pp_c_decl_output_var fmt id =
   if (not !Options.ansi) && Types.is_address_type id.var_type then
-    pp_c_type ~var_is_contract:id.var_is_contract ~var_opt:id id.var_id fmt id.var_type
+    pp_c_type
+      ~var_is_contract:id.var_is_contract
+      ~var_opt:id
+      id.var_id
+      fmt
+      id.var_type
   else
     pp_c_type
       ~var_is_contract:id.var_is_contract
@@ -937,9 +943,7 @@ module Protos (Mod : MODIFIERS_GHOST_PROTO) = struct
       name
       (pp_comma_list pp_c_decl_input_var)
       inputs
-      (pp_comma_list
-         ~pp_prologue:pp_print_comma
-         pp_c_decl_output_var)
+      (pp_comma_list ~pp_prologue:pp_print_comma pp_c_decl_output_var)
       outputs
 end
 

src/backends/C/c_backend_header.ml

@@ -72,7 +72,8 @@ functor
        a predicate: function step and reset are associated to ACSL predicate -
        the node is associated to a refinement contract, wrt its ACSL sem - if
        the node is a regular node associated to a contract, print the contract
-       as function contract. - do not print anything if this is a contract node *)
+       as function contract. - do not print anything if this is a contract
+       node *)
     let pp_machine_alloc_decl fmt m =
       Mod.pp_machine_decl_prefix fmt m;
       if not (fst (get_stateless_status m)) then
@@ -125,7 +126,8 @@ functor
             fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
           else (
             (* TODO: raise proper error *)
-            Format.eprintf "internal error: pp_machine_decl_top_decl_from_header";
+            Format.eprintf
+              "internal error: pp_machine_decl_top_decl_from_header";
             assert false)
         else if inode.nodei_stateless then
           fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype

src/backends/C/c_backend_main.ml

@@ -481,7 +481,8 @@ module Main (Mod : MODIFIERS_MAINSRC) = struct
         content = [];
         is_stateful = true (* assuming it is stateful*);
       }
-      (* Print the svn version number and the supported C standard (C90 or C99) *)
+      (* Print the svn version number and the supported C standard (C90 or
+         C99) *)
       pp_print_version
       ()
       (pp_main_code machines)

src/backends/C/c_backend_makefile.ml

@@ -63,13 +63,13 @@ let fprintf_dependencies fmt (deps : dep_t list) =
       Log.report ~level:1 (fun fmt -> fprintf fmt "Adding dependency: %s@." s);
       fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
     ("${INC}/io_frontend.c"
-     ::
-     (* IO functions when a main function is computed *)
-     List.map
-       (fun dep ->
-         (if dep.local then dep.name else Version.include_path ^ "/" ^ dep.name)
-         ^ ".c")
-       compiled_deps)
+    :: (* IO functions when a main function is computed *)
+       List.map
+         (fun dep ->
+           (if dep.local then dep.name
+           else Version.include_path ^ "/" ^ dep.name)
+           ^ ".c")
+         compiled_deps)
 
 module type MODIFIERS_MKF = sig
   (* dep was (bool * ident * top_decl list) *)

src/backends/C/c_backend_src.ml

@@ -35,7 +35,8 @@ module type MODIFIERS_SRC = sig
 
   val pp_ghost_parameter : ident -> formatter -> ident option -> unit
 
-  val pp_contract : formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+  val pp_contract :
+    formatter -> machine_t list -> ident -> ident -> machine_t -> unit
 end
 
 module EmptyMod = struct
@@ -323,12 +324,12 @@ module Main (Mod : MODIFIERS_SRC) = struct
           i
           (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m)))
           vl
-      | MStep (il, i, vl) ->
-        begin match List.assoc_opt i m.minstances with
-          | Some (td, _) when Arrow.td_is_arrow td ->
-            pp_arrow_call m self mem fmt i il
-          | _ -> pp_basic_instance_call m self mem fmt i vl il
-        end
+      | MStep (il, i, vl) -> (
+        match List.assoc_opt i m.minstances with
+        | Some (td, _) when Arrow.td_is_arrow td ->
+          pp_arrow_call m self mem fmt i il
+        | _ ->
+          pp_basic_instance_call m self mem fmt i vl il)
       | MBranch (_, []) ->
         eprintf
           "internal error: C_backend_src.pp_machine_instr %a@."
@@ -544,9 +545,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
       check
 
   let pp_print_function ~pp_prototype ~prototype ?(is_contract = false)
-      ?(pp_spec = pp_print_nothing)
-      ?(pp_local = pp_print_nothing) ?(base_locals = [])
-      ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
+      ?(pp_spec = pp_print_nothing) ?(pp_local = pp_print_nothing)
+      ?(base_locals = []) ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
       ?(pp_init_mpfr_local = pp_print_nothing)
       ?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = [])
       ?(pp_check = pp_print_nothing) ?(checks = [])
@@ -1004,7 +1004,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
         content = [];
         is_stateful = true (* assuming it is stateful *);
       }
-      (* Print the svn version number and the supported C standard (C90 or C99) *)
+      (* Print the svn version number and the supported C standard (C90 or
+         C99) *)
       pp_print_version
       ()
       (* Print dependencies *)

src/backends/C/c_backend_src.mli

@@ -21,7 +21,8 @@ module type MODIFIERS_SRC = sig
 
   val pp_ghost_parameter : ident -> formatter -> ident option -> unit
 
-  val pp_contract : formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+  val pp_contract :
+    formatter -> machine_t list -> ident -> ident -> machine_t -> unit
 end
 
 module EmptyMod : MODIFIERS_SRC

src/backends/Horn/horn_backend_printers.ml

@@ -387,7 +387,8 @@ let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr :
        other did. Am I clear ? *)
     (* For each branch we obtain the logical encoding, and the information
        whether a sub node has been reset or not. If a node has been reset in one
-       of the branch, then all others have to have the mem_m = mem_c statement. *)
+       of the branch, then all others have to have the mem_m = mem_c
+       statement. *)
     let self = m.mname.node_id in
     let pp_branch fmt (tag, instrs) =
       fprintf

src/backends/Horn/horn_backend_traces.ml

@@ -53,7 +53,8 @@ let machines_traces machines =
         let filtered =
           List.filter (fun (kwds, _) -> kwds = [ "traceability" ]) all_annots
         in
-        (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot) (m.mannot); *)
+        (* List.iter (eprintf "Annots: %a@." Printers.pp_expr_annot)
+           (m.mannot); *)
         let content = List.map snd filtered in
         (* Elements are supposed to be a pair (tuple): variable, expression *)
         List.map

src/backends/backends.ml

@@ -5,7 +5,8 @@ let setup () =
   if !Options.output = Options.OutEMF then (
     (* Not merging branches *)
     join_guards := false;
-    (* In case of a default "int" type, substitute it with the legal int32 value *)
+    (* In case of a default "int" type, substitute it with the legal int32
+       value *)
     if !Options.int_type = "int" then Options.int_type := "int32");
   if !Options.optimization < 0 then join_guards := false
 

src/causality.ml

@@ -206,7 +206,8 @@ module ExprDep = struct
   (* mem/mem in g'                                *)
   (* match (lhs_is_mem, ISet.mem x mems) with | (false, true ) -> (add_edges [x]
      lhs g, g') | (false, false) -> (add_edges lhs [x] g, g') | (true , false)
-     -> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs g') *)
+     -> (add_edges lhs [x] g, g') | (true , true ) -> (g, add_edges [x] lhs
+     g') *)
   let add_eq_dependencies mems inputs node_vars eq (g, g') =
     let add_var lhs_is_mem lhs x (g, g') =
       if is_instance_var x || ISet.mem x node_vars then
@@ -590,7 +591,8 @@ module CycleDetection = struct
 
   (* Breaks cycles of the dependency graph [g] of memory variables [mems]
      belonging in node [node]. Returns: - a list of new auxiliary variable
-     declarations - a list of new equations - a modified acyclic version of [g] *)
+     declarations - a list of new equations - a modified acyclic version of
+     [g] *)
   let break_cycles node mems g =
     let eqs, auts = get_node_eqs node in
     assert (auts = []);

src/checks/algebraicLoop.ml

@@ -327,7 +327,8 @@ let clean_al prog : program_t * bool * report =
         | Node nd -> (
           let error, max_inlines =
             try
-              (* without exception the node is schedulable; nothing to declare *)
+              (* without exception the node is schedulable; nothing to
+                 declare *)
               let _ = Scheduling.schedule_node nd in
               None, max_inlines
             with Causality.Error (Causality.DataCycle partitions) ->

src/checks/liveness.ml

@@ -48,7 +48,8 @@ let pp_fanin fmt fanin =
   Hashtbl.iter (fun s t -> Format.fprintf fmt "@ %s -> %d" s t) fanin;
   Format.fprintf fmt "@]@ }@]"
 
-(* computes the cone of influence of a given [var] wrt a dependency graph [g]. *)
+(* computes the cone of influence of a given [var] wrt a dependency graph
+   [g]. *)
 let cone_of_influence g var =
   (*Format.printf "DEBUG coi: %s@." var;*)
   let frontier = ref (ISet.add var ISet.empty) in

src/checks/stateless.ml

@@ -62,8 +62,7 @@ let rec check_expr expr =
             i);
     check_expr e' && reset_opt && stateless_node
 
-and check_eexpr e =
-  check_expr e.eexpr_qfexpr
+and check_eexpr e = check_expr e.eexpr_qfexpr
 
 and compute_node nd =
   (* returns true iff the node is stateless.*)
@@ -76,18 +75,14 @@ and compute_contract nd =
   let c = node_as_contract nd in
   let eqs, aut = get_contract_eqs c in
   aut = []
-  && (* A node containinig an automaton will be stateful *)
-  List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
-  &&
-  List.for_all check_eexpr c.assume
-  &&
-  List.for_all check_eexpr c.guarantees
+  (* A node containinig an automaton will be stateful *)
+  && List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
+  && List.for_all check_eexpr c.assume
+  && List.for_all check_eexpr c.guarantees
 
 and compute_node_or_contract nd =
   match nd.node_spec, nd.node_iscontract with
-  | None, false
-  | Some (NodeSpec _), false
-  | Some (Contract _), false ->
+  | None, false | Some (NodeSpec _), false | Some (Contract _), false ->
     compute_node nd
   | Some (Contract _), true ->
     compute_contract nd
@@ -96,23 +91,22 @@ and compute_node_or_contract nd =
 
 and check_node td =
   match td.top_decl_desc with
-  | Node nd ->
-    begin match nd.node_stateless with
-      | None ->
-        let stateless = compute_node_or_contract nd in
-        nd.node_stateless <- Some stateless;
-        if stateless
-        then (if not nd.node_dec_stateless
-              then Log.report ~level:2 (fun fmt ->
-                  Format.fprintf fmt "%s: node -> function@;" nd.node_id))
-        else if nd.node_dec_stateless
-        then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id));
-        nd.node_dec_stateless <- stateless;
-        stateless
-      | Some stl ->
-        stl
-    end
-| ImportedNode nd ->
+  | Node nd -> (
+    match nd.node_stateless with
+    | None ->
+      let stateless = compute_node_or_contract nd in
+      nd.node_stateless <- Some stateless;
+      if stateless then (
+        if not nd.node_dec_stateless then
+          Log.report ~level:2 (fun fmt ->
+              Format.fprintf fmt "%s: node -> function@;" nd.node_id))
+      else if nd.node_dec_stateless then
+        raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id));
+      nd.node_dec_stateless <- stateless;
+      stateless
+    | Some stl ->
+      stl)
+  | ImportedNode nd ->
     if nd.nodei_prototype = Some "C" && not nd.nodei_stateless then
       raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id));
     nd.nodei_stateless

src/clocks.ml

@@ -38,7 +38,8 @@ and carrier_expr = {
 
 type t = { mutable cdesc : clock_desc; mutable cscoped : bool; cid : int }
 
-(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
+(* pck stands for periodic clock. Easier not to separate pck from other
+   clocks *)
 and clock_desc =
   | Carrow of t * t
   | Ctuple of t list
@@ -205,8 +206,10 @@ let split_arrow ck =
 
 (** Returns the clock corresponding to a clock list. *)
 let clock_of_clock_list = function
-  | [ck] -> ck
-  | ckl -> new_ck (Ctuple ckl) true
+  | [ ck ] ->
+    ck
+  | ckl ->
+    new_ck (Ctuple ckl) true
 
 let clock_list_of_clock ck =
   match (repr ck).cdesc with Ctuple cl -> cl | _ -> [ ck ]

src/clocks.mli

@@ -17,7 +17,8 @@ and carrier_expr = {
 
 type t = { mutable cdesc : clock_desc; mutable cscoped : bool; cid : int }
 
-(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
+(* pck stands for periodic clock. Easier not to separate pck from other
+   clocks *)
 and clock_desc =
   | Carrow of t * t
   | Ctuple of t list