Add ways to declare unsafe functions + unsafe fix

compiler/global/signature.ml

@@ -39,6 +39,7 @@ type node = {
   node_inputs             : arg list;
   node_outputs            : arg list;
   node_stateful           : bool;
+  node_unsafe             : bool;
   node_params             : param list;
   node_param_constraints  : constrnt list;
   node_loc                : location}
@@ -136,10 +137,11 @@ let mk_field n ty = { f_name = n; f_type = ty }
 let mk_const_def ty value =
   { c_type = ty; c_value = value }
 
-let mk_node ?(constraints = []) loc ins outs stateful params =
+let mk_node ?(constraints = []) loc ins outs stateful unsafe params =
   { node_inputs = ins;
     node_outputs  = outs;
     node_stateful = stateful;
+    node_unsafe = unsafe;
     node_params = params;
     node_param_constraints = constraints;
     node_loc = loc}

compiler/heptagon/analysis/unsafe.ml

@@ -0,0 +1,64 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+(* Checks that a node not declared unsafe is safe, and set app unsafe flag. *)
+open Names
+open Location
+open Signature
+open Modules
+open Heptagon
+open Hept_mapfold
+
+type error =
+  | Eshould_be_unsafe
+
+let message loc kind =
+  begin match kind with
+    | Eshould_be_unsafe ->
+        Format.eprintf "%aThis exp is unsafe but the current node is not declared unsafe.@."
+          print_location loc
+  end;
+  raise Errors.Error
+
+(* Returns whether an op is unsafe *)
+let unsafe_op op = match op with
+  | Enode f | Efun f ->
+      (find_value f).node_unsafe
+  | _ -> (*TODO il y a des op unsafe ??*)
+      false
+
+(* Update app unsafe field
+   and gives an error if some exp is unsafe in a safe node ([unsafe]=false) *)
+let exp funs unsafe e =
+  let e, unsafe = Hept_mapfold.exp funs unsafe e in
+    match e.e_desc with
+      | Eapp({ a_op = op } as app, e_l, r) ->
+          let u = (unsafe_op op) or app.a_unsafe in
+          if u & (not unsafe)
+          then message e.e_loc Eshould_be_unsafe
+          else {e with e_desc = Eapp({ app with a_unsafe = u }, e_l, r)}, (unsafe or u)
+      | Eiterator(it, ({ a_op = op } as app), n, pe_list, e_list, r) ->
+          let u = (unsafe_op op) or app.a_unsafe in
+          if u & (not unsafe)
+          then message e.e_loc Eshould_be_unsafe
+          else
+            {e with e_desc = Eiterator(it, { app with a_unsafe = u }, n, pe_list, e_list, r)}
+            , (unsafe or u)
+      | _ -> e, unsafe
+
+(* unsafe nodes are rejected if they are not declared unsafe *)
+let node_dec funs _ n = Hept_mapfold.node_dec funs n.n_unsafe n
+
+let funs =
+  { Hept_mapfold.defaults with
+      exp = exp;
+      node_dec = node_dec; }
+
+let program p =
+  let p, _ = Hept_mapfold.program_it funs false p in
+  p

compiler/heptagon/hept_utils.ml

@@ -74,10 +74,11 @@ let mk_signature name ins outs stateful params constraints loc =
 
 let mk_node
     ?(input = []) ?(output = []) ?(contract = None)
-    ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
+    ?(stateful = true) ?(unsafe = false) ?(loc = no_location) ?(param = []) ?(constraints = [])
     name block =
   { n_name = name;
     n_stateful = stateful;
+    n_unsafe = unsafe;
     n_input = input;
     n_output = output;
     n_contract = contract;
@@ -112,6 +113,7 @@ let signature_of_node n =
     { node_inputs = args_of_var_decs n.n_input;
       node_outputs  = args_of_var_decs n.n_output;
       node_stateful = n.n_stateful;
+      node_unsafe = n.n_unsafe;
       node_params = n.n_params;
       node_param_constraints = n.n_param_constraints;
       node_loc = n.n_loc }

compiler/heptagon/heptagon.ml

@@ -150,6 +150,7 @@ type contract = {
 type node_dec = {
   n_name               : qualname;
   n_stateful           : bool;
+  n_unsafe             : bool;
   n_input              : var_dec list;
   n_output             : var_dec list;
   n_contract           : contract option;

compiler/heptagon/main/hept_compiler.ml

@@ -17,6 +17,7 @@ let pp p = if !verbose then Hept_printer.print stdout p
 let compile_program p =
   (* Typing *)
   let p = silent_pass "Statefulness check" true Stateful.program p in
+  let p = silent_pass "Unsafe check" true Unsafe.program p in
   let p = pass "Typing" true Typing.program p pp in
   let p = pass "Linear Typing" !do_linear_typing Linear_typing.program p pp in
 

compiler/heptagon/parsing/hept_lexer.mll

@@ -68,6 +68,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
  "init", INIT;
  "split", SPLIT;
  "reinit", REINIT;
+ "unsafe", UNSAFE;
  "quo", INFIX3("quo");
  "mod", INFIX3("mod");
  "land", INFIX3("land");

compiler/heptagon/parsing/hept_parser.mly

@@ -18,7 +18,7 @@ open Hept_parsetree
 %token <float> FLOAT
 %token <bool> BOOL
 %token <string * string> PRAGMA
-%token TYPE FUN NODE RETURNS VAR VAL OPEN END CONST
+%token TYPE FUN NODE RETURNS VAR VAL OPEN END CONST UNSAFE
 %token FBY PRE SWITCH EVERY
 %token OR STAR NOT
 %token AMPERSAND
@@ -170,11 +170,12 @@ returns: RETURNS | EQUAL {}
 ;
 
 node_dec:
-  | n=node_or_fun f=ident pc=node_params LPAREN i=in_params RPAREN
+  | u=unsafe n=node_or_fun f=ident pc=node_params LPAREN i=in_params RPAREN
     returns LPAREN o=out_params RPAREN
     c=contract b=block(LET) TEL
       {{ n_name = f;
          n_stateful = n;
+         n_unsafe = u;
          n_input  = i;
          n_output = o;
          n_contract = c;
@@ -655,14 +656,19 @@ interface:
     { { i_modname = ""; i_opened = o; i_desc = i } }
 ;
 
+unsafe:
+  | UNSAFE    { true }
+  | /*empty*/ { false }
+
 interface_desc:
   | type_dec         { Itypedef $1 }
   | const_dec        { Iconstdef $1 }
-  | VAL n=node_or_fun f=ident pc=node_params LPAREN i=params_signature RPAREN
+  | u=unsafe VAL n=node_or_fun f=ident pc=node_params LPAREN i=params_signature RPAREN
     returns LPAREN o=params_signature RPAREN
     { Isignature({ sig_name = f;
                    sig_inputs = i;
                    sig_stateful = n;
+                   sig_unsafe = u;
                    sig_outputs = o;
                    sig_params = fst pc;
                    sig_param_constraints = snd pc;

compiler/heptagon/parsing/hept_parsetree.ml

@@ -177,6 +177,7 @@ type contract =
 type node_dec =
   { n_name        : dec_name;
     n_stateful    : bool;
+    n_unsafe      : bool;
     n_input       : var_dec list;
     n_output      : var_dec list;
     n_contract    : contract option;
@@ -213,6 +214,7 @@ type signature =
   { sig_name        : dec_name;
     sig_inputs      : arg list;
     sig_stateful    : bool;
+    sig_unsafe      : bool;
     sig_outputs     : arg list;
     sig_params      : var_dec list;
     sig_param_constraints : exp list;

compiler/heptagon/parsing/hept_scoping.ml

@@ -200,15 +200,6 @@ let translate_iterator_type = function
   | Ifoldi -> Heptagon.Ifoldi
   | Imapfold -> Heptagon.Imapfold
 
-(** convention : static params are set as the first static args,
-    op<a1,a2> (a3) == op <a1> (a2,a3) == op (a1,a2,a3) *)
-let static_app_from_app app args=
-  match app.a_op with
-    | Efun (Q ({ qual = Pervasives } as q))
-    | Enode (Q ({ qual = Pervasives } as q)) ->
-        q, (app.a_params @ args)
-    | _ -> raise Not_static
-
 let rec translate_static_exp se =
   try
     let se_d = translate_static_exp_desc se.se_loc se.se_desc in
@@ -430,11 +421,10 @@ let translate_contract env opt_ct =
   | Some ct ->
       let env' = Rename.append env ct.c_controllables in
       let b, env = translate_block env ct.c_block in
-      Some
-	{ Heptagon.c_assume = translate_exp env ct.c_assume;
-	  Heptagon.c_enforce = translate_exp env ct.c_enforce;
-	  Heptagon.c_controllables = translate_vd_list env' ct.c_controllables;
-	  Heptagon.c_block = b }, env'
+      Some { Heptagon.c_assume = translate_exp env ct.c_assume;
+             Heptagon.c_enforce = translate_exp env ct.c_enforce;
+             Heptagon.c_controllables = translate_vd_list env' ct.c_controllables;
+             Heptagon.c_block = b }, env'
 
 let params_of_var_decs env p_l =
   let pofvd env vd =
@@ -476,6 +466,7 @@ let translate_node node =
   (* add the node signature to the environment *)
   let nnode = { Heptagon.n_name = n;
                Heptagon.n_stateful = node.n_stateful;
+               Heptagon.n_unsafe = node.n_unsafe;
                Heptagon.n_input = inputs;
                Heptagon.n_output = outputs;
                Heptagon.n_contract = contract;
@@ -555,7 +546,7 @@ let translate_signature s =
   let o = List.map translate_arg s.sig_outputs in
   let p, _ = params_of_var_decs Rename.empty s.sig_params in
   let c = List.map translate_constrnt s.sig_param_constraints in
-  let sig_node = Signature.mk_node s.sig_loc i o s.sig_stateful p in
+  let sig_node = Signature.mk_node s.sig_loc i o s.sig_stateful s.sig_unsafe p in
   Signature.check_signature sig_node;
   safe_add s.sig_loc add_value n sig_node;
   mk_signature n i o s.sig_stateful p c s.sig_loc

compiler/main/hept2mls.ml

@@ -90,9 +90,12 @@ let translate_app app =
 
 let rec translate_extvalue e =
   let mk_extvalue =
-    mk_extvalue
-      ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity ~ty:e.Heptagon.e_ty
-      ~clock:(match e.Heptagon.e_ct_annot with None -> fresh_clock () | Some ct -> assert_1 (unprod ct))
+    let clock = match e.Heptagon.e_ct_annot with
+      | None -> fresh_clock ()
+      | Some ct -> assert_1 (unprod ct)
+    in
+    mk_extvalue ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity
+                ~ty:e.Heptagon.e_ty ~clock:clock
   in
   match e.Heptagon.e_desc with
     | Heptagon.Econst c -> mk_extvalue (Wconst c)
@@ -156,11 +159,15 @@ let rec translate_pat = function
   | Heptagon.Evarpat(n) -> Evarpat n
   | Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
 
-let rec translate_eq
-    { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
+let rec translate_eq { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
   match desc with
     | Heptagon.Eeq(p, e) ->
-        mk_equation ~loc:loc (translate_pat p) (translate e)
+        begin match e.Heptagon.e_desc with
+          | Heptagon.Eapp({ Heptagon.a_unsafe = unsafe },_,_)
+          | Heptagon.Eiterator(_,{ Heptagon.a_unsafe = unsafe},_,_,_,_) ->
+              mk_equation ~loc:loc unsafe (translate_pat p) (translate e)
+          | _ -> mk_equation ~loc:loc false (translate_pat p) (translate e)
+        end
     | Heptagon.Eblock _ | Heptagon.Eswitch _
     | Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
         Error.message loc Error.Eunsupported_language_construct

compiler/minils/analysis/interference.ml

@@ -484,10 +484,10 @@ let process_eq ({ eq_lhs = pat; eq_rhs = e } as eq) =
     (resp at the bottom and top) *)
 let add_init_return_eq f =
    (** a_1,..,a_p = __init__  *)
-  let eq_init = mk_equation (Mls_utils.pat_from_dec_list f.n_input)
+  let eq_init = mk_equation false (Mls_utils.pat_from_dec_list f.n_input)
     (mk_extvalue_exp Cbase Initial.tint Ltop (Wconst (Initial.mk_static_int 0))) in
     (** __return__ = o_1,..,o_q *)
-  let eq_return = mk_equation (Etuplepat [])
+  let eq_return = mk_equation false (Etuplepat [])
     (mk_exp Cbase Tinvalid Ltop (Mls_utils.tuple_from_dec_list f.n_output)) in
     (eq_init::f.n_equs)@[eq_return]
 

compiler/minils/minils.ml

@@ -106,36 +106,37 @@ type pat =
   | Evarpat of var_ident
 
 type eq = {
-  eq_lhs : pat;
-  eq_rhs : exp;
-  eq_loc : location }
+  eq_lhs    : pat;
+  eq_rhs    : exp;
+  eq_unsafe : bool;
+  eq_loc    : location }
 
 type var_dec = {
-  v_ident : var_ident;
-  v_type : ty;
+  v_ident     : var_ident;
+  v_type      : ty;
   v_linearity : linearity;
-  v_clock : ck;
-  v_loc : location }
+  v_clock     : ck;
+  v_loc       : location }
 
 type contract = {
-  c_assume : extvalue;
-  c_enforce : extvalue;
+  c_assume        : extvalue;
+  c_enforce       : extvalue;
   c_controllables : var_dec list;
-  c_local : var_dec list;
-  c_eq : eq list }
+  c_local         : var_dec list;
+  c_eq            : eq list }
 
 type node_dec = {
-  n_name   : qualname;
+  n_name     : qualname;
   n_stateful : bool;
-  n_input  : var_dec list;
-  n_output : var_dec list;
+  n_input    : var_dec list;
+  n_output   : var_dec list;
   n_contract : contract option;
   (* GD: inglorious hack for controller call *)
   mutable n_controller_call : string list * string list;
-  n_local  : var_dec list;
-  n_equs   : eq list;
-  n_loc    : location;
-  n_params : param list;
+  n_local    : var_dec list;
+  n_equs     : eq list;
+  n_loc      : location;
+  n_params   : param list;
   n_param_constraints : constrnt list;
   n_mem_alloc : (ty * Interference_graph.ivar list) list; }
 
@@ -195,8 +196,8 @@ let mk_extvalue_exp ?(clock = fresh_clock())
   mk_exp ~ck:clock ~loc:loc level_ck ty ~linearity:linearity
     (Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc))
 
-let mk_equation ?(loc = no_location) pat exp =
-  { eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
+let mk_equation ?(loc = no_location) unsafe pat exp =
+  { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_loc = loc }
 
 let mk_node
     ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[]))

compiler/minils/mls_utils.ml

@@ -233,7 +233,9 @@ let remove_eqs_from_node nd ids =
   let walk_vd vd vd_list = if IdentSet.mem vd.v_ident ids then vd_list else vd :: vd_list in
   let walk_eq eq eq_list =
     let defs = ident_list_of_pat eq.eq_lhs in
-    if List.for_all (fun v -> IdentSet.mem v ids) defs then eq_list else eq :: eq_list
+    if (not eq.eq_unsafe) & List.for_all (fun v -> IdentSet.mem v ids) defs
+    then eq_list
+    else eq :: eq_list
   in
   let vd_list = List.fold_right walk_vd nd.n_local [] in
   let eq_list = List.fold_right walk_eq nd.n_equs [] in

compiler/minils/transformations/tomato.ml

@@ -356,7 +356,7 @@ let rec reconstruct ((tenv, cenv) as env) mapping =
 
     let pat = reconstruct_pattern mapping repr.er_pattern in
 
-    mk_equation pat e :: eq_list in
+    mk_equation false pat e :: eq_list in
   IntMap.fold reconstruct_class cenv []
 
 and reconstruct_exp_desc mapping headd children =
@@ -555,7 +555,7 @@ let rec fix_output_var_dec mapping vd (seen, equs, vd_list) =
     let new_vd = { vd with v_ident = new_id; v_clock = new_clock } in
     let new_eq =
       let w = mk_extvalue ~ty:vd.v_type ~clock:new_clock ~linearity:Linearity.Ltop (Wvar x) in
-      mk_equation
+      mk_equation false
         (Evarpat new_id)
         (mk_exp new_clock vd.v_type ~ct:(Ck new_clock)
            ~ck:new_clock ~linearity:Linearity.Ltop (Eextvalue w))