Added option -nosink (CS optimisation)

The -nosink option suppress the sink state of sigali equations.

This optimizes the controller synthesis, but work only
when the synthesis objective instantaneoulsy depends only
on the current state (and not on current inputs).

compiler/main/heptc.ml

@@ -148,6 +148,7 @@ let main () =
         "-fname", Arg.Set full_name, doc_full_name;
         "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion;
         "-strict_ssa", Arg.Unit set_strict_ssa, doc_strict_ssa;
+	"-nosink", Arg.Set nosink, doc_nosink;
         "-memalloc", Arg.Unit do_mem_alloc_and_typing, doc_memalloc;
         "-only-memalloc", Arg.Set do_mem_alloc, doc_memalloc_only;
         "-only-linear", Arg.Set do_linear_typing, doc_linear_only;

compiler/minils/sigali/sigalimain.ml

@@ -402,19 +402,26 @@ let translate_node
       (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
       (sig_inputs@sig_ctrl) in
   let constraints = constraints @ [Sequal (a_c,Sconst(Ctrue))] in
-  (* Sink state when the guarantee part of the contract becomes false *)
-  (* f_error_state state variable initialized to true; become false
-     the instant after the guarantee part is false *)
-  let error_state_name = f ^ "_error_state" in
-  let sig_states_full = sig_states @ [error_state_name] in
-  let body_sink =
-    [(extend
-        initialisations
-        (Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
-     (extend
-        evolutions
-        (Slist[g_c]))] in
-  let obj = Security(Svar(error_state_name)) in
+  let body_sink, sig_states_full, obj_exp =
+    if !Compiler_options.nosink then
+      ([], sig_states, g_c)
+    else
+      begin
+	(* Sink state when the guarantee part of the contract becomes false *)
+	(* f_error_state state variable initialized to true; become false
+	   the instant after the guarantee part is false *)
+	let error_state_name = f ^ "_error_state" in
+	let sig_states_full = sig_states @ [error_state_name] in
+	let body_sink =
+	  [(extend
+              initialisations
+              (Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
+	   (extend
+              evolutions
+              (Slist[g_c]))] in
+	(body_sink, sig_states_full, Svar(error_state_name))
+      end in
+  let obj = Security(obj_exp) in
   let p = { proc_dep = [];
             proc_name = f;
             proc_inputs = sig_inputs@sig_ctrl;

compiler/utilities/global/compiler_options.ml

@@ -85,6 +85,8 @@ let create_object_file = ref false
 
 let boolean = ref false
 
+let nosink = ref false
+
 (* Target languages list for code generation *)
 let target_languages : string list ref = ref []
 
@@ -190,6 +192,7 @@ and doc_target_path =
   "<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is"
   ^ " cleaned)"
 and doc_boolean = "\t\tTranslate enumerated values towards boolean vectors"
+and doc_nosink = "\t\tSuppress the sink state in sigali equations"
 and doc_deadcode = "\t\tDeadcode removal"
 and doc_nocaus = "\t\tDisable causality analysis"
 and doc_noinit = "\t\tDisable initialization analysis"