Correct handling of local assume/enforce of contracts

compiler/heptagon/analysis/hept_clocking.ml

@@ -77,7 +77,13 @@ let error_message loc = function
 let ck_of_name h x =
   if is_reset x
   then fresh_clock()
-  else Env.find x h
+  else
+    try
+      Env.find x h
+    with Not_found ->
+      Format.printf "Not found while hept_clocking : %a@\n"
+	Idents.print_ident x;
+      raise Not_found
 
 let rec typing_pat h = function
   | Evarpat x -> Ck (ck_of_name h x)
@@ -258,19 +264,25 @@ let typing_contract h contract =
     | Some { c_block = b;
              c_assume = e_a;
              c_enforce = e_g;
-             c_assume_loc = e_a_loc;
-             c_enforce_loc = e_g_loc;
              c_controllables = c_list } ->
         let h' = typing_block h b in
         (* assumption *)
         expect h' (Etuplepat []) (Ck Cbase) e_a;
-        expect h' (Etuplepat []) (Ck Cbase) e_a_loc;
         (* property *)
         expect h' (Etuplepat []) (Ck Cbase) e_g;
-        expect h' (Etuplepat []) (Ck Cbase) e_g_loc;
         
         append_env h c_list
 
+let typing_local_contract h contract =
+  match contract with
+    | None -> ()
+    | Some { c_assume_loc = e_a_loc;
+             c_enforce_loc = e_g_loc } ->
+        (* assumption *)
+        expect h (Etuplepat []) (Ck Cbase) e_a_loc;
+        (* property *)
+        expect h (Etuplepat []) (Ck Cbase) e_g_loc
+
 (* check signature causality and update it in the global env *)
 let update_signature h node =
   let set_arg_clock vd ad =
@@ -287,7 +299,8 @@ let typing_node node =
   let h0 = append_env Env.empty node.n_input in
   let h0 = append_env h0 node.n_output in
   let h = typing_contract h0 node.n_contract in
-  typing_block h node.n_block;
+  let h = typing_block h node.n_block in
+  typing_local_contract h node.n_contract;
   (* synchronize input and output on base : find the free vars and set them to base *)
   Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;
   (*update clock info in variables descriptions *)

compiler/heptagon/transformations/contracts.ml

@@ -31,7 +31,9 @@
 
 (* To be done before "completion" and "switch" transformations *)
 
+open Misc
 open Names
+open Idents
 open Heptagon
 open Hept_utils
 open Hept_mapfold
@@ -45,6 +47,77 @@ open Linearity
 
 let fresh = Idents.gen_var "contracts"
 
+let mk_unique_node nd =
+  let mk_bind vd =
+    let id = fresh (Idents.name vd.v_ident) in
+    (vd.v_ident, { vd with v_ident = id; v_clock = Clocks.fresh_clock () }) in
+  let subst =
+    List.fold_left
+      (fun subst vd ->
+         let id, vd = mk_bind vd in
+         Env.add id vd.v_ident subst)
+      Env.empty
+      (nd.n_input @ nd.n_output) in
+
+  let subst_var_ident _funs subst v =
+    let v = Env.find v subst in
+    v, subst
+  in
+
+  let subst_block funs subst b =
+    let b_local, subst' =
+      mapfold 
+        (fun subst vd ->
+           let id, vd = mk_bind vd in
+           vd, (Env.add id vd.v_ident subst))
+        subst b.b_local in
+    let b, _ = Hept_mapfold.block funs subst' b in
+    { b with b_local = b_local }, subst
+  in
+  
+  let subst_contract_block funs subst b =
+    let b_local, subst' =
+      mapfold 
+        (fun subst vd ->
+           let id, vd = mk_bind vd in
+           vd, (Env.add id vd.v_ident subst))
+        subst b.b_local in
+    let b, _ = Hept_mapfold.block funs subst' b in
+    { b with b_local = b_local }, subst'
+  in
+
+  let subst_contract funs subst c =
+    let c_block, subst' = subst_contract_block funs subst c.c_block in
+    let c_assume, subst' = exp_it funs subst' c.c_assume in
+    let c_enforce, subst' = exp_it funs subst' c.c_enforce in
+    let subst =
+    List.fold_left
+      (fun subst vd ->
+         let id, vd = mk_bind vd in
+         Env.add id vd.v_ident subst)
+      subst c.c_controllables in
+    let c_controllables, subst = mapfold (var_dec_it funs) subst c.c_controllables in
+    let c_assume_loc, subst = exp_it funs subst c.c_assume_loc in
+    let c_enforce_loc, subst = exp_it funs subst c.c_enforce_loc in
+    { c_assume = c_assume;
+      c_enforce = c_enforce;
+      c_assume_loc = c_assume_loc;
+      c_enforce_loc = c_enforce_loc;
+      c_block = c_block;
+      c_controllables = c_controllables },
+    subst in
+
+  (* let funs = { defaults with *)
+  (*                var_dec = subst_var_dec; *)
+  (*                eqdesc = subst_eqdesc; *)
+  (*                edesc = subst_edesc; } in *)
+  let funs = { Hept_mapfold.defaults with
+                 block = subst_block;
+		 contract = subst_contract;
+                 global_funs = { Global_mapfold.defaults with
+                                   Global_mapfold.var_ident = subst_var_ident } } in
+  fst (Hept_mapfold.node_dec funs subst nd)
+
 let mk_unique_contract nd =
   let mk_bind vd =
     let id = fresh (Idents.name vd.v_ident) in
@@ -93,11 +166,13 @@ let exp funs (env, newvars, newequs, contracts) exp =
   match exp.e_desc with
   | Eapp ({ a_op = (Enode nn | Efun nn); } as op, argl, rso) ->
     begin try
+      
       let add_reset eq = match rso with
         | None -> eq
         | Some x -> mk_equation (Ereset (mk_block [eq], x)) in
 
-      let ni = mk_unique_contract (QualEnv.find nn env) in
+      let n = QualEnv.find nn env in
+      let ni = mk_unique_node n in
 
       let ci = match ni.n_contract with
           None -> raise Not_found
@@ -190,7 +265,7 @@ let mk_vd_bool v = mk_var_dec ~last:(Last (Some (mk_static_bool true))) v tbool
 let node_dec funs (env, newvars, newequs, contracts) nd =
   let nd, (env, newvars, newequs, contracts) =
     Hept_mapfold.node_dec funs (env, newvars, newequs, contracts) nd in
-  
+
   (* Build assume and guarantee parts from contract list (list of
      ident pairs (v_a,v_g)). Returns also a list of variable
      declarations. *)

compiler/heptagon/transformations/normalize.ml

@@ -351,8 +351,8 @@ let eq funs context eq =
   let context = translate_eq context eq in
     eq, context
 
-let block funs _ b =
-  let _, (v_acc, eq_acc) = Hept_mapfold.block funs ([],[]) b in
+let block funs context b =
+  let _, (v_acc, eq_acc) = Hept_mapfold.block funs context b in
     { b with b_local = v_acc@b.b_local; b_equs = eq_acc}, ([], [])
 
 let contract funs context c =
@@ -361,9 +361,9 @@ let contract funs context c =
   (* Non-void context could mean lost equations *)
   assert (void_context=([],[]));
   let context, e_a = translate ExtValue ([],[]) c.c_assume in
-  let context, e_a_loc = translate ExtValue context c.c_assume_loc in
   let context, e_e = translate ExtValue context c.c_enforce in
-  let context, e_e_loc = translate ExtValue context c.c_enforce_loc in
+  let local_context, e_a_loc = translate ExtValue ([],[]) c.c_assume_loc in
+  let local_context, e_e_loc = translate ExtValue local_context c.c_enforce_loc in
   let (d_list, eq_list) = context in
   { c with
       c_assume = e_a;
@@ -373,7 +373,22 @@ let contract funs context c =
       c_block = { b with
                     b_local = d_list@b.b_local;
                     b_equs = eq_list@b.b_equs; }
-  }, void_context
+  }, local_context
+
+and node_dec funs context nd =
+  let n_input, context = mapfold (var_dec_it funs) context nd.n_input in
+  let n_output, context = mapfold (var_dec_it funs) context nd.n_output in
+  let n_params, context = mapfold (param_it funs.global_funs) context nd.n_params in
+  let n_contract, context =  optional_wacc (contract_it funs) context nd.n_contract in
+  let n_block, context = block_it funs context nd.n_block in
+  { nd with
+      n_input = n_input;
+      n_output = n_output;
+      n_block = n_block;
+      n_params = n_params;
+      n_contract = n_contract }
+  , context
+
 
 let program p =
   let funs = { defaults with block = block; eq = eq; contract = contract } in

compiler/minils/analysis/clocking.ml

@@ -253,7 +253,7 @@ let append_env h vds =
   List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds
 
 
-let typing_contract h contract =
+let typing_contract h0 h contract =
   match contract with
     | None -> None, h
     | Some ({ c_local = l_list;
@@ -263,14 +263,14 @@ let typing_contract h contract =
              c_assume_loc = e_a_loc;
              c_enforce_loc = e_g_loc;
              c_controllables = c_list } as contract) ->
-        let h' = append_env h l_list in
+        let h' = append_env h0 l_list in
         (* assumption *)
         (* property *)
         let eq_list = typing_eqs h' eq_list in
         expect_extvalue h' Cbase e_a;
         expect_extvalue h' Cbase e_g;
-        expect_extvalue h' Cbase e_a_loc;
-        expect_extvalue h' Cbase e_g_loc;
+        expect_extvalue h Cbase e_a_loc;
+        expect_extvalue h Cbase e_g_loc;
         let h = append_env h c_list in
         Some { contract with c_eq = eq_list }, h
 
@@ -278,8 +278,9 @@ let typing_contract h contract =
 let typing_node node =
   let h0 = append_env Env.empty node.n_input in
   let h0 = append_env h0 node.n_output in
-  let contract, h = typing_contract h0 node.n_contract in
-  let h = append_env h node.n_local in
+  let h = append_env h0 node.n_local in
+  let contract, h = typing_contract h0 h node.n_contract in
+  (*   let h = append_env h node.n_local in *)
   let equs = typing_eqs h node.n_equs in
   (* synchronize input and output on base : find the free vars and set them to base *)
   Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;