diff --git a/domains/DecisionTree.ml b/domains/DecisionTree.ml index ea56d30..6c8ff76 100644 --- a/domains/DecisionTree.ml +++ b/domains/DecisionTree.ml @@ -86,7 +86,15 @@ struct | Node ((c,_),l,r) -> Format.fprintf fmt "\n%sNODE %a%a%a" ind (C.print vars) c (aux (ind ^ " ")) l (aux (ind ^ " ")) r in aux "" fmt t - + let output_json vars t:Yojson.Safe.t= + + let rec aux t = + match t with + | Bot -> `String "BOT" + | Leaf f -> `Assoc [("Leaf", `String (Format.asprintf "%a" (F.print) f))] + | Node ((c,_),l,r) -> + `Assoc [("Node",`Assoc [("constraint",`String (Format.asprintf "%a" (C.print vars) c ));("left", aux l );("right", aux r)] )] + in aux t.tree (** Prints a tree in graphviz 'dot' format for visualization. http://www.graphviz.org/content/dot-language diff --git a/domains/Domain.ml b/domains/Domain.ml index 99d2d64..593f526 100644 --- a/domains/Domain.ml +++ b/domains/Domain.ml @@ -43,6 +43,7 @@ sig val compress : t -> t val print : Format.formatter -> t -> unit + val output_json : var list -> t -> Yojson.Safe.t val print_graphviz_dot : Format.formatter -> t -> unit end diff --git a/domains/dune b/domains/dune index 5f10e67..ecb343a 100644 --- a/domains/dune +++ b/domains/dune @@ -1,7 +1,7 @@ (library (name domains) (libraries utils frontend banal apron apron.boxMPQ apron.octMPQ - apron.polkaMPQ) + apron.polkaMPQ yojson) (flags (:standard -open Utils -open Banal -open Frontend -open Apron))) diff --git a/main/CFGCTLIterator.ml b/main/CFGCTLIterator.ml index a3e48ac..55107ed 100644 --- a/main/CFGCTLIterator.ml +++ b/main/CFGCTLIterator.ml @@ -5,7 +5,7 @@ open Apron open Domain open Partition open Functions -open Iterator +open Config open ForwardIterator @@ -334,6 +334,7 @@ module CFGCTLIterator(D: RANKING_FUNCTION) = struct let inv = compute cfg main loop_heads domSets property in let programInvariant = NodeMap.find main.func_entry inv in let precondition = Conversion.of_bool_expr precondition in + tree := (D.output_json (List.map (Cfgfrontend.Conversion.of_var) cfg.cfg_vars) programInvariant); D.defined ~condition:precondition programInvariant end diff --git a/main/CFGForwardIterator.ml b/main/CFGForwardIterator.ml index 166b1d4..cad8604 100644 --- a/main/CFGForwardIterator.ml +++ b/main/CFGForwardIterator.ml @@ -9,7 +9,7 @@ open Cfg open CFGInterpreter open Partition -open Iterator +open Config module CFGForwardIterator (B: PARTITION) = struct diff --git a/main/CFGInterpreter.ml b/main/CFGInterpreter.ml index 6c7dfe5..2139e15 100644 --- a/main/CFGInterpreter.ml +++ b/main/CFGInterpreter.ml @@ -9,7 +9,7 @@ (***************************************************) open Cfg -open Iterator +open Config (* log worklist algorithm *) diff --git a/main/CTLIterator.ml b/main/CTLIterator.ml index dc21835..a302e28 100644 --- a/main/CTLIterator.ml +++ b/main/CTLIterator.ml @@ -5,7 +5,7 @@ open Apron open Domain open Partition open Functions -open Iterator +open Config open ForwardIterator (* type for CTL properties, instantiated with bExp for atomic propositions *) @@ -196,6 +196,7 @@ module CTLIterator(D: RANKING_FUNCTION) = struct if !tracebwd && not !minimal then Format.fprintf !fmt "### %a ###:\n%a\n" label_print blockLabel D.print in_state; addInv blockLabel in_state | A_block (blockLabel,(stmt,_),nextBlock) -> + let pre_dom = if !refine then Some (fwdInv blockLabel) else None in let invBlockKeep = InvMap.find blockLabel inv_keep in let invBlockReset = InvMap.find blockLabel inv_reset in let d_until = fun t -> D.until t invBlockKeep invBlockReset in @@ -204,21 +205,22 @@ module CTLIterator(D: RANKING_FUNCTION) = struct let in_state = match stmt with | A_label (l,_) -> out_state | A_return -> bot - | A_assign ((l,_),(e,_)) -> bwd_assign out_state (l,e) - | A_assert (b,_) -> bwd_filter out_state b + | A_assign ((l,_),(e,_)) -> bwd_assign ?domain: pre_dom out_state (l,e) + | A_assert (b,_) -> bwd_filter ?domain: pre_dom out_state b | A_if ((b,ba),s1,s2) -> let in_if = bwd out_state s1 in (* compute 'in state for if-block*) let in_else = bwd out_state s2 in (* compute 'in state for else-block *) - let in_if_filtered = bwd_filter in_if b in (* filter *) - let in_else_filtered = bwd_filter in_else (fst (negBExp (b,ba))) in (* filter *) + let in_if_filtered = bwd_filter ?domain:pre_dom in_if b in (* filter *) + let in_else_filtered = bwd_filter ?domain:pre_dom in_else (fst (negBExp (b,ba))) in (* filter *) branch_join in_if_filtered in_else_filtered (* join the two branches *) | A_while (l,(b,ba),loop_body) -> - let out_exit = bwd_filter out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *) + let pre_dom = if !refine then Some (fwdInv l) else None in + let out_exit = bwd_filter ?domain:pre_dom out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *) let rec aux (* recursive function that iteratively computes fixed point for 'in' state at loop head *) in_state (* 'in' state of the previous iteration *) out_enter (* current 'out' state when entering the loop body *) n = (* iteration counter *) - let in_state' = d_until (D.join APPROXIMATION out_exit out_enter) in (* 'in' state for this iteration *) + let in_state' = d_until (branch_join out_exit out_enter) in (* 'in' state for this iteration *) if !tracebwd && not !minimal then begin Format.fprintf !fmt "### %a:%i ###:\n" label_print l n; Format.fprintf !fmt "out_exit: %a\n" D.print out_exit; @@ -228,7 +230,9 @@ module CTLIterator(D: RANKING_FUNCTION) = struct end; let isLeqComp = D.isLeq COMPUTATIONAL in_state' in_state in let isLeqApprox = D.isLeq APPROXIMATION in_state' in_state in - if isLeqComp && isLeqApprox then + let jokers = max 0 (!retrybwd * (!Ordinals.max + 1) - n + !joinbwd) in + if isLeqComp then + if isLeqApprox then begin (* fixed-point reached *) let fixed_point = in_state in if !tracebwd && not !minimal then begin @@ -236,25 +240,44 @@ module CTLIterator(D: RANKING_FUNCTION) = struct Format.fprintf !fmt "in_state: %a\n" D.print fixed_point; end; fixed_point - else - (*fixed-point not yet reached, continue with next iteration*) + end + else begin + (*fixed-point not yet reached, continue with next iteration*) let in_state'' = if n <= !joinbwd then in_state' (* iteration count below widening threshold *) - else if (not isLeqComp) then - D.widen in_state (D.join COMPUTATIONAL in_state in_state') (* widening threshold reached, apply widening *) - (* NOTE: the join might be necessary to ensure termination because of a bug (???) *) - else - D.widen in_state in_state' (* widening threshold reached, apply widening *) + else + D.widen ~jokers:jokers in_state in_state' (* widening threshold reached, apply widening *) + in if !tracebwd && not !minimal then Format.fprintf !fmt "in'': %a\n" D.print in_state''; - let out_enter' = bwd_filter (bwd in_state'' loop_body) b in (* process loop body again with updated 'in' state *) + let out_enter' = bwd_filter ?domain: pre_dom (bwd in_state'' loop_body) b in (* process loop body again with updated 'in' state *) aux in_state'' out_enter' (n+1) (* run next iteration *) + end + else + let in_state'' = + if n <= !joinbwd then + in_state' + else + D.widen ~jokers:jokers in_state + (D.join COMPUTATIONAL in_state in_state') + (* NOTE: the join might be necessary to ensure termination because of a bug (???) *) + in + if !tracebwd && not !minimal then + Format.fprintf !fmt "in'': %a\n" D.print in_state''; + let out_enter' = + (bwd in_state'' loop_body) in + let out_enter' = D.filter ?domain:pre_dom out_enter' b in + aux in_state'' out_enter' (n + 1) in - let initial_in = bot in (* start with bottom as initial 'in' state *) - let initial_out_enter = bwd_filter (bwd initial_in loop_body) b in (* process loop body with initial 'in' state *) + let initial_in = D.bot ?domain:pre_dom program.environment program.variables in (* start with bottom as initial 'in' state *) + let initial_out_enter = D.filter ?domain:pre_dom (bwd initial_in loop_body) b in (* process loop body with initial 'in' state *) let final_in_state = aux initial_in initial_out_enter 1 in (* compute fixed point for loop-head *) - addInv l final_in_state + let ret = addInv l final_in_state in + if !refine then + D.refine ret (Option.get pre_dom) + else + ret | A_call (f,ss) -> raise (Invalid_argument "bwdStm:A_call") | A_recall (f,ss) -> raise (Invalid_argument "bwdStm:A_recall") in @@ -299,18 +322,20 @@ module CTLIterator(D: RANKING_FUNCTION) = struct let out = if !refine then D.refine out (fwdInv blockLabel) else out in addInv blockLabel (D.mask current_in out) | A_block (blockLabel, (stmt,_), nextBlock) -> + let pre_dom = if !refine then Some (fwdInv blockLabel) else None in let out_state = bwd out nextBlock in (* recursively process the rest of the program, this gives us the 'out' state for this statement *) let new_in = match stmt with | A_label (l,_) -> out_state | A_return -> if use_sink_state then zero else bot - | A_assign ((l,_),(e,_)) -> D.mask current_in (bwd_assign out_state (l,e)) - | A_assert (b,_) -> D.mask current_in (bwd_filter out_state b) + | A_assign ((l,_),(e,_)) -> D.mask current_in (bwd_assign ?domain:pre_dom out_state (l,e)) + | A_assert (b,_) -> D.mask current_in (bwd_filter ?domain:pre_dom out_state b) | A_if ((b,ba),s1,s2) -> - let out_if = bwd_filter (bwd out_state s1) b in (* compute 'out' state for if-block*) - let out_else = bwd_filter (bwd out_state s2) (fst (negBExp (b,ba))) in (* compute 'out' state for else-block *) + let out_if = bwd_filter ?domain:pre_dom (bwd out_state s1) b in (* compute 'out' state for if-block*) + let out_else = bwd_filter ?domain:pre_dom (bwd out_state s2) (fst (negBExp (b,ba))) in (* compute 'out' state for else-block *) D.mask current_in (branch_join out_if out_else) (* join the two branches and combine with current 'in' state using mask *) | A_while (l,(b,ba),loop_body) -> - let out_exit = bwd_filter out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *) + let pre_dom = if !refine then Some (fwdInv l) else None in + let out_exit = bwd_filter ?domain:pre_dom out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *) let rec aux (* recursive function that iteratively computes fixed point for 'in' state at loop head *) (current_in:D.t) (* 'in' state of the previous iteration *) (out_enter:D.t) (* current 'out' state when entering the loop body *) @@ -337,11 +362,11 @@ module CTLIterator(D: RANKING_FUNCTION) = struct if n <= !joinbwd then updated_in (* widening threshold not yet reached *) else D.dual_widen current_in updated_in (* use dual_widen after widening threshold reached *) in - let out_enter' = bwd_filter (bwd updated_in' loop_body) b in (* process loop body again with updated 'in' state *) + let out_enter' = bwd_filter ?domain:pre_dom (bwd updated_in' loop_body) b in (* process loop body again with updated 'in' state *) (* next iteration *) aux updated_in' out_enter' (n+1) in - let initial_out_enter = bwd_filter (bwd current_in loop_body) b in (* process loop body with current 'in' state at loop-head *) + let initial_out_enter = bwd_filter ?domain:pre_dom (bwd current_in loop_body) b in (* process loop body with current 'in' state at loop-head *) let final_in_state = aux current_in initial_out_enter 1 in (* compute fixed point for while-loop starting with current 'in' state at loop-head *) addInv l final_in_state | A_call (f,ss) -> raise (Invalid_argument "bwdStm:A_call") @@ -397,8 +422,6 @@ module CTLIterator(D: RANKING_FUNCTION) = struct aux program.mainFunction.funcBody bot (); let zero_leafs t = D.until t top t in (* set all defined leafs of the decision trees to zero *) InvMap.map zero_leafs !invMap - - (* Assign atomic state to those blocks that match the label and bot to all others *) @@ -534,6 +557,7 @@ module CTLIterator(D: RANKING_FUNCTION) = struct let inv = compute program property in let initialLabel = block_label program.mainFunction.funcBody in let programInvariant = InvMap.find initialLabel inv in + tree := (D.output_json program.variables programInvariant); D.defined ?condition:precondition programInvariant diff --git a/main/ForwardIterator.ml b/main/ForwardIterator.ml index e97e250..1ed2d0c 100644 --- a/main/ForwardIterator.ml +++ b/main/ForwardIterator.ml @@ -7,7 +7,7 @@ open AbstractSyntax open InvMap open Apron open Functions -open Iterator +open Config open Domain open Partition diff --git a/main/GuaranteeIterator.ml b/main/GuaranteeIterator.ml index 57c4ed4..4069edf 100644 --- a/main/GuaranteeIterator.ml +++ b/main/GuaranteeIterator.ml @@ -9,7 +9,7 @@ open ForwardIterator open Apron open Domain open Functions -open Iterator +open Config module GuaranteeIterator (D: RANKING_FUNCTION) = struct @@ -149,6 +149,7 @@ struct Format.fprintf !fmt "\nBackward Analysis:\n"; bwdMap_print !fmt !bwdInvMap; end; + tree := (D.output_json vars i); D.defined ~condition:precondition i end diff --git a/main/Main.ml b/main/Main.ml index b3b4cb2..b51fda8 100644 --- a/main/Main.ml +++ b/main/Main.ml @@ -10,17 +10,7 @@ (* parsing *) -let analysis = ref "termination" -let domain = ref "boxes" -let filename = ref "" -let fmt = ref Format.std_formatter -let main = ref "main" -let minimal = ref false -let ordinals = ref false -let property = ref "" -let precondition = ref "true" -let time = ref false -let noinline = ref false +open Config let parseFile filename = let f = open_in filename in @@ -134,28 +124,28 @@ let parse_args () = | "-domain"::x::r -> (* abstract domain: boxes|octagons|polyhedra *) domain := x; doit r | "-timeout"::x::r -> (* analysis timeout *) - Iterator.timeout := float_of_string x; doit r + timeout := float_of_string x; doit r | "-joinfwd"::x::r -> (* widening delay in forward analysis *) - Iterator.joinfwd := int_of_string x; doit r + joinfwd := int_of_string x; doit r | "-joinbwd"::x::r -> (* widening delay in backward analysis *) - Iterator.joinbwd := int_of_string x; doit r + joinbwd := int_of_string x; doit r | "-main"::x::r -> (* analyzer entry point *) main := x; doit r | "-meetbwd"::x::r -> (* dual widening delay in backward analysis *) - Iterator.meetbwd := int_of_string x; doit r + meetbwd := int_of_string x; doit r | "-minimal"::r -> (* analysis result only *) - minimal := true; Iterator.minimal := true; doit r + minimal := true; minimal := true; doit r | "-ordinals"::x::r -> (* ordinal-valued ranking functions *) ordinals := true; Ordinals.max := int_of_string x; doit r | "-refine"::r -> (* refine in backward analysis *) - Iterator.refine := true; doit r + refine := true; doit r | "-retrybwd"::x::r -> - Iterator.retrybwd := int_of_string x; + retrybwd := int_of_string x; DecisionTree.retrybwd := int_of_string x; doit r | "-tracefwd"::r -> (* forward analysis trace *) - Iterator.tracefwd := true; doit r + tracefwd := true; doit r | "-tracebwd"::r -> (* backward analysis trace *) - Iterator.tracebwd := true; + tracebwd := true; DecisionTree.tracebwd := true; CFGInterpreter.trace := true; CFGInterpreter.trace_states := true; @@ -171,26 +161,32 @@ let parse_args () = | "-time"::r -> (* track analysis time *) time := true; doit r | "-timefwd"::r -> (* track forward analysis time *) - Iterator.timefwd := true; doit r + timefwd := true; doit r | "-timebwd"::r -> (* track backward analysis time *) - Iterator.timebwd := true; doit r + timebwd := true; doit r (* CTL arguments ---------------------------------------------------------*) | "-ctl"::x::r -> (* CTL analysis *) analysis := "ctl"; property := x; doit r | "-ctl-ast"::x::r -> (* CTL analysis *) - analysis := "ctl-ast"; property := x; doit r + analysis := "ctl"; ctltype:="AST"; property := x; doit r | "-ctl-cfg"::x::r -> (* CTL analysis *) - analysis := "ctl-cfg"; property := x; doit r + analysis := "ctl"; ctltype:="CFG"; property := x; doit r | "-dot"::r -> (* print CFG and decision trees in 'dot' format *) - Iterator.dot := true; doit r + dot := true; doit r | "-precondition"::c::r -> (* optional precondition that holds at the start of the program, default = true *) precondition := c; doit r | "-ctl_existential_equivalence"::r -> (* use CTL equivalence relations to convert existential to universal CTL properties *) - Iterator.ctl_existential_equivalence := true; doit r + ctl_existential_equivalence := true; doit r | "-noinline"::r -> (* don't inline function calls, only for CFG based analysis *) noinline := true; doit r + | "-output_std"::r -> + output_std := true; doit r + | "-json_output"::x::r when x <> "-output_std"-> + json_output := true; output_dir :=x; output_dir :=x; time:=true; doit r + | "-json_output"::r -> (* guarantee analysis *) + json_output := true; time:=true; doit r | x::r -> filename := x; doit r | [] -> () in @@ -257,15 +253,17 @@ let run_analysis analysis_function program () = try let start = Sys.time () in let terminating = analysis_function program !main in + Config.result := terminating; let stop = Sys.time () in Format.fprintf !fmt "Analysis Result: "; let result = if terminating then "TRUE" else "UNKNOWN" in Format.fprintf !fmt "%s\n" result; if !time then + exectime := string_of_float (stop -. start); Format.fprintf !fmt "Time: %f s\n" (stop-.start); Format.fprintf !fmt "\nDone.\n" with - | Iterator.Timeout -> + | Timeout -> Format.fprintf !fmt "\nThe Analysis Timed Out!\n"; Format.fprintf !fmt "\nDone.\n" @@ -375,8 +373,10 @@ let ctl_ast () = | _ -> raise (Invalid_argument "Unknown Abstract Domain") in let result = analyze ~precondition:precondition program property in + Config.result := result; if !time then begin let stoptime = Sys.time () in + exectime := string_of_float (stoptime-.starttime); Format.fprintf !fmt "\nTime: %f" (stoptime-.starttime) end; if result then @@ -409,7 +409,7 @@ let ctl_cfg () = Printf.printf "%a" Cfg_printer.print_cfg cfg; Printf.printf "\n"; end; - if not !minimal && !Iterator.dot then + if not !minimal && !dot then begin Printf.printf "CFG_DOT:\n %a" Cfg_printer.output_dot cfg; Printf.printf "\n"; @@ -418,8 +418,10 @@ let ctl_cfg () = let possibleLoopHeads = Loop_detection.possible_loop_heads cfg mainFunc in let domSets = Loop_detection.dominator cfg mainFunc in let result = analyze ~precondition:precondition cfg mainFunc possibleLoopHeads domSets ctlProperty in + Config.result := result; if !time then begin let stoptime = Sys.time () in + exectime := string_of_float (stoptime-.starttime); Format.fprintf !fmt "\nTime: %f" (stoptime-.starttime) end; if result then @@ -429,13 +431,35 @@ let ctl_cfg () = let doit () = parse_args (); + if !json_output then + begin + Regression.create_logfile_name (); + (* Open the log file *) + f_log := Out_channel.open_bin !logfile; + (* Set the formatter to logfile*) + fmt := Format.formatter_of_out_channel !f_log + end + ; + let _ = match !analysis with | "termination" -> termination () | "guarantee" -> guarantee () | "recurrence" -> recurrence () - | "ctl" -> ctl_ast () (* default CTL analysis is CTL-AST *) - | "ctl-ast" -> ctl_ast () - | "ctl-cfg" -> ctl_cfg () + | "ctl" -> ctl_ast (); analysis:= "ctl" (* default CTL analysis is CTL-AST *) + | "ctl-ast" when !ctltype = "AST" -> ctl_ast (); (* default CTL analysis is CTL-AST *) + | "ctl-cfg" when !ctltype = "CFG" -> ctl_cfg (); (* default CTL analysis is CTL-AST *) | _ -> raise (Invalid_argument "Unknown Analysis") - + in + if !json_output then + begin + Out_channel.close !f_log; + Regression.output_json () + end + ; + (* Get the log to ouput them on std output *) + if !output_std && !json_output then + let f_log = In_channel.open_bin !logfile in + let s = In_channel.input_all f_log in + Printf.printf "%s" s + let _ = doit () diff --git a/main/RecurrenceIterator.ml b/main/RecurrenceIterator.ml index f2dbb2e..dafb5ed 100644 --- a/main/RecurrenceIterator.ml +++ b/main/RecurrenceIterator.ml @@ -9,7 +9,7 @@ open InvMap open Apron open Domain open Functions -open Iterator +open Config module RecurrenceIterator (D: RANKING_FUNCTION) = struct @@ -185,6 +185,7 @@ struct Format.fprintf !fmt "\nBackward Analysis:\n"; bwdMap_print !fmt !bwdInvMap; end; + tree := (D.output_json vars i); D.defined ~condition:precondition i end diff --git a/main/Regression.ml b/main/Regression.ml new file mode 100644 index 0000000..e8a61f6 --- /dev/null +++ b/main/Regression.ml @@ -0,0 +1,28 @@ +open Config + +let create_logfile_name () = + let replace = Str.regexp ("tests/[A-Za-z]+/") in + let name = Str.replace_first (replace) (!output_dir^(!analysis)^"/") (!filename) in + let name = name^"-domain"^(!domain)^(if !ordinals then "-ordinals"^(string_of_int !Ordinals.max) else "")^(if !refine then "-refine" else "")^".out" in + Config.logfile := name + +let json_string filename time analysis property domain = + Printf.sprintf {| + {"filename" : "%s", + "analysis_type": "%s", + "property": "%s", + "result": "%s", + "domain": "%s" + }|} + filename analysis property domain + +let output_json () = + let replace = Str.regexp ("tests/[A-Za-z]+/") in + let basefile = Str.replace_first (replace) ((!output_dir)^(!analysis)^"/") (!filename) in + let basefile = basefile^"-domain"^(!domain)^(if !ordinals then "-ordinals"^(string_of_int !Ordinals.max) else "")^(if !refine then "-refine" else "") in + let jsonfile = basefile^".json" in + let output = json_string !filename time !analysis !property (if !Config.result then "TRUE" else "UKNOWN") !domain in + let json : Yojson.Safe.t = `Assoc(("Config",Yojson.Safe.from_string output)::[("tree", !tree)]) in + let f = Out_channel.open_bin (jsonfile) in + Yojson.Safe.pretty_to_channel f json; + Out_channel.close f \ No newline at end of file diff --git a/main/TerminationIterator.ml b/main/TerminationIterator.ml index 116c7e5..a3e629b 100644 --- a/main/TerminationIterator.ml +++ b/main/TerminationIterator.ml @@ -13,7 +13,7 @@ open InvMap open Apron open Domain open Functions -open Iterator +open Config open AbstractSyntax module TerminationIterator (D: RANKING_FUNCTION) = @@ -307,6 +307,7 @@ struct Format.fprintf !fmt "\nBackward Analysis:\n"; bwdMap_print !fmt !bwdInvMap; end; + tree := (D.output_json vars i); D.defined ~condition:precondition i end diff --git a/main/dune b/main/dune index 3b2ccb7..f17d1d5 100644 --- a/main/dune +++ b/main/dune @@ -6,7 +6,7 @@ (into ..)) (flags (:standard -open Frontend -open Domains -open Cfgfrontend -open Utils)) - (libraries frontend cfgfrontend utils domains)) + (libraries yojson frontend cfgfrontend utils domains str)) (env (dev diff --git a/main/Iterator.ml b/utils/Config.ml similarity index 51% rename from main/Iterator.ml rename to utils/Config.ml index d2e2110..abd84f7 100644 --- a/main/Iterator.ml +++ b/utils/Config.ml @@ -1,13 +1,3 @@ -(* - ********* Forward/Backward Iterator ************ - Copyright (C) 2012-2014 by Caterina Urban. All rights reserved. -*) - -let abort = ref false -let cda = ref false (* conflict-driven conditional termination *) -let compress = ref true (* false *) -let ctl_existential_equivalence = ref false (* use logical equivalences to express existential CTL properties based on universal properties *) -let fmt = ref Format.std_formatter let joinbwd = ref 2 let joinfwd = ref 2 let learn = ref false (* conflict-driven conditional termination *) @@ -15,15 +5,41 @@ let meetbwd = ref 2 let minimal = ref false let refine = ref false let retrybwd = ref 5 +let analysis = ref "termination" +let domain = ref "boxes" +let filename = ref "" +let fmt = ref Format.std_formatter +let main = ref "main" +let minimal = ref false +let compress = ref true (* false *) +let ordinals = ref false +let property = ref "" +let precondition = ref "true" +let time = ref false +let noinline = ref false let size = ref 2 (* conflict-driven conditional termination *) let start = ref 0.0 let stop = ref 0.0 let timebwd = ref false let timefwd = ref false +let fmt = ref Format.std_formatter let timeout = ref 300.0 +let ctl_existential_equivalence = ref false let tracefwd = ref false let tracebwd = ref false let dot = ref false (* output trees in graphviz dot format *) +let abort = ref false +let json_output = ref false +let output_dir = ref "logs/" +let exectime = ref "0" +let ctltype = ref "" +let logfile = ref "" +let result = ref false +let output_std = ref false +let f_log = ref Out_channel.stdout +let tree: Yojson.Safe.t ref = ref `Null exception Abort exception Timeout + + diff --git a/utils/dune b/utils/dune index 6c9bc85..e0a2252 100644 --- a/utils/dune +++ b/utils/dune @@ -1,6 +1,6 @@ (library (name utils) - (libraries frontend) + (libraries frontend yojson) (flags (:standard -open Frontend)))