open Lexing

open Cmdline

open Ast

open Num_domain
open Nonrelational
open Apron_domain

open Abs_domain

open Enum_domain_edd
open Abs_interp_dynpart

module Interpret = Interpret.I

module ItvND = Apron_domain.ND_Box   (* Nonrelational.ND(Intervals_domain.VD) *)
module PolyND = Apron_domain.ND_Poly
module OctND = Apron_domain.ND_Oct
module ItvOND = NumDomainOnly(ItvND)
module PolyOND = NumDomainOnly(PolyND)
module OctOND = NumDomainOnly(OctND)
module ItvEND = NumEnumDomain(Enum_domain.MultiValuation)(ItvND)
module PolyEND = NumEnumDomain(Enum_domain.MultiValuation)(PolyND)
module ItvENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(ItvND)
module PolyENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(PolyND)

module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND)
module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND)

module AI_Itv_EDD = Abs_interp_edd.I(ItvOND)
module AI_Poly_EDD = Abs_interp_edd.I(PolyOND)
module AI_Oct_EDD = Abs_interp_edd.I(OctOND)

module AI_S_Itv_DP = Abs_interp_dynpart.I(ItvEND)
module AI_S_Rel_DP = Abs_interp_dynpart.I(PolyEND)
module AI_EDD_Itv_DP = Abs_interp_dynpart.I(ItvENDEdd)
module AI_EDD_Rel_DP = Abs_interp_dynpart.I(PolyENDEdd)

(* command line options *)
let times = ref false
let dump = ref false
let dumprn = ref false
let test = ref false
let vtest = ref false
let ai_itv = ref false
let ai_poly = ref false
let ai_oct = ref false
let ai_itv_edd = ref false
let ai_poly_edd = ref false
let ai_oct_edd = ref false
let ai_s_itv_dp = ref false
let ai_s_rel_dp = ref false
let ai_edd_itv_dp = ref false
let ai_edd_rel_dp = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
let ai_init_scopes = ref "all"
let ai_disj_v = ref "all"
let ai_max_dp_depth = ref 10
let ai_max_dp_width = ref 100
let ai_vci = ref false
let ai_vvci = ref false
let ifile = ref ""

let usage = "usage: analyzer [options] file.scade"

let options = [
    "--exec-times", Arg.Set times,
        "Show time spent in each function of the analyzer, for some functions";

    "--dump", Arg.Set dump, "Dump program source.";
    "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";

    "--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
    "--test", Arg.Set test, "Simple testing (direct interpret).";

    "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
    "--ai-poly", Arg.Set ai_poly, "Do abstract analysis using Apron polyhedra domain.";
    "--ai-oct", Arg.Set ai_oct, "Do abstract analysis using Apron octagon domain.";

    "--ai-itv-edd", Arg.Set ai_itv_edd,
        "Do abstract analysis using intervals and EDD disjunction domain.";
    "--ai-poly-edd", Arg.Set ai_poly_edd,
        "Do abstract analysis using Apron polyhedra domain and EDD disjunction domain.";
    "--ai-oct-edd", Arg.Set ai_oct_edd,
        "Do abstract analysis using Apron octagon domain and EDD disjunction domain.";

    "--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
        "Do abstract analysis using dynamic partitionning method, "^
        "with intervals and valuation domain for enums.";
    "--ai-s-rel-dp", Arg.Set ai_s_rel_dp,
        "Do abstract analysis using dynamic partitionning method, "^
        "with Apron and valuation domain for enums.";
    "--ai-edd-itv-dp", Arg.Set ai_edd_itv_dp,
        "Do abstract analysis using dynamic partitionning method, "^
        "with intervals and EDD domain for enums.";
    "--ai-edd-rel-dp", Arg.Set ai_edd_rel_dp,
        "Do abstract analysis using dynamic partitionning method, "^
        "with Apron and EDD domain for enums.";
        
    "--ai-vci", Arg.Set ai_vci,
        "Verbose chaotic iterations (show state at each iteration)";
    "--ai-vvci", Arg.Set ai_vvci,
        "Very verbose chaotic iterations (show everything all the time)";
    "--ai-wd", Arg.Set_int ai_widen_delay,
        "Widening delay in abstract analysis of loops (default: 3).";

    "--ai-max-dp-depth", Arg.Set_int ai_max_dp_depth,
        "Maximum depth in the dynamic partitionning tree.";
    "--ai-max-dp-width", Arg.Set_int ai_max_dp_width,
        "Maximum number of dynamically partitionned locations.";

    "--root", Arg.Set_string ai_root,
        "Root node for abstract analysis (default: test).";
    "--no-time", Arg.Set_string ai_no_time_scopes,
        "Scopes for which not to introduce a 'time' variable in analysis.";
    "--disj", Arg.Set_string ai_disj_v,
        "Variables for which to introduce a disjunction.";
    "--init", Arg.Set_string ai_init_scopes,
        "Scopes for which to introduce a 'init' variable in analysis.";
]

let parse_file (filename : string) : prog =
  let f = open_in filename in
  let lex = from_channel f in
  try
    lex.lex_curr_p <- { lex.lex_curr_p with pos_fname = filename; };
    Parser.file Lexer.token lex
  with
  | Parser.Error ->
    Util.error (Printf.sprintf "Parse error (invalid syntax) near %s"
                  (Util.string_of_position lex.lex_start_p))
  | Failure "lexing: empty token" ->
    Util.error (Printf.sprintf "Parse error (invalid token) near %s"
                  (Util.string_of_position lex.lex_start_p))

let do_test_interpret prog verbose =
    let f0 _ = false in
    let s0 = Interpret.init_state (Typing.root_prog prog "test" f0 f0) in
    if verbose then begin
      Format.printf "Init state:@.";
      Interpret.print_state Format.std_formatter s0;
    end;
    let rec it i st =
      let next_st, out =
        Interpret.step st
        ["i", Interpret.int_value i]
      in
      if verbose then begin
        Format.printf "@.> Step %d:@." i;
        Interpret.print_state Format.std_formatter st;
        Format.printf "Outputs:@.";
        List.iter
          (fun (k, v) -> Format.printf "%s = %s@."
              k (Interpret.str_repr_of_val v))
            out;
      end else begin
        Format.printf "%d. %s %s %s@." i 
          (Interpret.str_repr_of_val (List.assoc "a" out))
          (Interpret.str_repr_of_val (List.assoc "b" out))
          (Interpret.str_repr_of_val (List.assoc "c" out));
      end;
      if not (Interpret.as_bool (List.assoc "exit" out)) then
        it (i+1) next_st
    in
    it 0 s0

let () =
    (* AI_Itv_EDD.test (); *)

    Arg.parse options (fun f -> ifile := f) usage;

    if !ifile = "" then begin
        Format.eprintf "No input file...@.";
        exit 1
    end;

    try
      let prog = parse_file !ifile in
      if !dump then Ast_printer.print_prog Format.std_formatter prog;

      let prog = Rename.rename_prog prog in
      if !dumprn then Ast_printer.print_prog Format.std_formatter prog;

      if !ai_itv || !ai_poly || !ai_oct
          || !ai_itv_edd || !ai_poly_edd || !ai_oct_edd
          || !ai_s_itv_dp || !ai_s_rel_dp
          || !ai_edd_itv_dp || !ai_edd_rel_dp then
      begin
          let comma_split = Str.split (Str.regexp ",") in
          let match_s s pat =
            let n, m = String.length s, String.length pat in
            let memo = Array.make_matrix (n+1) (m+1) None in
            let rec aux i j =
              match memo.(i).(j) with
              | Some x -> x
              | None ->
                let x =
                  if i = n && j = m
                    then true
                  else if j = m && i < n
                    then false
                  else if i = n && j < m
                    then pat.[j] = '*' && aux i (j+1)
                  else
                    if pat.[j] = '*'
                      then aux (i+1) j || aux i (j+1)
                      else s.[i] = pat.[j] && aux (i+1) (j+1)
                in memo.(i).(j) <- Some x; x
            in aux 0 0
          in
          let select_f x =
              if x = "all" then
                (fun _ -> true)
              else if x = "last" then
                (fun i -> i.[0] = 'L')
              else if String.length x > 5 && String.sub x 0 5 = "last+" then
                let psl = comma_split
                  (String.sub x 5 (String.length x - 5)) in
                (fun i -> i.[0] = 'L' || List.exists (match_s i) psl)
              else
                 (fun i -> List.mem i (comma_split x))
          in
          let rp = Typing.root_prog prog !ai_root
              (select_f !ai_no_time_scopes)
              (select_f !ai_init_scopes) in

          let disj = select_f !ai_disj_v in

          let opt = {
              widen_delay = !ai_widen_delay;
              disjunct = disj;
              verbose_ci = !ai_vci;
              vverbose_ci = !ai_vvci;
              max_dp_width = !ai_max_dp_width;
              max_dp_depth = !ai_max_dp_depth;
          } in
          
          if !ai_itv then AI_Itv.do_prog opt rp;
          if !ai_poly then AI_Poly.do_prog opt rp;
          if !ai_oct then AI_Oct.do_prog opt rp;
          
          if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
          if !ai_poly_edd then AI_Poly_EDD.do_prog opt rp;
          if !ai_oct_edd then AI_Oct_EDD.do_prog opt rp;

          if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
          if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
          if !ai_edd_itv_dp then AI_EDD_Itv_DP.do_prog opt rp;
          if !ai_edd_rel_dp then AI_EDD_Rel_DP.do_prog opt rp;
      end;

      if !vtest then do_test_interpret prog true
      else if !test then do_test_interpret prog false;

      if !times then Util.show_times();

    with
    | Util.NoLocError e -> Format.eprintf "Error: %s@." e
    | Util.LocError(l, e) ->
        Format.eprintf "Error: %s@." e;
        List.iter
          (fun loc -> Format.eprintf "At: %s@." (Util.string_of_extent loc))
          l