Ported Initialization and Causality

Removed safe property from initialization.

heptagon/analysis/causal.ml

@@ -37,14 +37,12 @@ type sc =
   | Ctuple of sc list
   | Cwrite of ident
   | Cread of ident
-  | Clinread of ident
   | Clastread of ident
   | Cempty
 
 (* normalized constraints *)
 type ac =
     | Awrite of ident
-    | Alinread of ident
     | Aread of ident
     | Alastread of ident
     | Aseq of ac * ac
@@ -85,7 +83,6 @@ let output_ac ff ac =
 	  fprintf ff ")"
       | Awrite(m) -> fprintf ff "%s" (sourcename m)
       | Aread(m) -> fprintf ff "^%s" (sourcename m)
-      | Alinread(m) -> fprintf ff "*%s" (sourcename m)
       | Alastread(m) -> fprintf ff "last %s" (sourcename m)
     end;
     fprintf ff "@]" in
@@ -134,7 +131,6 @@ let rec ctuple l =
   let conv = function
     | Cwrite(n) -> Awrite(n)
     | Cread(n) -> Aread(n)
-    | Clinread(n) -> Alinread(n)
     | Clastread(n) -> Alastread(n)
     | Ctuple(l) -> Atuple (ctuple l)
     | Cand _ -> Format.printf "Unexpected and\n"; assert false
@@ -154,7 +150,6 @@ let rec norm = function
   | Ctuple l -> Aac(Atuple (ctuple l))
   | Cwrite(n) -> Aac(Awrite(n))
   | Cread(n) -> Aac(Aread(n))
-  | Clinread(n) -> Aac(Alinread(n))
   | Clastread(n) -> Aac(Alastread(n))
   | _ -> Aempty
 
@@ -166,8 +161,6 @@ let build ac =
   let rec associate_node g (n_to_graph,lin_map) = function
     | Awrite(n) ->
         nametograph n g n_to_graph, lin_map
-    | Alinread(n) ->
-	n_to_graph, nametograph n g lin_map
     | Atuple l ->
 	List.fold_left (associate_node g) (n_to_graph, lin_map) l
     | _ -> 
@@ -204,7 +197,6 @@ let build ac =
 
     let rec add_dependence g = function
         | Aread(n) -> attach g n; attach_lin g n
-	| Alinread(n) -> let g = Env.find n lin_map in attach g n
 	| Atuple l -> List.iter (add_dependence g) l
 	| _ -> ()
     in
@@ -220,7 +212,6 @@ let build ac =
 	    )
       in 
 	match ac with 
-	  | Alinread n -> Env.find n lin_map
 	  | Awrite n -> Env.find n n_to_graph
 	  | Atuple l ->
 	      begin try
@@ -247,7 +238,6 @@ let build ac =
               top1 @ top2, bot1 @ bot2
 	| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
 	| Aread(n) -> let g = make ac in attach g n; attach_lin g n; [g], [g]
-	| Alinread(n) -> let g = Env.find n lin_map in attach g n; [g], [g]
 	| Atuple(l) -> 
 	    let g = node_for_ac ac in
 	      List.iter (add_dependence g) l;

heptagon/analysis/causality.ml

@@ -16,7 +16,6 @@ open Names
 open Ident
 open Heptagon
 open Location
-open Linearity
 open Graph
 open Causal
 
@@ -56,7 +55,6 @@ let rec cseqlist l =
   | c1 :: l -> cseq c1 (cseqlist l)
 
 let read x = Cread(x)
-let linread x = Clinread(x)
 let lastread x = Clastread(x)
 let cwrite x = Cwrite(x)
 
@@ -66,7 +64,7 @@ let rec pre = function
   | Cand(c1, c2) -> Cand(pre c1, pre c2)
   | Ctuple l -> Ctuple (List.map pre l)
   | Cseq(c1, c2) -> Cseq(pre c1, pre c2)
-  | Cread(x) | Clinread (x) -> Cempty
+  | Cread(x) -> Cempty
   | (Cwrite _ | Clastread _ | Cempty) as c -> c
 
 (* projection and restriction *)
@@ -86,7 +84,7 @@ let clear env c =
         let c2 = clearec c2 in
         cseq c1 c2
     | Ctuple l -> Ctuple (List.map clearec l)
-    | Cwrite(id) | Cread(id) | Clinread(id) | Clastread(id) ->
+    | Cwrite(id) | Cread(id) | Clastread(id) ->
         if IdentSet.mem id env then Cempty else c
     | Cempty -> c in
   clearec c
@@ -99,11 +97,7 @@ let rec typing e =
   match e.e_desc with
     | Econst(c) -> cempty
     | Econstvar(x) -> cempty
-    | Evar(x) -> 
+    | Evar(x) -> read x
-	(match e.e_linearity with
-	   | At _ -> linread x
-	   | _ -> read x
-	)
     | Elast(x) -> lastread x
     | Etuple(e_list) ->
 	candlist (List.map typing e_list)
@@ -114,7 +108,6 @@ let rec typing e =
 	candlist l
     | Earray(e_list) ->
 	candlist (List.map typing e_list)
-    | Ereset_mem _ -> assert false
 
 (** Typing an application *)
 and apply op e_list =
@@ -133,14 +126,24 @@ and apply op e_list =
 	let i2 = typing e2 in
 	let i3 = typing e3 in
 	cseq t1 (cor i2 i3)
-    | (Enode _ | Eevery _ | Eop _ | Eiterator (_, _, _, _)
+    | Ecall _, e_list ->
-      | Econcat | Eselect_slice | Emake _ | Eflatten _
+	      ctuplelist (List.map typing e_list)
-      | Eselect_dyn | Eselect _ | Erepeat | Ecopy), e_list ->
+    | Efield_update _, [e1;e2] ->
-	ctuplelist (List.map typing e_list)
+	      let t1 = typing e1 in
-    | Eupdate _, [e1;e2] | Efield_update _, [e1;e2] ->
+	      let t2 = typing e2 in
-	let t1 = typing e1 in
+	        cseq t2 t1
-	let t2 = typing e2 in
+    | Earray_op op, e_list ->
-	cseq t2 t1
+        apply_array_op op e_list
+
+and apply_array_op op e_list =
+  match op, e_list with 
+    | (Eiterator (_, _, _) | Econcat | Eselect_slice 
+      | Eselect_dyn | Eselect _ | Erepeat), e_list -> 
+        ctuplelist (List.map typing e_list)
+    | Eupdate _, [e1;e2] ->
+	      let t1 = typing e1 in
+	      let t2 = typing e2 in
+	        cseq t2 t1
 	
 let rec typing_pat = function
   | Evarpat(x) -> cwrite(x)

heptagon/analysis/initialization.ml

@@ -16,6 +16,7 @@ open Misc
 open Names
 open Ident
 open Heptagon
+open Types
 open Location
 open Format
 
@@ -90,8 +91,8 @@ let rec initialized i =
 (* build an initialization type from a type *)
 let rec skeleton i ty =
   match ty with
-    | Tbase _ -> leaf i
     | Tprod(ty_list) -> product (List.map (skeleton i) ty_list)
+    | _ -> leaf i
 
 (* sub-typing *)
 let rec less left_ty right_ty =
@@ -188,10 +189,6 @@ let less_exp e actual_ty expected_ty =
     less actual_ty expected_ty
   with | Unify -> Error.message e.e_loc (Error.Eclash(actual_ty, expected_ty))
 
-(** Is-it a safe imported value? *)
-let safe f =
-  let { Global.info = { Global.safe = s } } = Modules.find_value f in s
-
 (** Main typing function *)
 let rec typing h e =
   match e.e_desc with
@@ -234,19 +231,8 @@ and apply h op e_list =
 	let i2 = itype (typing h e2) in
 	let i3 = itype (typing h e3) in
 	max i1 (max i2 i3)
-    | (Enode(f,_) | Eevery(f,_)), e_list ->
+    | (Ecall _ | Earray_op _| Efield_update _) , e_list ->
-	List.iter (fun e -> initialized_exp h e) e_list; izero
+	      List.iter (fun e -> initialized_exp h e) e_list; izero
-    | Eop(f,_), e_list when safe f ->
-	(* unsafe primitives must have an initialized argument *)
-	List.fold_left (fun acc e -> itype (typing h e)) izero e_list
-    | Eop(f,_), e_list ->
-	List.iter (fun e -> initialized_exp h e) e_list; izero
-(*Array operators*)
-    | (Erepeat | Econcat | Eupdate _ | Efield_update _
-      | Eselect _ | Eselect_dyn | Eselect_slice
-      | Eiterator _ | Ecopy | Emake _ | Eflatten _), e_list ->
-	List.iter (fun e -> initialized_exp h e) e_list; izero
-    | _ -> assert false
 
 and expect h e expected_ty =
   let actual_ty = typing h e in