(**********************************************************************)
(* (c) Greg Morrisett, Neal Glew,                                     *)
(*     June 1998, all rights reserved.                                *)
(**********************************************************************)

(* tallinkchk.ml
 * TAL Link Verifier
 *
 * Checks various linking operations are correct.
 *)

open Utilities;;
open Identifier;;
open Tal;;
open Talctxt;;
open Talcon;;

type ('a,'b) coalase = ('a,'b) coalase_item list ref
and ('a,'b) coalase_item = {key : 'a; mutable vals : 'b list}
;;

let coalase_new () : ('a,'b) coalase = ref [];;
let coalase_add k v c =
  let rec loop c1 =
    match c1 with
      [] -> c := {key=k; vals=[v]} :: !c
    | ci::c1 ->
	if ci.key=k then ci.vals <- v :: ci.vals else loop c1 in
  loop !c
;;
let coalase_map f c =
  List.map (fun {key=k; vals=vs} -> f k vs) !c
;;
let coalase_iter f c =
  List.iter (fun {key=k; vals=vs} -> f k vs) !c
;;
let coalase_fold f a c =
  List.fold_left (fun a {key=k; vals=vs} -> f a k vs) a !c

let sub_con_def ctxt cd1 cd2 =
  match cd1,cd2 with
    _,AbsCon -> ()
  | AbsCon,(BoundCon _ | ConcCon _) -> generate_error ctxt Con_def_nleq
  | BoundCon c1,BoundCon c2 -> leqcon ctxt c1 c2
  | BoundCon _,ConcCon _ -> generate_error ctxt Con_def_nleq
  | ConcCon c1,BoundCon c2 -> leqcon ctxt c1 c2
  | ConcCon c1,ConcCon c2 -> eqcon ctxt c1 c2
;;

let con_def_meet ctxt cd1 cd2 =
  match cd1,cd2 with
    AbsCon,_ -> cd2
  | _,AbsCon -> cd1
  | BoundCon c1,BoundCon c2 -> BoundCon (conmeet ctxt c1 c2)
  | ConcCon c1,BoundCon c2 -> leqcon ctxt c1 c2; cd1
  | BoundCon c1,ConcCon c2 -> leqcon ctxt c2 c1; cd2
  | ConcCon c1,ConcCon c2 -> eqcon ctxt c1 c2; cd1
;;

(*** Link Checking ***)

type inex = I | E;;

(* Phase 1: Build a context to check in *)

let link_build_ctxt cons =
  let aux ctxt l iekcds =
    let ctxt = set_loc ctxt (Loccon l) in
    match iekcds with
      [] -> failwith "Tallinkchk.verify_link - internal error 1"
    | (_,k,_)::iekcds ->
	let k =
	  List.fold_left (fun k1 (_,k2,_) -> kindmeet ctxt k1 k2) k iekcds in
	add_con ctxt l k in
  let ctxt = set_verify_ctxt empty_ctxt "building checking context" in
  let ctxt = coalase_fold aux ctxt cons in
  ctxt
;;

(* Phase 2: Process the constructors *)

let link_process_cons ctxt cons =
  let ctxt = set_verify_ctxt ctxt "" in
  let check_cons_loop ctxt (ie1,k1,cd1 as iekcd1) (ie2,k2,cd2 as iekcd2) =
    let aux k1 cd1 k2 cd2 =
      let ctxt = set_verify_ctxt ctxt "verifying export/import consistency" in
      kindleq ctxt k1 k2; sub_con_def ctxt cd1 cd2 in
    match ie1,ie2 with
      I,I ->
	let ctxt = set_verify_ctxt ctxt "verifying two imports consistency" in
	let k = kindmeet ctxt k1 k2 in
	let cd = con_def_meet ctxt cd1 cd2 in
	(I,k,cd)
    | I,E -> aux k2 cd2 k1 cd1; iekcd2
    | E,I -> aux k1 cd1 k2 cd2; iekcd1
    | E,E ->
 	generate_error (set_verify_ctxt ctxt "") Multiple_exports; iekcd1 in
  let check_cons (ctxt,icons,econs) l iekcds =
    let ctxt = set_loc ctxt (Loccon l) in
    match iekcds with
      [] -> failwith "Tallinkchk.verify_link - internal error 2"
    | iekcd::iekcds ->
	let (ie,k,cd) = List.fold_left (check_cons_loop ctxt) iekcd iekcds in
	let ctxt = add_con_def ctxt l cd in
	if ie=E then (ctxt,icons,(l,k,cd)::econs)
 	else (ctxt,(l,k,cd)::icons,econs) in
  coalase_fold check_cons (ctxt,[],[]) cons
;;

(* Phase 3: Process the values *)

let link_process_vals ctxt vals =
  let ctxt = set_verify_ctxt ctxt "" in
  let check_vals_loop ctxt (ie1,c1 as iec1) (ie2,c2 as iec2) =
    let aux c1 c2 =
      let ctxt = set_verify_ctxt ctxt "verifying export/import consistency" in
      leqcon ctxt c1 c2 in
    match ie1,ie2 with
      I,I ->
 	let ctxt = set_verify_ctxt ctxt "verifying two imports consistency" in
	(I,conmeet ctxt c1 c2)
    | I,E -> aux c2 c1; iec2
    | E,I -> aux c1 c2; iec1
    | E,E -> generate_error (set_verify_ctxt ctxt "") Multiple_exports; iec1 in
  let check_vals (ivals,evals) l iecs =
    let ctxt = set_loc ctxt (Locval l) in
    match iecs with
      [] -> failwith "Tallinkchk.verify_link - internal error 3"
    | iec::iecs ->
	let (ie,c) = List.fold_left (check_vals_loop ctxt) iec iecs in
	if ie=E then (ivals,(l,c)::evals)
 	else ((l,c)::ivals,evals) in
  coalase_fold check_vals ([],[]) vals
;;

(* The whole thing *)

let verify_link intts =
  let cons = coalase_new () in
  let aux1 inex (l,k,cd) = coalase_add l (inex,k,cd) cons in
  let aux2 (imp,exp) =
    List.iter (aux1 I) imp.it_cons; List.iter (aux1 E) exp.it_cons in
  List.iter aux2 intts;
  let ctxt = link_build_ctxt cons in
  let (ctxt,icons,econs) = link_process_cons ctxt cons in
  let vals = coalase_new () in
  let aux1 inex (l,c) = coalase_add l (inex,c) vals in
  let aux2 (imp,exp) =
    List.iter (aux1 I) imp.it_vals; List.iter (aux1 E) exp.it_vals in
  List.iter aux2 intts;
  let (ivals,evals) = link_process_vals ctxt vals in
  ({it_cons=icons; it_vals=ivals}, {it_cons=econs; it_vals=evals})
;;

(*** Program Checking ***)

let rec assoc2 k l =
  match l with
    [] -> raise Not_found
  | (k1,v1,v2)::l -> if k=k1 then (v1,v2) else assoc2 k l
;;

let sub_intt s1 s2 intt1 intt2 =
  let aux ctxt (l,k,_) = add_con (set_loc ctxt (Loccon l)) l k in
  let ctxt =
    set_verify_ctxt empty_ctxt ("building checking context for "^s1) in
  let ctxt = List.fold_left aux ctxt intt1.it_cons in
  let ctxt = set_verify_ctxt ctxt ("verifying "^s1) in
  let check_con ctxt (l,k1,cd1) =
    let ctxt = set_loc ctxt (Loccon l) in
    (try
      let (k2,cd2) = assoc2 l intt1.it_cons in
      kindleq ctxt k2 k1; sub_con_def ctxt cd2 cd1
    with Not_found -> generate_error ctxt (Intt_nleq s2));
    add_con_def ctxt l cd1 in
  let ctxt = List.fold_left check_con ctxt intt2.it_cons in
  let check_val (l,c1) =
    let ctxt = set_loc ctxt (Locval l) in
    (try
      let c2 = List.assoc l intt1.it_vals in
      leqcon ctxt c1 c2
    with Not_found -> generate_error ctxt (Intt_nleq s2)) in
  List.iter check_val intt2.it_vals
;;

let sub_module (imps1,exps1) (imps2,exps2) =
  sub_intt "imports" "extra label" imps2 imps1;
  sub_intt "exports" "missing label" exps1 exps2
;;

let prog_imex = ref ({it_cons=[]; it_vals=[]},{it_cons=[]; it_vals=[]});;

let set_program_interface ref2int imps exps =
  let ctxt = set_verify_ctxt empty_ctxt "setting program interface" in
  let imps = Talverify.process_impexps ref2int imps in
  let exps = Talverify.process_impexps ref2int exps in
  let aux1 ctxt (l,k,_) = add_con (set_loc ctxt (Loccon l)) l k in
  let aux2 ctxt (abbrevs,int) =
    Array.fold_left aux1 (set_abbrevs ctxt abbrevs) int.int_cons in
  let ctxt = Array.fold_left aux2 ctxt imps in
  let ctxt = Array.fold_left aux2 ctxt exps in
  let aux1 (ctxt,cons) (l,k,cd) =
    let ctxt = set_loc ctxt (Loccon l) in
    let cd =
      match cd with
      	AbsCon -> cd
      |	BoundCon c -> BoundCon (snd (check_whnorm ctxt c))
      |	ConcCon c -> ConcCon (snd (check_whnorm ctxt c)) in
    (add_con_def ctxt l cd,(l,k,cd)::cons) in
  let aux2 (ctxt,cons) (abbrevs,int) =
    Array.fold_left aux1 (set_abbrevs ctxt abbrevs,cons) int.int_cons in
  let (ctxt,icons) = Array.fold_left aux2 (ctxt,[]) imps in
  let (ctxt,econs) = Array.fold_left aux2 (ctxt,[]) exps in
  let aux1 ctxt vals (l,c) =
    (l,snd (check_whnorm (set_loc ctxt (Locval l)) c))::vals in
  let aux2 vals (abbrevs,int) =
    Array.fold_left (aux1 (set_abbrevs ctxt abbrevs)) vals int.int_vals in
  let ivals = Array.fold_left aux2 [] imps in
  let evals = Array.fold_left aux2 [] exps in
  prog_imex := ({it_cons=List.rev icons; it_vals=List.rev ivals},
		{it_cons=List.rev econs; it_vals=List.rev evals})
;;

let verify_program progt =
  sub_module progt !prog_imex
;;

(* tallinkchk.ml *)
