New option to force abstraction of infinite-domain state variables in ctrln export

Also add an option to silence related warnings

compiler/main/heptc.ml

@@ -157,8 +157,11 @@ let main () =
         "-O", Arg.Unit do_optim, doc_optim;
         "-mall", Arg.Set interf_all, doc_interf_all;
         "-time", Arg.Set time_passes, doc_time_passes;
+        "-abstract-infinite", Arg.Set abstract_infinite, doc_abstract_infinite;
         ("-Wno-untranslatable", Arg.Clear warn_untranslatable,
          doc_no_warn_untranslat);
+        ("-Wno-abstract", Arg.Clear warn_abstractions,
+         doc_no_warn_abstractions);
       ]
         compile errmsg;
   with

compiler/minils/ctrln/ctrlNbacGen.ml

@@ -119,6 +119,14 @@ let rec translate_typ typ = match Modules.unalias_type typ with
   | Tarray _ -> raise & Untranslatable ("array type")
   | Tinvalid -> failwith "Encountered an invalid type!"
 
+let rec fintypp typ = match Modules.unalias_type typ with
+  | Tid ({ qual = Pervasives; name = "bool" }) -> true
+  | Tid t -> (match Modules.find_type t with
+      | Tenum _ -> true
+      | Talias t -> fintypp t                                          (* XXX? *)
+      | _ -> false)
+  | _ -> false
+
 let ref_of_ty ty = match translate_typ ty with
   | `Bool -> mk_bref
   | `Enum _ -> mk_eref
@@ -326,18 +334,25 @@ let translate_abstract_app ~pref gd pat _f args =
     if SSet.is_empty depc then gd else close_uc_group gd depc
   in
   (* declare extra inputs. *)
-  (List.fold_left (declare_additional_input ~pref) gd results, [])
+  List.fold_left (declare_additional_input ~pref) gd results
 
 (* --- *)
 
+
 let translate_eq ~pref (gd, equs)
     ({ eq_lhs = pat;
        eq_rhs = { e_desc = exp; e_ty = ty } as rhs;
        eq_base_ck = clk } as eq)
     =
+  let abstract_infinite_state = !Compiler_options.abstract_infinite in
   match pat with
     | Evarpat id ->
         begin match exp with
+          | Efby _ when (abstract_infinite_state && not (fintypp ty)) ->
+              warn ~cond:(!Compiler_options.warn_abstractions)
+                "Abstracting@ %a@ state@ variable@ %s@ as@ non-controllable@ \
+                 input." Global_printer.print_type ty (name id);
+              (declare_additional_input ~pref gd id, eq :: equs)
           | Efby (init, ev) ->
               let v = pref & mk_symb & name id in
               let ev = translate_ext ~pref ev in
@@ -345,21 +360,19 @@ let translate_eq ~pref (gd, equs)
               (add_state_var ~pref gd id ty ev init, eq :: equs)
           | Eapp ({ a_op = (Enode f | Efun f) }, args, None)
                 when f.qual <> Pervasives ->
-              let gd, equs' = translate_abstract_app ~pref gd pat f args in
-              (gd, eq :: equs' @ equs)
+              (translate_abstract_app ~pref gd pat f args, eq :: equs)
           | _ when IdentSet.mem id gd.output ->
-              (add_output_var ~pref gd id ty (translate_exp ~pref rhs),
-               eq :: equs)
+              let exp = translate_exp ~pref rhs in
+              (add_output_var ~pref gd id ty exp, eq :: equs)
           | _ ->
-              (add_local_var ~pref gd id ty (translate_exp ~pref rhs),
-               eq :: equs)
+              let exp = translate_exp ~pref rhs in
+              (add_local_var ~pref gd id ty exp, eq :: equs)
         end
     | Etuplepat _ ->
         begin match exp with
           | Eapp ({ a_op = (Enode f | Efun f) }, args, None)
                 when f.qual <> Pervasives ->
-              let gd, equs' = translate_abstract_app ~pref gd pat f args in
-              (gd, eq :: equs' @ equs)
+              (translate_abstract_app ~pref gd pat f args, eq :: equs)
           | _ -> failwith "TODO: Minils.Etuplepat construct!"
         end
 

compiler/minils/sigali/sigalimain.ml

@@ -280,7 +280,8 @@ let translate_eq f
       | _ ->
           untranslatable_warn e;
           (* Mark n as input: unusable as local variable *)
-	  Format.printf "Adding non-bool variable %s in current_inputs@\n" (name n);
+	  warn ~cond:(!Compiler_options.warn_abstractions)
+            "Adding non-bool variable %s in current_inputs@\n" (name n);
           current_inputs := IdentSet.add n !current_inputs;
           acc_states,acc_init,acc_inputs,acc_eqs
       end

compiler/utilities/global/compiler_options.ml

@@ -163,6 +163,8 @@ let do_optim () =
   deadcode := true
 
 let warn_untranslatable = ref true                             (* z3z | ctrln *)
+let abstract_infinite = ref false                                    (* ctrln *)
+let warn_abstractions = ref true                                     (* ctrln *)
 
 let check_options () =
   let err m = raise (Arg.Bad m) in
@@ -189,7 +191,7 @@ and doc_no_pervasives = "\tDo not load the pervasives module"
 and doc_flatten = "\t\tInline everything."
 and doc_target =
   "<lang>\tGenerate code in language <lang>\n\t\t\t(with <lang>=c,"
-  ^ " java or z3z)"
+  ^ " java, z3z or ctrln)"
 and doc_full_type_info = "\t\t\tPrint full type information"
 and doc_stateful_info = "\t\tPrint stateful information"
 and doc_full_name = "\t\tPrint full variable name information"
@@ -215,4 +217,6 @@ and doc_optim = "\t\t\tOptimize with deadcode, tomato, itfusion and memalloc"
 and doc_interf_all = "\t\tPerform memory allocation on all types"
 and doc_unroll = "\t\tUnroll all loops"
 and doc_time_passes = "\t\tTime compilation passes"
+and doc_abstract_infinite = "\tAbstract infinite state (implied for z3z target)"
 and doc_no_warn_untranslat = "\tSuppress warnings about untranslatable constructs"
+and doc_no_warn_abstractions = "\tSuppress abstraction warnings"