From 88ecd2d5f2b27a09060313fd29fd087b92e6166e Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Mon, 30 Jun 2014 17:43:06 +0200
Subject: Implement chaotic iterations on EDDs. Global widening is missing.

---
 main.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'main.ml')

diff --git a/main.ml b/main.ml
index dde682f..f38a484 100644
--- a/main.ml
+++ b/main.ml
@@ -13,8 +13,10 @@ module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
 module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
 
 module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
+module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
 
 (* command line options *)
+let times = ref false
 let dump = ref false
 let dumprn = ref false
 let test = ref false
@@ -22,6 +24,7 @@ let vtest = ref false
 let ai_itv = ref false
 let ai_rel = ref false
 let ai_itv_edd = ref false
+let ai_rel_edd = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 3
 let ai_no_time_scopes = ref ""
@@ -33,6 +36,7 @@ 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).";
@@ -40,6 +44,7 @@ let options = [
     "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
     "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
     "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain.";
+    "--ai-rel-edd", Arg.Set ai_rel_edd, "Do abstract analysis using Apron and EDD disjunction domain.";
     "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
     "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
     "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
@@ -80,7 +85,7 @@ let do_test_interpret prog verbose =
     it 0 s0
 
 let () =
-    AI_Itv_EDD.test ();
+    (* AI_Itv_EDD.test (); *)
 
     Arg.parse options (fun f -> ifile := f) usage;
 
@@ -96,7 +101,7 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !ai_itv || !ai_rel || !ai_itv_edd then begin
+      if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin
           let comma_split = Str.split (Str.regexp ",") in
           let select_f x =
               if x = "all"
@@ -119,11 +124,14 @@ let () =
           if !ai_rel then AI_Rel.do_prog opt rp;
           
           if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
+          if !ai_rel_edd then AI_Rel_EDD.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) ->
-- 
cgit v1.2.3