path: root/main.ml

open Ast

module Interpret = Interpret.I

module ItvND = Nonrelational.ND(Intervals_domain.VD)
module ItvD = Abs_domain.D(ItvND)

module ApronD = Abs_domain.D(Apron_domain.ND)

module AI_Itv = Abs_interp.I(ItvD)
module AI_Rel = Abs_interp.I(ApronD)

(* command line options *)
let dump = ref false
let dumprn = ref false
let test = ref false
let vtest = ref false
let ai_itv = ref false
let ai_rel = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 3
let ifile = ref ""

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

let options = [
    "--dump", Arg.Set dump, "Dump program source.";
    "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
    "--vtest", Arg.Set vtest, "Verbose testing.";
    "--test", Arg.Set test, "Simple testing.";
    "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
    "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
    "--ai-root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
    "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
]

let do_test_interpret prog verbose =
    let s0 = Interpret.init_state (Typing.root_prog prog "test") 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 () =
    Arg.parse options (fun f -> ifile := f) usage;

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

    try
      let prog = File_parser.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 then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
      if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);

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

    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@." (Ast_printer.string_of_extent loc))
          l