Commit fdb1f1e1 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

removed fresh_name from process.ml

avoid multiple binding for the same term
parent 5f75a67d
......@@ -238,9 +238,9 @@ let reveal_element formula i =
and the term t in formula. The term t must type-check. *)
let add_binding : type a. formula -> variable_string -> a term -> formula =
fun formula s t ->
let env' = env_add_binding formula.env s t in
let env' = env_add_binding formula.env s t in
{ formula with env = env' }
{ formula with env = env' }
(* remove_binding formula s: Remove the binding associated with s in formula. *)
let remove_binding formula s =
......@@ -249,43 +249,6 @@ let remove_binding formula s =
{ formula with env = env' }
(* (\* clean_bindings formula : Remove all bindings that are unused. *\) *)
(* let clean_bindings formula = *)
(* let clean_bindings_aux : type a. a sort -> formula -> formula = *)
(* fun sort formula -> *)
(* let appears : type a. a sort -> variable_string -> bool = fun sort var -> *)
(* List.exists (fun el -> match el.term_pair with *)
(* | B (b,b') -> (subterm formula.env (t_var var sort) b) *)
(* || (subterm formula.env (t_var var sort) b') *)
(* | T (u,u') -> (subterm formula.env (t_var var sort) u) *)
(* || (subterm formula.env (t_var var sort) u')) *)
(* formula.formula_element_list in *)
(* let f_fold : type a. variable_string list -> (variable_string * a term) -> *)
(* variable_string list = *)
(* fun acc (var, t) -> *)
(* if appears (get_sort t) var then *)
(* acc *)
(* else *)
(* var :: acc in *)
(* let to_remove = match sort with *)
(* | Msg -> *)
(* List.fold_left f_fold [] (get_bindings formula.env Msg) *)
(* | Bool -> *)
(* List.fold_left f_fold [] (get_bindings formula.env Bool) in *)
(* List.fold_left remove_binding formula to_remove in *)
(* clean_bindings_aux Msg formula *)
(* |> (clean_bindings_aux Bool) *)
(*******************)
(* Pretty Printing *)
(*******************)
......
......@@ -475,16 +475,6 @@ let weakly_normalize_proof ?collect:(c=false) state =
state'
(* if c then *)
(* begin *)
(* let new_formula = clean_bindings state'.c_proof.goal in *)
(* state'.c_proof.goal <- new_formula; *)
(* state' *)
(* end *)
(* else *)
(* state' *)
(* We apply FA everywhere we can, except for the following function symbols:
EQ, pk, sk, enc, dec
......
......@@ -358,25 +358,8 @@ module String_map = Map.Make(String)
type map_fresh = int String_map.t
(* Return a fresh string prefixed by s and bind it to the proper type in env.
Never return a string that was already used. *)
let rec fresh_name env map_fresh side s =
let sside = s ^ "_" ^ side_to_short_string side in
let (fresh_s, map_fresh') =
if String_map.mem sside map_fresh then
let i = String_map.find sside map_fresh in
let map_fresh' = String_map.add sside (i + 1) map_fresh in
(sside ^ string_of_int i, map_fresh')
else
let map_fresh' = String_map.add sside 0 map_fresh in
(sside, map_fresh') in
(* If fresh_s was already used then reiterate the process. *)
if is_binded env fresh_s then
fresh_name env map_fresh' side s
else
(fresh_s, map_fresh')
let side_name env side s =
fresh_name env (s ^ "_" ^ side_to_short_string side)
(* Guard are conjunctions of positive and negative boolean terms.
Intuitively, Conj (b, g) ~ Conj (Guard b, g)
......@@ -422,79 +405,73 @@ type guarded_process = guard * concrete process
type configuration =
{ procs : guarded_process list;
env : env;
map_fresh : int String_map.t }
env : env }
(* Apply the internal reduction rules to all process as much as possible.
Notice that when a let binding is encountered, a new binding is added to
the environment. *)
let ireduce conf side =
let rec aux_ireduce reduced_gp_list env map_fresh acc_gp_list =
let rec aux_ireduce reduced_gp_list env acc_gp_list =
match acc_gp_list with
| [] -> (List.rev reduced_gp_list, env, map_fresh)
| [] -> (List.rev reduced_gp_list, env)
| gp :: acc_gp_list' -> match gp with
| g, Nil -> aux_ireduce reduced_gp_list env map_fresh acc_gp_list'
| g, Nil -> aux_ireduce reduced_gp_list env acc_gp_list'
| g, Apply (s, l) ->
let (l_args,env',map_fresh') = match s with
let (l_args,env') = match s with
| Loop (_,i) ->
let l_arg_names = get_args (get_decl s) in
let (l_args,env',map_fresh') =
List.fold_left2 (fun (acc_args,env,map_fresh) t arg_name ->
let (l_args,env') =
List.fold_left2 (fun (acc_args,env) t arg_name ->
if term_is_binded env t then
(t :: acc_args, env, map_fresh)
(t :: acc_args, env)
else
let (var, map_fresh') =
fresh_name env map_fresh side arg_name in
let var =
side_name env side arg_name in
let env' = env_add_binding env var t in
(t :: acc_args, env', map_fresh'))
([],env,map_fresh) l l_arg_names in
(t :: acc_args, env'))
([],env) l l_arg_names in
(List.rev l_args,env',map_fresh')
(List.rev l_args,env')
| _ -> (l,env,map_fresh) in
| _ -> (l,env) in
aux_ireduce
reduced_gp_list
env'
map_fresh'
((g, process_apply s l_args) :: acc_gp_list')
| g, New (s, p') ->
let (name, map_fresh') = fresh_name env map_fresh side s in
let name = side_name env side s in
let env' = bind_new_type env name TName in
aux_ireduce
reduced_gp_list
env'
map_fresh'
((g, process_subst s (t_name name Msg) p') :: acc_gp_list')
| g, Parallel (p', p'') ->
aux_ireduce
reduced_gp_list
env
map_fresh
((g, p') :: (g, p'') :: acc_gp_list')
| g, IfThenElse (b, p', p'') ->
aux_ireduce
reduced_gp_list
env
map_fresh
((Conj (b, g), p') :: (NConj (b, g), p'') :: acc_gp_list')
| _, In _ | _,Out _ ->
aux_ireduce
(gp :: reduced_gp_list)
env
map_fresh
acc_gp_list'
| g, Let (s, t, p') ->
......@@ -502,24 +479,21 @@ let ireduce conf side =
aux_ireduce
reduced_gp_list
env
map_fresh
((g, process_subst s t p') :: acc_gp_list')
else
let (var, map_fresh') = fresh_name env map_fresh side s in
let var = side_name env side s in
let env' = env_add_binding env var t in
aux_ireduce
reduced_gp_list
env'
map_fresh'
((g, process_subst s t p') :: acc_gp_list') in
let (gp_list',env',map_fresh') =
aux_ireduce [] conf.env conf.map_fresh conf.procs in
let (gp_list',env') =
aux_ireduce [] conf.env conf.procs in
{ procs = gp_list';
env = env';
map_fresh = map_fresh' }
env = env' }
(********************************)
(* Action-Deterministic process *)
......@@ -893,8 +867,7 @@ let get_option x = match x with
(* get_adv_term conf env map s: Return the term representing an
adversarial input in a pi-calculus input variable s. *)
let get_adv_term (conf : configuration) frame phi side s =
let env = conf.env
and map_fresh = conf.map_fresh in
let env = conf.env in
let i = List.length frame in
let adv_term_fun_name = "g" ^ (string_of_int i) in
......@@ -906,12 +879,11 @@ let get_adv_term (conf : configuration) frame phi side s =
let env' = bind_type env adv_term_fun_name (TFun 1) in
(* We bind Var s to the message computed by the attacker. *)
let (var,map_fresh') = fresh_name env' map_fresh side s in
let var = side_name env' side s in
let env'' = env_add_binding env' var adv_term in
let new_conf = { conf with env = env'';
map_fresh = map_fresh' } in
let new_conf = { conf with env = env'' } in
(adv_term, new_conf)
......@@ -925,15 +897,14 @@ type f_conf_side =
type f_conf =
{ left_c : f_conf_side;
right_c : f_conf_side;
f_env : env;
f_map_fresh : int String_map.t }
f_env : env }
(* sorted_conf f_conf_side env map_fresh : Return the corresponding
configuration, where guarded processes are sorted according to the
lexicographical order on (x,c) where x \in {in,out} and c is the
(input or output) channel name (inputs are first). *)
let sorted_conf f_conf_side env map_fresh =
let sorted_conf f_conf_side env =
let gp_compare gp1 gp2 = match gp1, gp2 with
| (_, In _), (_, Out _) -> -1
......@@ -947,8 +918,7 @@ let sorted_conf f_conf_side env map_fresh =
let gp_list' = List.stable_sort gp_compare f_conf_side.f_procs in
{ procs = gp_list';
env = env;
map_fresh = map_fresh }
env = env }
(* apply_action action side f_conf: Apply 'action' to 'f_conf' in the
environment 'env', and return the new f_conf. *)
......@@ -959,8 +929,7 @@ let apply_action action side f_conf =
let frame = f_conf_side.frame
and phi = f_conf_side.phi in
let sorted_conf = sorted_conf f_conf_side
f_conf.f_env f_conf.f_map_fresh in
let sorted_conf = sorted_conf f_conf_side f_conf.f_env in
let (new_conf, itree) =
List.fold_left
......@@ -1016,11 +985,9 @@ let apply_action action side f_conf =
(* We define the new frame variable phi', and bind it in the environment. *)
let i = List.length frame
and env = red_new_conf.env
and map_fresh = red_new_conf.map_fresh in
and env = red_new_conf.env in
let (var_phi', map_fresh') =
fresh_name env map_fresh side ("phi" ^ string_of_int i) in
let var_phi' = side_name env side ("phi" ^ string_of_int i) in
let term_phi' = t_fun "pair" [phi; norm_outputed_term] in
......@@ -1030,8 +997,7 @@ let apply_action action side f_conf =
frame = norm_outputed_term :: frame;
phi = term_phi' } in
let f_conf' = { f_conf with f_env = env';
f_map_fresh = map_fresh' } in
let f_conf' = { f_conf with f_env = env' } in
match side with
| Left -> { f_conf' with left_c = f_conf_side' }
......@@ -1121,18 +1087,14 @@ let fold_protocol env left_process right_process =
(aux new_f_conf) @ acc)
[] (fold f_conf) in
let init_map = String_map.empty in
let l_red_conf =
ireduce { procs = [(NilGuard, left_process)];
env = env;
map_fresh = init_map } Left in
env = env } Left in
let r_red_conf =
ireduce { l_red_conf with procs = [(NilGuard, right_process)] } Right in
let new_env = r_red_conf.env
and new_map_fresh = r_red_conf.map_fresh in
let new_env = r_red_conf.env in
let left_f_conf_s =
{ f_procs = l_red_conf.procs;
......@@ -1146,5 +1108,4 @@ let fold_protocol env left_process right_process =
aux { left_c = left_f_conf_s;
right_c = right_f_conf_s;
f_env = new_env;
f_map_fresh = new_map_fresh }
f_env = new_env }
......@@ -503,18 +503,26 @@ let bindings_to_print env =
(* Variable typing *)
(*******************)
let fresh_ht = Hashtbl.create ~random:false 256
(* fresh_name env pre : Return a string s such that pre is a preffix of s, and
s is fresh in env. *)
let fresh_name env pre =
let rec fresh_name env pre =
if not (is_binded env pre) then
pre
else
begin
let cpt = ref 0 in
while is_binded env (pre ^ "_" ^ string_of_int !cpt) do
incr cpt
done;
pre ^ "_" ^ string_of_int !cpt
let cpt = try Hashtbl.find fresh_ht pre with
| Not_found -> 0 in
Hashtbl.replace fresh_ht pre (cpt + 1);
let tent_s = (pre ^ "_" ^ string_of_int cpt) in
if is_binded env tent_s then
fresh_name env pre
else
tent_s
end
let typing_err env s mtype =
......@@ -718,34 +726,37 @@ let env_add_binding : type a. env -> variable_string -> a term -> env =
if StringMap.mem s env'.string_types then
raise (Bad_binding (TVar,(StringMap.find s env'.string_types)));
let type_map = match get_sort t with
| Msg -> StringMap.add s TVar env'.string_types
| Bool -> StringMap.add s BTVar env'.string_types in
let hide_map = StringMap.add s true env'.hide_bindings in
let term_map : msg term StringMap.t = match get_sort t with
| Msg -> StringMap.add s t env'.t_bindings
| _ -> env'.t_bindings in
let r_term_map = match get_sort t with
| Msg -> TMap.add t s env'.r_t_bindings
| _ -> env'.r_t_bindings in
let bterm_map : boole term StringMap.t = match get_sort t with
| Bool -> StringMap.add s t env'.bt_bindings
| _ -> env'.bt_bindings in
let r_bterm_map = match get_sort t with
| Bool -> BTMap.add t s env'.r_bt_bindings
| _ -> env'.r_bt_bindings in
{ t_bindings = term_map;
r_t_bindings = r_term_map;
bt_bindings = bterm_map;
r_bt_bindings = r_bterm_map;
hide_bindings = hide_map;
string_types = type_map }
if term_is_binded env t then
env
else
let type_map = match get_sort t with
| Msg -> StringMap.add s TVar env'.string_types
| Bool -> StringMap.add s BTVar env'.string_types in
let hide_map = StringMap.add s true env'.hide_bindings in
let term_map : msg term StringMap.t = match get_sort t with
| Msg -> StringMap.add s t env'.t_bindings
| _ -> env'.t_bindings in
let r_term_map = match get_sort t with
| Msg -> TMap.add t s env'.r_t_bindings
| _ -> env'.r_t_bindings in
let bterm_map : boole term StringMap.t = match get_sort t with
| Bool -> StringMap.add s t env'.bt_bindings
| _ -> env'.bt_bindings in
let r_bterm_map = match get_sort t with
| Bool -> BTMap.add t s env'.r_bt_bindings
| _ -> env'.r_bt_bindings in
{ t_bindings = term_map;
r_t_bindings = r_term_map;
bt_bindings = bterm_map;
r_bt_bindings = r_bterm_map;
hide_bindings = hide_map;
string_types = type_map }
(* env_remove_binding env s: Remove the binding associated with s in env. *)
let env_remove_binding env s =
......
......@@ -4,7 +4,6 @@ obiwan;
cca2 guard;
cca2 guard;
fab 4;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
......@@ -14,8 +13,8 @@ cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_3,nB_r);
cca2;
cca2 guard;
......@@ -27,8 +26,8 @@ cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_7,nB_r);
cca2;
cca2 guard;
......@@ -41,8 +40,8 @@ cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_11,nB_r);
cca2;
(* Second trace *)
......@@ -56,8 +55,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_15,nB_r);
cca2;
cca2 guard;
......@@ -66,12 +65,12 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi2(dec_g5_0)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_g5_2_0)),nB_r);
cond_fresh Left EQ(pi1(pi2(dec_g5)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_g5_6)),nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_19,nB_r);
cca2;
cca2 guard;
......@@ -82,8 +81,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_23,nB_r);
cca2;
cca2 guard;
......@@ -92,12 +91,12 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi2(dec_g5_0)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_g5_2_0)),nB_r);
cond_fresh Left EQ(pi1(pi2(dec_g5)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_g5_9)),nB_r);
cca2;
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cond_fresh Left EQ(dec_g7,nB_l);
cond_fresh Right EQ(dec_g7_27,nB_r);
cca2;
(* Third trace *)
......@@ -110,8 +109,8 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2 guard;
cond_fresh Left EQ(dec_g5_0,nB_l);
cond_fresh Right EQ(dec_g5_2_0,nB_r);
cond_fresh Left EQ(dec_g5,nB_l);
cond_fresh Right EQ(dec_g5_12,nB_r);
cca2 guard;
......@@ -122,7 +121,7 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2 guard;
cond_fresh Left EQ(dec_g5_0,nB_l);
cond_fresh Right EQ(dec_g5_2_0,nB_r);
cond_fresh Left EQ(dec_g5,nB_l);
cond_fresh Right EQ(dec_g5_15,nB_r);
cca2 guard;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment