Correct scoping and typing with contracts

compiler/heptagon/analysis/typing.ml

@@ -1025,14 +1025,14 @@ let typing_contract const_env h contract =
               c_assume = e_a;
               c_enforce = e_g;
               c_controllables = c }) ->
-        let typed_b, defined_names, _ = typing_block const_env h b in
+        let typed_b, defined_names, h' = typing_block const_env h b in
           (* check that the equations do not define other unexpected names *)
           included_env defined_names Env.empty;
 
         (* assumption *)
-        let typed_e_a = expect const_env h (Tid Initial.pbool) e_a in
+        let typed_e_a = expect const_env h' (Tid Initial.pbool) e_a in
         (* property *)
-        let typed_e_g = expect const_env h (Tid Initial.pbool) e_g in
+        let typed_e_g = expect const_env h' (Tid Initial.pbool) e_g in
 
         let typed_c, (c_names, h) = build const_env h c in
 

compiler/heptagon/hept_printer.ml

@@ -270,7 +270,7 @@ let rec print_type_def ff { t_name = name; t_desc = tdesc } =
 let print_contract ff { c_block = b;
                         c_assume = e_a; c_enforce = e_g;
       c_controllables = c} =
-  fprintf ff "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@]"
+  fprintf ff "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@\n@]"
     print_block b
     print_exp e_a
     print_exp e_g

compiler/heptagon/parsing/hept_scoping.ml

@@ -371,12 +371,17 @@ and translate_last = function
   | Last (None) -> Heptagon.Last None
   | Last (Some e) -> Heptagon.Last (Some (expect_static_exp e))
 
-let translate_contract env ct =
-  let b, _ = translate_block env ct.c_block in
-  { 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 }
+let translate_contract env opt_ct =
+  match opt_ct with
+  | None -> None, env
+  | 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'
 
 let params_of_var_decs =
   List.map (fun vd -> Signature.mk_param
@@ -396,10 +401,9 @@ let translate_node node =
   let params = params_of_var_decs node.n_params in
   let inputs = translate_vd_list env0 node.n_input in
   let outputs = translate_vd_list env0 node.n_output in
-  let b, env = translate_block env0 node.n_block in
-  let contract =
-    Misc.optional (translate_contract env) node.n_contract in
-  (* the env of the block is used in the contract translation *)
+  (* Enrich env with controllable variables (used in block) *)
+  let contract, env = translate_contract env0 node.n_contract in
+  let b, _ = translate_block env node.n_block in
   (* add the node signature to the environment *)
   let i = args_of_var_decs node.n_input in
   let o = args_of_var_decs node.n_output in

compiler/heptagon/transformations/normalize.ml

@@ -284,7 +284,23 @@ let block funs _ b =
   let _, (v_acc, eq_acc) = Hept_mapfold.block funs ([],[]) b in
     { b with b_local = v_acc@b.b_local; b_equs = eq_acc}, ([], [])
 
+let contract funs context c =
+  let ({ c_block = b } as c), void_context =
+    Hept_mapfold.contract funs context c in 
+  (* Non-void context could mean lost equations *)
+  assert (void_context=([],[]));
+  let context, e_a = translate Any ([],[]) c.c_assume in
+  let context, e_e = translate Any context c.c_enforce in
+  let (d_list, eq_list) = context in
+  { c with
+      c_assume = e_a;
+      c_enforce = e_e;
+      c_block = { b with
+		    b_local = d_list@b.b_local;
+		    b_equs = eq_list@b.b_equs; }
+  }, void_context
+
 let program p =
-  let funs = { defaults with block = block; eq = eq } in
+  let funs = { defaults with block = block; eq = eq; contract = contract } in
   let p, _ = Hept_mapfold.program funs ([], []) p in
     p

compiler/main/mls2obc.ml

@@ -585,12 +585,12 @@ let translate_contract map mem_var_tys =
 
 (** Returns a map, mapping variables names to the variables
     where they will be stored. *)
-let subst_map inputs outputs locals mem_tys =
+let subst_map inputs outputs controllables c_locals locals mem_tys =
   (* Create a map that simply maps each var to itself *)
   let map =
     List.fold_left
       (fun m { Minils.v_ident = x; Minils.v_type = ty } -> Env.add x (mk_pattern ty (Lvar x)) m)
-      Env.empty (inputs @ outputs @ locals)
+      Env.empty (inputs @ outputs @ controllables @ c_locals @ locals)
   in
   List.fold_left (fun map (x, x_ty) -> Env.add x (mk_pattern x_ty (Lmem x)) map) map mem_tys
 
@@ -601,7 +601,11 @@ let translate_node
     } as n) =
   Idents.enter_node f;
   let mem_var_tys = Mls_utils.node_memory_vars n in
-  let subst_map = subst_map i_list o_list d_list mem_var_tys in
+  let c_list, c_locals = 
+    match contract with
+    | None -> [], []
+    | Some c -> c.Minils.c_controllables, c.Minils.c_local in
+  let subst_map = subst_map i_list o_list c_list c_locals d_list mem_var_tys in
   let (v, si, j, s_list) = translate_eq_list subst_map empty_call_context eq_list in
   let (si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in
   let i_list = translate_var_dec i_list in

compiler/minils/transformations/normalize_mem.ml

@@ -24,11 +24,15 @@ let eq _ (v, eqs) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with
   | _, _ ->
       eq, (v, eq::eqs)
 
+(* Leave contract unchanged (no output defined in it) *)
+let contract funs acc c = c, acc
+
 let node funs acc nd =
   let nd, (v, eqs) = Mls_mapfold.node_dec funs (nd.n_local, []) nd in
     { nd with n_local = v; n_equs = eqs  }, acc
 
 let program p =
-  let funs = { Mls_mapfold.defaults with eq = eq; node_dec = node } in
+  let funs = { Mls_mapfold.defaults with 
+		 eq = eq; node_dec = node; contract = contract } in
   let p, _ = Mls_mapfold.program_it funs ([], []) p in
     p