diff --git a/banal/banal_apron_domain.ml b/banal/banal_apron_domain.ml index 6dbe6348..616aeec5 100644 --- a/banal/banal_apron_domain.ml +++ b/banal/banal_apron_domain.ml @@ -22,13 +22,17 @@ module Lin = Linearization.Make (Itv_rat) module ApronDomain (Param : Banal_apron_utils.APRON_PARAM) = struct module U = Banal_apron_utils.Make (Param) (Itv_rat) + let man = Param.manager type t = Param.lib Abstract1.t + let top_apron env = Abstract1.top man env + let bot_apron env = Abstract1.bottom man env + let of_apron v env = Abstract1.join man v (bot_apron env) - + (*************) (* UTILITIES *) (*************) @@ -296,7 +300,7 @@ module ApronDomain (Param : Banal_apron_utils.APRON_PARAM) = struct (* for each constraint oldc in a *) for i = 0 to Lincons1.array_length ar - 1 do let oldc = Lincons1.array_get ar i in - if c <> oldc then ( + if lincons1_cmp c oldc = 0 then ( (* try to replace oldc with c *) Lincons1.array_set ar i c ; let aa = Abstract1.of_lincons_array man env ar in @@ -309,7 +313,7 @@ module ApronDomain (Param : Banal_apron_utils.APRON_PARAM) = struct (pool @ [c]) ; (* now, remove c *) let l = list_of_lincons_array ar in - let ll = List.filter (fun cc -> c <> cc) l in + let ll = List.filter (fun cc -> lincons1_cmp c cc = 0) l in if trace_remove && List.length l <> List.length ll then Format.printf "### remove_constraint remove: %a ###@\n" Lincons1.print c ; @@ -354,8 +358,7 @@ module ApronDomain (Param : Banal_apron_utils.APRON_PARAM) = struct (* this is required to analyze preciselw bwd_loop7! *) (* TODO: better heuristic to find which ray to add *) if - Linexpr0.compare ea - g.Generator1.generator0.Generator0.linexpr0 + Linexpr0.cmp ea g.Generator1.generator0.Generator0.linexpr0 = 0 then acc else @@ -560,26 +563,26 @@ module ApronDomain (Param : Banal_apron_utils.APRON_PARAM) = struct stroke-width='1px'/>\n" (xx 0.) 0 (xx 0.) h ; ( if svg_grid then - let c = ref scale in - while !c <= x1 do - Printf.fprintf ch - "\n" - 0 (yy !c) w (yy !c) ; - Printf.fprintf ch - "\n" - 0 (yy (-. !c)) w (yy (-. !c)) ; - Printf.fprintf ch - "\n" - (xx !c) 0 (xx !c) h ; - Printf.fprintf ch - "\n" - (xx (-. !c)) 0 (xx (-. !c)) h ; - c := !c +. scale - done ) ; + let c = ref scale in + while !c <= x1 do + Printf.fprintf ch + "\n" + 0 (yy !c) w (yy !c) ; + Printf.fprintf ch + "\n" + 0 (yy (-. !c)) w (yy (-. !c)) ; + Printf.fprintf ch + "\n" + (xx !c) 0 (xx !c) h ; + Printf.fprintf ch + "\n" + (xx (-. !c)) 0 (xx (-. !c)) h ; + c := !c +. scale + done ) ; text (float_of_int (w - 10)) (yy 0. -. 4.) "end" "gray" x.var_name ; text (xx 0. +. 4.) 10. "start" "gray" y.var_name ; (* output constraints *) @@ -964,38 +967,43 @@ module ApronDomain (Param : Banal_apron_utils.APRON_PARAM) = struct in bwd_trace "meet" (Abstract1.meet man pre) post - let bwd_join ((_,vset) as post1: t * VSet.t) (post2 : t * VSet.t) ((pre,_) : t * VSet.t) = - - let lift_vset2 f (a,v) (b,_) = f a b, v in - lift_vset2 (fun post1 post2 -> - (* check if one element is contained in the other *) - if Abstract1.is_leq man post1 post2 then post2 else - if Abstract1.is_leq man post2 post1 then post1 else - - (* HEURISTIC -> perform the refinement only if the result has some "reasonable" - directions, namely the ones of the `pre` and `post{1,2}` (in both polarities). *) - let allowed_dirs = U.get_directions pre @ U.get_directions post1 @ U.get_directions post2 in - let check_dirs a = - let dirs = U.get_directions a in - List.for_all (fun d1 -> List.exists (fun d2 -> d1 = d2 || U.neg_linexpr d2 = d1) allowed_dirs) dirs - in - - (* try refinement of poly with singleton components differing by +-1 *) - match U.refine_singleton vset post1 post2 with - | Some post1 when check_dirs post1 -> post1 - | _ -> - - (* try refinement of poly by adding behind some constraint *) - match U.refine_behind_cons vset post1 post2 with - | Some post1 when check_dirs post1 -> post1 - | _ -> - - (* refinemenet failed.. *) - post1 - - ) post1 post2 - - + let bwd_join ((_, vset) as post1 : t * VSet.t) (post2 : t * VSet.t) + ((pre, _) : t * VSet.t) = + let lift_vset2 f (a, v) (b, _) = (f a b, v) in + lift_vset2 + (fun post1 post2 -> + (* check if one element is contained in the other *) + if Abstract1.is_leq man post1 post2 then post2 + else if Abstract1.is_leq man post2 post1 then post1 + else + (* HEURISTIC -> perform the refinement only if the result has some + "reasonable" directions, namely the ones of the `pre` and + `post{1,2}` (in both polarities). *) + let allowed_dirs = + U.get_directions pre @ U.get_directions post1 + @ U.get_directions post2 + in + let check_dirs a = + let dirs = U.get_directions a in + List.for_all + (fun d1 -> + List.exists + (fun d2 -> d1 = d2 || U.neg_linexpr d2 = d1) + allowed_dirs ) + dirs + in + (* try refinement of poly with singleton components differing by + +-1 *) + match U.refine_singleton vset post1 post2 with + | Some post1 when check_dirs post1 -> post1 + | _ -> ( + (* try refinement of poly by adding behind some constraint *) + match U.refine_behind_cons vset post1 post2 with + | Some post1 when check_dirs post1 -> post1 + | _ -> + (* refinemenet failed.. *) + post1 ) ) + post1 post2 end (* INSTANTIATIONS *) diff --git a/banal/banal_apron_utils.ml b/banal/banal_apron_utils.ml index 145aff09..42f88b31 100644 --- a/banal/banal_apron_utils.ml +++ b/banal/banal_apron_utils.ml @@ -10,9 +10,11 @@ module type APRON_PARAM = sig val manager : lib Manager.t end -module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct +module Make (Param : APRON_PARAM) (Itv : INTERVAL) = struct module Lin = Banal_linearization.Make (Itv) + type t = Param.lib Abstract1.t + let man = Param.manager (* To/from APRON types *) @@ -24,29 +26,32 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let add_var_to_env env v = let i, r = match v.var_typ with - | A_int _ | A_BOOL -> ([| apron_of_var v |], [||]) - | A_float _ -> ([||], [| apron_of_var v |]) + | A_int _ | A_BOOL -> ([|apron_of_var v|], [||]) + | A_float _ -> ([||], [|apron_of_var v|]) in Environment.add env i r (* linear expressions *) let lin_of_blin env ((i, m) : Lin.linexpr) : Linexpr1.t = let r = Linexpr1.make env in - Linexpr1.set_cst r (Coeff.Interval (Lin.I.to_apron i)); + Linexpr1.set_cst r (Coeff.Interval (Lin.I.to_apron i)) ; Lin.VMap.iter (fun v i -> Linexpr1.set_coeff r (apron_of_var v) - (Coeff.Interval (Lin.I.to_apron i))) - m; + (Coeff.Interval (Lin.I.to_apron i)) ) + m ; r - let blin_of_lin (vset: VSet.t) (le: Linexpr1.t) : Lin.linexpr = + let blin_of_lin (vset : VSet.t) (le : Linexpr1.t) : Lin.linexpr = let cst = Linexpr1.get_cst le |> Lin.I.of_coeff in - let vmap = VSet.to_seq vset - |> Seq.map (fun v -> v, apron_of_var v) - |> Seq.map (fun (v,av) -> v, Linexpr1.get_coeff le av |> Lin.I.of_coeff) + let vmap = + VSet.to_seq vset + |> Seq.map (fun v -> (v, apron_of_var v)) + |> Seq.map (fun (v, av) -> + (v, Linexpr1.get_coeff le av |> Lin.I.of_coeff) ) |> Lin.VMap.of_seq - in cst,vmap + in + (cst, vmap) (* linear constraints *) let cons_op_of_bcons_op = function @@ -60,8 +65,7 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let lincons_array_of_lincons env (c : Lincons1.t) : Lincons1.earray = let a = Lincons1.array_make env 1 in - Lincons1.array_set a 0 c; - a + Lincons1.array_set a 0 c ; a let lincons_array_of_blincons env (c : Lin.lincons) : Lincons1.earray = lincons_array_of_lincons env (lincons_of_blincons env c) @@ -76,29 +80,30 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct (* negate a linexpr *) let neg_linexpr (e : Linexpr1.t) : Linexpr1.t = let e = Linexpr1.copy e in - Linexpr1.set_cst e (Coeff.neg (Linexpr1.get_cst e)); - Linexpr1.iter (fun c v -> Linexpr1.set_coeff e v (Coeff.neg c)) e; + Linexpr1.set_cst e (Coeff.neg (Linexpr1.get_cst e)) ; + Linexpr1.iter (fun c v -> Linexpr1.set_coeff e v (Coeff.neg c)) e ; e (* constructs a new contraint in opposite direction *) let neg_lincons (d : Lincons1.t) : Lincons1.t = - Lincons1.make (Lincons1.get_linexpr1 d |> neg_linexpr) (Lincons1.get_typ d) + Lincons1.make + (Lincons1.get_linexpr1 d |> neg_linexpr) + (Lincons1.get_typ d) (* normalize equalities as pairs of inequalities *) - let normalize_lincons (d:Lincons1.t) : Lincons1.t list = + let normalize_lincons (d : Lincons1.t) : Lincons1.t list = match Lincons1.get_typ d with | Lincons1.EQ -> - Lincons1.set_typ d Lincons1.SUPEQ; + Lincons1.set_typ d Lincons1.SUPEQ ; [d; neg_lincons d] - | DISEQ - | EQMOD _ -> failwith (__LOC__^": unexpected lincons kind") + | DISEQ | EQMOD _ -> failwith (__LOC__ ^ ": unexpected lincons kind") | _ -> [d] - let seq_of_lincons_array (ar: Lincons1.earray) : Lincons1.t Seq.t = + let seq_of_lincons_array (ar : Lincons1.earray) : Lincons1.t Seq.t = Seq.ints 0 - |> Seq.take (Lincons1.array_length ar) - |> Seq.map (fun i -> Lincons1.array_get ar i) - |> Seq.flat_map (fun c -> normalize_lincons c |> List.to_seq) + |> Seq.take (Lincons1.array_length ar) + |> Seq.map (fun i -> Lincons1.array_get ar i) + |> Seq.flat_map (fun c -> normalize_lincons c |> List.to_seq) let list_of_lincons_array (ar : Lincons1.earray) : Lincons1.t list = seq_of_lincons_array ar |> List.of_seq @@ -108,9 +113,9 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let i = ref 0 in List.iter (fun c -> - Lincons1.array_set ar !i c; - incr i) - l; + Lincons1.array_set ar !i c ; + incr i ) + l ; ar let array_of_lincons_seq env (s : Lincons1.t Seq.t) : Lincons1.earray = @@ -118,9 +123,9 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let i = ref 0 in Seq.iter (fun c -> - Lincons1.array_set ar !i c; - incr i) - s; + Lincons1.array_set ar !i c ; + incr i ) + s ; ar let lincons_list_of_abs (a : t) : Lincons1.t list = @@ -133,46 +138,45 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct array_of_lincons_list (Abstract1.env a) (lincons_list_of_abs a) let safe_abs_of_lincons_array env (l : Lincons1.earray) = - (* Workaround a bug in APRON which causes a segfault when a a constraint of - the form `lin_expr +- inf >= 0` is converted into an abstract value. + (* Workaround a bug in APRON which causes a segfault when a a constraint + of the form `lin_expr +- inf >= 0` is converted into an abstract + value. Workaround also an imprecision in APRON which returns top as the - abstract element corresponding to the constraints `x-inf>=0`. - *) - + abstract element corresponding to the constraints `x-inf>=0`. *) let s_inf = Coeff.(Scalar (Scalar.of_infty 1)) in - let i_inf = Coeff.(Interval {inf=Scalar.of_infty 1;sup=Scalar.of_infty 1}) in + let i_inf = + Coeff.(Interval {inf= Scalar.of_infty 1; sup= Scalar.of_infty 1}) + in let s_minf = Coeff.(Scalar (Scalar.of_infty (-1))) in - let i_minf = Coeff.(Interval {inf=Scalar.of_infty (-1);sup=Scalar.of_infty (-1)}) in - - for i=0 to Lincons1.array_length l - 1 do + let i_minf = + Coeff.(Interval {inf= Scalar.of_infty (-1); sup= Scalar.of_infty (-1)}) + in + for i = 0 to Lincons1.array_length l - 1 do let cons = Lincons1.array_get l i in - - (* ensure that all the coefficients of the variables are not infinite *) - let all_finite = Array.to_seq (fst (Environment.vars env)) + (* ensure that all the coefficients of the variables are not + infinite *) + let all_finite = + Array.to_seq (fst (Environment.vars env)) |> Seq.interleave (Array.to_seq (snd (Environment.vars env))) |> Seq.for_all (fun v -> - match Lincons1.get_coeff cons v with - | Scalar s -> Scalar.is_infty s = 0 - | Interval {inf; sup} -> Scalar.is_infty inf = 0 && Scalar.is_infty sup = 0 - ) - in assert all_finite; - + match Lincons1.get_coeff cons v with + | Scalar s -> Scalar.is_infty s = 0 + | Interval {inf; sup} -> + Scalar.is_infty inf = 0 && Scalar.is_infty sup = 0 ) + in + assert all_finite ; let cst = Lincons1.get_cst cons in - - if Coeff.equal s_inf cst || Coeff.equal i_inf cst then begin + if Coeff.equal s_inf cst || Coeff.equal i_inf cst then (* inf >= 0 is always true, replace it with 0 >= 0 *) - Lincons1.array_set l i (Lincons1.make (Linexpr1.make env) Lincons1.SUPEQ); - end; - - if Coeff.equal s_minf cst || Coeff.equal i_minf cst then begin + Lincons1.array_set l i + (Lincons1.make (Linexpr1.make env) Lincons1.SUPEQ) ; + if Coeff.equal s_minf cst || Coeff.equal i_minf cst then ( (* minf >= 0 is never true, replace it with -1 >= 0 *) let le = Linexpr1.make env in - Linexpr1.set_cst le (Coeff.Scalar (Scalar.of_int (-1))); - Lincons1.array_set l i (Lincons1.make le Lincons1.SUPEQ); - end - done; - + Linexpr1.set_cst le (Coeff.Scalar (Scalar.of_int (-1))) ; + Lincons1.array_set l i (Lincons1.make le Lincons1.SUPEQ) ) + done ; Abstract1.of_lincons_array man env l (* construct abstract element from constraint list *) @@ -184,12 +188,12 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct safe_abs_of_lincons_array env (array_of_lincons_seq env l) (* construct an abstract element from a constraint *) - let abs_of_lincons env (c: Lincons1.t) : t = + let abs_of_lincons env (c : Lincons1.t) : t = let ar = Lincons1.array_make env 1 in - Lincons1.array_set ar 0 c; + Lincons1.array_set ar 0 c ; safe_abs_of_lincons_array env ar - let abs_of_blincons env (c: Lin.lincons) : t = + let abs_of_blincons env (c : Lin.lincons) : t = abs_of_lincons env (lincons_of_blincons env c) (* Generators construction/extraction and normalization *) @@ -197,23 +201,23 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct (* constructs a new generator in opposite direction *) let neg_generator (g : Generator1.t) : Generator1.t = - Generator1.make (Generator1.get_linexpr1 g |> neg_linexpr) (Generator1.get_typ g) + Generator1.make + (Generator1.get_linexpr1 g |> neg_linexpr) + (Generator1.get_typ g) - (* normalize generators. Vertexs and rays are left unmodified, - lines are converted into a pair of rays (thus the output is - a list) - *) + (* normalize generators. Vertexs and rays are left unmodified, lines are + converted into a pair of rays (thus the output is a list) *) let normalize_gen (g : Generator1.t) : Generator1.t list = match Generator1.get_typ g with | Generator1.LINE -> let g = Generator1.copy g in - Generator1.set_typ g Generator1.RAY; - [ g; neg_generator g ] + Generator1.set_typ g Generator1.RAY ; + [g; neg_generator g] | Generator1.LINEMOD -> let g = Generator1.copy g in - Generator1.set_typ g Generator1.RAYMOD; - [ g; neg_generator g ] - | _ -> [ g ] + Generator1.set_typ g Generator1.RAYMOD ; + [g; neg_generator g] + | _ -> [g] (* normalize lines as pairs of rays *) let list_of_generator_array (ar : Generator1.earray) : Generator1.t list = @@ -221,52 +225,54 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct for i = 0 to Generator1.array_length ar - 1 do let d = Generator1.array_get ar i in l := normalize_gen d @ !l - done; + done ; !l (* generator list -> generator array *) - let array_of_generator_list env (l : Generator1.t list) : Generator1.earray = + let array_of_generator_list env (l : Generator1.t list) : Generator1.earray + = let ar = Generator1.array_make env (List.length l) in let i = ref 0 in List.iter (fun c -> - Generator1.array_set ar !i c; - incr i) - l; + Generator1.array_set ar !i c ; + incr i ) + l ; ar (* normalized constraint list from abstract element *) let generator_seq_of_abs (a : t) : Generator1.t Seq.t = let ar = Abstract1.to_generator_array man a in Seq.ints 0 - |> Seq.take (Generator1.array_length ar) - |> Seq.map (fun i -> Generator1.array_get ar i) - |> Seq.flat_map (fun g -> normalize_gen g |> List.to_seq) + |> Seq.take (Generator1.array_length ar) + |> Seq.map (fun i -> Generator1.array_get ar i) + |> Seq.flat_map (fun g -> normalize_gen g |> List.to_seq) let generator_list_of_abs (a : t) : Generator1.t list = list_of_generator_array (Abstract1.to_generator_array man a) - let vertex_seq_of_abs (a:t) : Generator1.t Seq.t = + let vertex_seq_of_abs (a : t) : Generator1.t Seq.t = generator_seq_of_abs a - |> Seq.filter (fun g -> Generator1.get_typ g = VERTEX) + |> Seq.filter (fun g -> Generator1.get_typ g = VERTEX) - let vertex_list_of_abs (a:t) : Generator1.t list = + let vertex_list_of_abs (a : t) : Generator1.t list = List.of_seq (vertex_seq_of_abs a) - let ray_seq_of_abs (a:t) : Generator1.t Seq.t = + let ray_seq_of_abs (a : t) : Generator1.t Seq.t = generator_seq_of_abs a - |> Seq.filter (fun g -> Generator1.get_typ g = RAY || Generator1.get_typ g = RAYMOD) + |> Seq.filter (fun g -> + Generator1.get_typ g = RAY || Generator1.get_typ g = RAYMOD ) - let ray_list_of_abs (a:t) : Generator1.t list = + let ray_list_of_abs (a : t) : Generator1.t list = List.of_seq (ray_seq_of_abs a) (* Modifiers *) (* ********* *) - let meet_lincons env (a:t) (c:Lincons1.t) : t = + let meet_lincons env (a : t) (c : Lincons1.t) : t = Abstract1.meet_lincons_array man a (lincons_array_of_lincons env c) - let meet_blincons env (a:t) (c:Lin.lincons) : t = + let meet_blincons env (a : t) (c : Lin.lincons) : t = Abstract1.meet_lincons_array man a (lincons_array_of_blincons env c) (* similar to add_ray, but also works for vertices *) @@ -277,7 +283,7 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct List.fold_left (fun (v, r) g -> if Generator1.get_typ g = Generator1.VERTEX then (g :: v, r) - else (v, g :: r)) + else (v, g :: r) ) ([], []) g in (* add vertices *) @@ -289,39 +295,46 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let vals = Array.init (Array.length vars) (fun i -> let le = Linexpr1.make env in - Linexpr1.set_cst le (Generator1.get_coeff g vars.(i)); - le) + Linexpr1.set_cst le (Generator1.get_coeff g vars.(i)) ; + le ) in - - (* Note: use `assign_linexpr` as `of_box` does not work with fractionary coordinates. *) - let vtx = Abstract1.assign_linexpr_array man (Abstract1.top man env) vars vals None in - Abstract1.join man a vtx) + (* Note: use `assign_linexpr` as `of_box` does not work with + fractionary coordinates. *) + let vtx = + Abstract1.assign_linexpr_array man (Abstract1.top man env) vars + vals None + in + Abstract1.join man a vtx ) a vs in (* add rays *) if rs = [] || Abstract1.is_bottom man a then a else Abstract1.add_ray_array man a (array_of_generator_list env rs) - let abs_of_generators_list (env: Environment.t) (g: Generator1.t list) : t = + let abs_of_generators_list (env : Environment.t) (g : Generator1.t list) : + t = add_generators (Abstract1.bottom man env) g - (* try to remove a constraint. returns `Some a` if the contraint was removed, - `None` otherwise *) - let remove_lincons (c:Lincons1.t) (a:t) : t option = - let lincons_list, found = lincons_seq_of_abs a - |> Seq.fold_left (fun (acc_lst, found) cc -> - if c = cc then acc_lst, true else cc::acc_lst, found - ) - ([], false) - in if found then Some (abs_of_lincons_list (Abstract1.env a) lincons_list) else None - - let remove_blincons (c:Lin.lincons) (a:t) : t option = + (* try to remove a constraint. returns `Some a` if the contraint was + removed, `None` otherwise *) + let remove_lincons (c : Lincons1.t) (a : t) : t option = + let lincons_list, found = + lincons_seq_of_abs a + |> Seq.fold_left + (fun (acc_lst, found) cc -> + if c = cc then (acc_lst, true) else (cc :: acc_lst, found) ) + ([], false) + in + if found then Some (abs_of_lincons_list (Abstract1.env a) lincons_list) + else None + + let remove_blincons (c : Lin.lincons) (a : t) : t option = remove_lincons (lincons_of_blincons (Abstract1.env a) c) a - (* first try to replace constraints in a with those in pool (or c), - then remove the contraint c - *) - let remove_lincons_and_harmonize (a : t) (pool : Lincons1.t list) (c : Lin.lincons) : t = + (* first try to replace constraints in a with those in pool (or c), then + remove the contraint c *) + let remove_lincons_and_harmonize (a : t) (pool : Lincons1.t list) + (c : Lin.lincons) : t = let env = Abstract1.env a in let c = lincons_of_blincons env c in let ar = lincons_array_of_abs a in @@ -331,20 +344,20 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct (* for each constraint oldc in a *) for i = 0 to Lincons1.array_length ar - 1 do let oldc = Lincons1.array_get ar i in - if c <> oldc then ( + if lincons1_cmp c oldc = 0 then ( (* try to replace oldc with c *) - Lincons1.array_set ar i c; + Lincons1.array_set ar i c ; let aa = safe_abs_of_lincons_array env ar in - if not (Abstract1.is_eq man a aa) then Lincons1.array_set ar i oldc - ) - done) - (pool @ [ c ]); + if not (Abstract1.is_eq man a aa) then + Lincons1.array_set ar i oldc ) + done ) + (pool @ [c]) ; (* now, remove c *) let l = list_of_lincons_array ar in let ll = List.filter (fun cc -> c <> cc) l in abs_of_lincons_list env ll - (* add to a rays from dir that satisfy the constraint *) + (* add to a rays from dir that satisfy the constraint *) let add_cone (a : t) (dir : Generator1.t list) (e : Lin.linexpr) : t = (* homogenous expression *) let e = Lin.A.set_cst Lin.I.zero e in @@ -363,136 +376,152 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct (* this is required to analyze precisely bwd_loop7! *) (* TODO: better heuristic to find which ray to add *) if - Linexpr0.compare ea g.Generator1.generator0.Generator0.linexpr0 + Linexpr0.cmp ea g.Generator1.generator0.Generator0.linexpr0 = 0 then acc else (* sign of scalar product *) let x = Lin.B.sign (fst (Lin.A.eval env e)) in if x >= 0 then g :: acc else acc - | _ -> acc) + | _ -> acc ) [] dir in - (* add filtered rays *) let gar = array_of_generator_list (Abstract1.env a) rays in Abstract1.add_ray_array man a gar - (* Predicates *) (* ********** *) (* whether a contains the generator g *) let sat_generator (a : t) (g : Generator1.t) : bool = - Abstract1.is_eq man a (add_generators a [ g ]) + Abstract1.is_eq man a (add_generators a [g]) - let is_closed (a:t) : bool = + let is_closed (a : t) : bool = lincons_seq_of_abs a - |> Seq.for_all (fun c -> - match Lincons1.get_typ c with - | EQ - | SUPEQ -> true - | SUP -> false - | EQMOD _ -> failwith "unexpected EQMOD constraint" - | DISEQ -> failwith "unexpected DISEQ constraint" - ) + |> Seq.for_all (fun c -> + match Lincons1.get_typ c with + | EQ | SUPEQ -> true + | SUP -> false + | EQMOD _ -> failwith "unexpected EQMOD constraint" + | DISEQ -> failwith "unexpected DISEQ constraint" ) (* find all the generators saturating a constraint *) let gen_saturating_cons cons vset a = let le = blin_of_lin vset (Lincons1.get_linexpr1 cons) in let le_no_cst = Lin.A.set_cst Itv.zero le in - generator_seq_of_abs a - |> Seq.fold_left (fun acc g -> - let env = fun v -> Generator1.get_coeff g (apron_of_var v) |> Itv.of_coeff in - if (Generator1.get_typ g = VERTEX && Lin.A.eval env le = Itv.zero) - || Generator1.get_typ g = RAY && Lin.A.eval env le_no_cst = Itv.zero then - g::acc - else - acc - ) - [] + |> Seq.fold_left + (fun acc g -> + let env = + fun v -> Generator1.get_coeff g (apron_of_var v) |> Itv.of_coeff + in + if + (Generator1.get_typ g = VERTEX && Lin.A.eval env le = Itv.zero) + || Generator1.get_typ g = RAY + && Lin.A.eval env le_no_cst = Itv.zero + then g :: acc + else acc ) + [] (* Misc *) (* **** *) (* check if a lincons is of the form `v>=c` or `v<=c`. If it is, returns - `Some (sign, v)` where sign is `true` if `>=` or `false` if `<=`. If - the lincons has a different form, returns `None`. - *) - let lincons_single_var (vset: VSet.t) (lincons: Lincons1.t) : (bool * var) option = - let lb = VSet.fold (fun v acc -> - if Coeff.equal_int (Lincons1.get_coeff lincons (apron_of_var v)) 1 then - v::acc else acc) vset [] + `Some (sign, v)` where sign is `true` if `>=` or `false` if `<=`. If the + lincons has a different form, returns `None`. *) + let lincons_single_var (vset : VSet.t) (lincons : Lincons1.t) : + (bool * var) option = + let lb = + VSet.fold + (fun v acc -> + if Coeff.equal_int (Lincons1.get_coeff lincons (apron_of_var v)) 1 + then v :: acc + else acc ) + vset [] in - let ub = VSet.fold (fun v acc -> - if Coeff.equal_int (Lincons1.get_coeff lincons (apron_of_var v)) (-1) then - v::acc else acc) vset [] + let ub = + VSet.fold + (fun v acc -> + if + Coeff.equal_int (Lincons1.get_coeff lincons (apron_of_var v)) (-1) + then v :: acc + else acc ) + vset [] in - match lb, ub with + match (lb, ub) with | [v], [] -> Some (true, v) | [], [v] -> Some (false, v) | _ -> None (* bounds of integer variable *) - let int_var_bnds (var:var) : (Int.t * Int.t) option = - let inf, sup = match var.var_typ with - | A_int (i, s) -> Banal_semantics.int_type_set i s - | A_BOOL -> Finite Int.zero, Finite (Int.of_int 2) - | _ -> invalid_arg "bnd on a non-integer variable" + let int_var_bnds (var : var) : (Int.t * Int.t) option = + let inf, sup = + match var.var_typ with + | A_int (i, s) -> Banal_semantics.int_type_set i s + | A_BOOL -> (Finite Int.zero, Finite (Int.of_int 2)) + | _ -> invalid_arg "bnd on a non-integer variable" in - match inf, sup with - | Finite var_inf, Finite var_sup -> Some (var_inf, Int.(var_sup-var_inf+one)) + match (inf, sup) with + | Finite var_inf, Finite var_sup -> + Some (var_inf, Int.(var_sup - var_inf + one)) | _ -> None (* compute a sequence a quadrants containing the poly *) - let get_quadrants (vset: VSet.t) (a: t) : var Seq.t * Int.t VMap.t Seq.t = - if Abstract1.is_bottom man a then Seq.empty, Seq.empty else - let unbound, bound = VSet.to_seq vset - |> Seq.filter (fun v -> match v.var_typ with - | A_int _ | A_BOOL -> true - | _ -> false) - |> Seq.map (fun v -> - match int_var_bnds v with - | None -> v, Seq.return Int.zero - | Some (var_inf, var_len) -> - - let (inf,sup) = Abstract1.bound_variable man a (apron_of_var v) - |> Banal_itv_int.of_apron - in - match inf, sup with - | Finite inf, Finite sup -> - let inf_id = Int.(fdiv (inf-var_inf) var_len) in - let sup_id = Int.(fdiv (sup-var_inf) var_len) in - assert (sup_id >= inf_id); - - if Int.(sup_id - inf_id > of_int 2) then begin - v, Seq.empty - end else v, Seq.ints 0 - |> Seq.map (fun i -> Int.(of_int i + inf_id)) - |> Seq.take_while (fun i -> i <= sup_id) - | _ -> v, Seq.empty - ) - |> Seq.partition (fun (_, idxs) -> Seq.is_empty idxs) - in - let unbound = Seq.map (fun (v,_) -> v) unbound in - - (* compute the quadrant indexs *) - let rec doit seq vars = match Seq.uncons vars with - | None -> seq - | Some ((v,bnd), next) -> let seq = Seq.flat_map (fun idx -> Seq.map (fun id -> VMap.add v id idx) bnd) seq in - doit seq next - in - let idxs = doit (Seq.return VMap.empty) bound in - - unbound, idxs + let get_quadrants (vset : VSet.t) (a : t) : var Seq.t * Int.t VMap.t Seq.t + = + if Abstract1.is_bottom man a then (Seq.empty, Seq.empty) + else + let unbound, bound = + VSet.to_seq vset + |> Seq.filter (fun v -> + match v.var_typ with A_int _ | A_BOOL -> true | _ -> false ) + |> Seq.map (fun v -> + match int_var_bnds v with + | None -> (v, Seq.return Int.zero) + | Some (var_inf, var_len) -> ( + let inf, sup = + Abstract1.bound_variable man a (apron_of_var v) + |> Banal_itv_int.of_apron + in + match (inf, sup) with + | Finite inf, Finite sup -> + let inf_id = Int.(fdiv (inf - var_inf) var_len) in + let sup_id = Int.(fdiv (sup - var_inf) var_len) in + assert (sup_id >= inf_id) ; + if Int.(sup_id - inf_id > of_int 2) then (v, Seq.empty) + else + ( v + , Seq.ints 0 + |> Seq.map (fun i -> Int.(of_int i + inf_id)) + |> Seq.take_while (fun i -> i <= sup_id) ) + | _ -> (v, Seq.empty) ) ) + |> Seq.partition (fun (_, idxs) -> Seq.is_empty idxs) + in + let unbound = Seq.map (fun (v, _) -> v) unbound in + (* compute the quadrant indexs *) + let rec doit seq vars = + match Seq.uncons vars with + | None -> seq + | Some ((v, bnd), next) -> + let seq = + Seq.flat_map + (fun idx -> Seq.map (fun id -> VMap.add v id idx) bnd) + seq + in + doit seq next + in + let idxs = doit (Seq.return VMap.empty) bound in + (unbound, idxs) (* compute the directions of a poly *) - let get_directions (a: t) : Linexpr1.t list = + let get_directions (a : t) : Linexpr1.t list = lincons_seq_of_abs a - |> Seq.map (Lincons1.get_linexpr1) - |> Seq.map (fun lc -> Linexpr1.set_cst lc (Coeff.s_of_int 0); lc) - |> List.of_seq + |> Seq.map Lincons1.get_linexpr1 + |> Seq.map (fun lc -> + Linexpr1.set_cst lc (Coeff.s_of_int 0) ; + lc ) + |> List.of_seq (* Refinement utils *) (* **************** *) @@ -501,38 +530,47 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let get_singleton post = let arr = Abstract1.to_lincons_array man post in Seq.ints 0 - |> Seq.take (Lincons1.array_length arr) - |> Seq.map (Lincons1.array_get arr) - |> Seq.fold_left (fun acc lc -> - if Lincons1.get_typ lc <> EQ then acc else - match lincons_single_var vset lc with - | Some (_, v) -> VMap.add v (Lincons1.get_cst lc) acc - | None -> acc - ) VMap.empty + |> Seq.take (Lincons1.array_length arr) + |> Seq.map (Lincons1.array_get arr) + |> Seq.fold_left + (fun acc lc -> + if Lincons1.get_typ lc <> EQ then acc + else + match lincons_single_var vset lc with + | Some (_, v) -> VMap.add v (Lincons1.get_cst lc) acc + | None -> acc ) + VMap.empty in - let singl1 = get_singleton post1 in let singl2 = get_singleton post2 in - (* ensure that at least one singleton component differ by +-1 *) - if VMap.exists2o - (fun _ _ -> false) - (fun _ _ -> false) - (fun v c1 c2 -> - match v.var_typ with - | A_int _ -> - let c1 = Banal_itv_rat.of_coeff c1 |> Banal_itv_rat.to_int_exact_opt |> Option.get in - let c2 = Banal_itv_rat.of_coeff c2 |> Banal_itv_rat.to_int_exact_opt |> Option.get in - Int.(abs (c2 - c1) = one) - | _ -> false) - singl1 singl2 + if + VMap.exists2o + (fun _ _ -> false) + (fun _ _ -> false) + (fun v c1 c2 -> + match v.var_typ with + | A_int _ -> + let c1 = + Banal_itv_rat.of_coeff c1 |> Banal_itv_rat.to_int_exact_opt + |> Option.get + in + let c2 = + Banal_itv_rat.of_coeff c2 |> Banal_itv_rat.to_int_exact_opt + |> Option.get + in + Int.(abs (c2 - c1) = one) + | _ -> false ) + singl1 singl2 then (* ensure that the arguments have the same rays *) let rays1 = ray_list_of_abs post1 in let rays2 = ray_list_of_abs post2 in - - if List.for_all (fun r1 -> List.exists (fun r2 -> r1 = r2) rays2) rays1 && - List.for_all (fun r2 -> List.exists (fun r1 -> r1 = r2) rays1) rays2 + if + List.for_all (fun r1 -> List.exists (fun r2 -> r1 = r2) rays2) rays1 + && List.for_all + (fun r2 -> List.exists (fun r1 -> r1 = r2) rays1) + rays2 then Abstract1.join man post1 post2 |> Option.some else None else None @@ -540,77 +578,93 @@ module Make (Param: APRON_PARAM) (Itv: INTERVAL) = struct let refine_behind_cons vset post1 post2 = let env = Abstract1.env post1 in let int_v, real_v = Environment.vars env in - lincons_seq_of_abs post1 - |> Seq.find_map (fun cons -> - (* consider only constraints relating integral variables with - integral coefficients *) - let nz_real = Array.exists (fun v -> - Lincons1.get_coeff cons v |> Coeff.is_zero |> not - ) real_v in - let nint_int = Array.for_all (fun v -> - Lincons1.get_coeff cons v - |> Banal_itv_rat.of_coeff - |> Banal_itv_rat.to_int_exact_opt - |> Option.is_none - ) int_v in - let nint_cst = Lincons1.get_cst cons - |> Banal_itv_rat.of_coeff - |> Banal_itv_rat.to_int_exact_opt - |> Option.is_none - in - if nz_real || nint_int || nint_cst then None else - - let () = assert (Lincons1.get_typ cons = SUPEQ) in - - (* find c' (note: c' here has opposite polarity compared to - the thm) *) - let lin_inc = Lincons1.get_linexpr1 cons |> Linexpr1.copy in - Linexpr1.set_cst lin_inc (Interval (Linexpr1.get_cst lin_inc |> Banal_itv_rat.of_coeff |> Banal_itv_rat.add Banal_itv_rat.one |> Banal_itv_rat.to_apron)); - let cons_inc = Lincons1.make lin_inc SUPEQ |> neg_lincons in - - (* instead of refining post1 with plain post2, meet post2 with - c' first to increase the chances of finding some generators - of post2 saturating c' *) - let post2_cons_inc = meet_lincons env post2 cons_inc in - if Abstract1.is_bottom man post2_cons_inc then None else - - (* find the generators of post1 and post2 saturating respectively - c and c'. Keep only the common rays *) - let post1_sat = gen_saturating_cons cons vset post1 in - let post2_sat = gen_saturating_cons cons_inc vset post2_cons_inc - |> List.filter (fun g1 -> - Generator1.get_typ g1 = VERTEX || List.exists (fun g2 -> g1 = g2) post1_sat) - in - let post1_sat = List.filter (fun g1 -> - Generator1.get_typ g1 = VERTEX || List.exists (fun g2 -> g1 = g2) post2_sat) post1_sat - in - - let () = assert (List.length post1_sat > 0) in - if List.length post2_sat = 0 then None else - - (* p1_nc *) - let post1_no_cons = remove_lincons cons post1 |> Option.get in - - (* pm *) - let middle_poly = add_generators (Abstract1.bottom man env) (post1_sat@post2_sat) in - - (* c' *) - let top_cons = Lincons1.make lin_inc SUPEQ in - - let rhs = match remove_lincons top_cons middle_poly with - | None -> Abstract1.meet_array man [|post1_no_cons; middle_poly; post2_cons_inc |] - | Some middle_poly_no_top -> Abstract1.meet_array man [|post1_no_cons; middle_poly_no_top; post2_cons_inc|] - in - - (* ensure that all the rays of `post` are also in `rhs` *) - let ray_post1 = ray_list_of_abs post1 in - let ray_rhs = ray_list_of_abs rhs in - if List.exists (fun g1 -> not (List.exists (fun g2 -> g1 = g2) ray_rhs)) ray_post1 - then None else - - let p = Abstract1.join man post1 rhs in - if Abstract1.is_leq man p post1 then None else Some p - ) - + |> Seq.find_map (fun cons -> + (* consider only constraints relating integral variables with + integral coefficients *) + let nz_real = + Array.exists + (fun v -> Lincons1.get_coeff cons v |> Coeff.is_zero |> not) + real_v + in + let nint_int = + Array.for_all + (fun v -> + Lincons1.get_coeff cons v |> Banal_itv_rat.of_coeff + |> Banal_itv_rat.to_int_exact_opt |> Option.is_none ) + int_v + in + let nint_cst = + Lincons1.get_cst cons |> Banal_itv_rat.of_coeff + |> Banal_itv_rat.to_int_exact_opt |> Option.is_none + in + if nz_real || nint_int || nint_cst then None + else + let () = assert (Lincons1.get_typ cons = SUPEQ) in + (* find c' (note: c' here has opposite polarity compared to the + thm) *) + let lin_inc = Lincons1.get_linexpr1 cons |> Linexpr1.copy in + Linexpr1.set_cst lin_inc + (Interval + ( Linexpr1.get_cst lin_inc |> Banal_itv_rat.of_coeff + |> Banal_itv_rat.add Banal_itv_rat.one + |> Banal_itv_rat.to_apron ) ) ; + let cons_inc = Lincons1.make lin_inc SUPEQ |> neg_lincons in + (* instead of refining post1 with plain post2, meet post2 with + c' first to increase the chances of finding some generators + of post2 saturating c' *) + let post2_cons_inc = meet_lincons env post2 cons_inc in + if Abstract1.is_bottom man post2_cons_inc then None + else + (* find the generators of post1 and post2 saturating + respectively c and c'. Keep only the common rays *) + let post1_sat = gen_saturating_cons cons vset post1 in + let post2_sat = + gen_saturating_cons cons_inc vset post2_cons_inc + |> List.filter (fun g1 -> + Generator1.get_typ g1 = VERTEX + || List.exists (fun g2 -> g1 = g2) post1_sat ) + in + let post1_sat = + List.filter + (fun g1 -> + Generator1.get_typ g1 = VERTEX + || List.exists (fun g2 -> g1 = g2) post2_sat ) + post1_sat + in + let () = assert (List.length post1_sat > 0) in + if List.length post2_sat = 0 then None + else + (* p1_nc *) + let post1_no_cons = + remove_lincons cons post1 |> Option.get + in + (* pm *) + let middle_poly = + add_generators + (Abstract1.bottom man env) + (post1_sat @ post2_sat) + in + (* c' *) + let top_cons = Lincons1.make lin_inc SUPEQ in + let rhs = + match remove_lincons top_cons middle_poly with + | None -> + Abstract1.meet_array man + [|post1_no_cons; middle_poly; post2_cons_inc|] + | Some middle_poly_no_top -> + Abstract1.meet_array man + [|post1_no_cons; middle_poly_no_top; post2_cons_inc|] + in + (* ensure that all the rays of `post` are also in `rhs` *) + let ray_post1 = ray_list_of_abs post1 in + let ray_rhs = ray_list_of_abs rhs in + if + List.exists + (fun g1 -> not (List.exists (fun g2 -> g1 = g2) ray_rhs)) + ray_post1 + then None + else + let p = Abstract1.join man post1 rhs in + if Abstract1.is_leq man p post1 then None else Some p ) end diff --git a/banal/banal_datatypes.ml b/banal/banal_datatypes.ml index 606154d6..a61b4d35 100644 --- a/banal/banal_datatypes.ml +++ b/banal/banal_datatypes.ml @@ -19,6 +19,12 @@ let compare_id (x : id) (y : id) = compare x y let dummy_id = Z.minus_one + +let lincons1_cmp c1 c2 = + Linexpr0.cmp c1.Lincons1.lincons0.Lincons0.linexpr0 + c2.Lincons1.lincons0.Lincons0.linexpr0 + + (* maps and sets *) (* ************* *) diff --git a/domains/Affines.ml b/domains/Affines.ml index 33547050..bcd10ef9 100644 --- a/domains/Affines.ml +++ b/domains/Affines.ml @@ -161,6 +161,9 @@ module Affine (B : PARTITION) : FUNCTION = struct | _ -> false (**) + let lincons1_cmp c1 c2 = + Linexpr0.cmp c1.Lincons1.lincons0.Lincons0.linexpr0 + c2.Lincons1.lincons0.Lincons0.linexpr0 let join_ranking k b f1 f2 = (* k = kind of join, b = domain of first/second function, f1/f2 = value @@ -170,7 +173,7 @@ module Affine (B : PARTITION) : FUNCTION = struct let l = Lincons1.array_length a in let b = ref false in for i = 0 to l - 1 do - if c = Lincons1.array_get a i then b := true + if lincons1_cmp c (Lincons1.array_get a i) = 0 then b := true done ; !b in @@ -309,7 +312,7 @@ module Affine (B : PARTITION) : FUNCTION = struct let l = Lincons1.array_length a in let b = ref false in for i = 0 to l - 1 do - if c = Lincons1.array_get a i then b := true + if lincons1_cmp c (Lincons1.array_get a i) = 0 then b := true done ; !b in @@ -381,7 +384,7 @@ module Affine (B : PARTITION) : FUNCTION = struct let l = Lincons1.array_length a in let b = ref false in for i = 0 to l - 1 do - if c = Lincons1.array_get a i then b := true + if lincons1_cmp c (Lincons1.array_get a i) = 0 then b := true done ; !b in diff --git a/domains/DecisionTree.ml b/domains/DecisionTree.ml index 4e18e5e2..3cb0b35f 100644 --- a/domains/DecisionTree.ml +++ b/domains/DecisionTree.ml @@ -79,6 +79,26 @@ struct (** The current decision tree. *) let tree t = t.tree + + 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 the current decision tree. *) let print_tree vars fmt t = @@ -521,9 +541,7 @@ struct else true else false | COMPUTATIONAL -> - F.isLeq k b f1 f2 (* forall x: f1(x) <= f2(x) *) - | _ -> raise (Invalid_argument ("Learning order not defined for tree")) ) - + F.isLeq k b f1 f2 (* forall x: f1(x) <= f2(x) *)) | Node ((c1,nc1),l1,r1), Node((c2,nc2),l2,r2) when (C.isEq c1 c2) -> (aux (l1,l2) (c1::cs)) && (aux (r1,r2) (nc1::cs)) | _ -> raise (Invalid_argument "isLeq:") @@ -623,7 +641,7 @@ struct let fBotLeftRight = match k with | APPROXIMATION -> fun _ _ -> Bot (* use NIL if at least one leaf is NIL *) | COMPUTATIONAL -> fun _ _ -> botLeaf (* use bottom leaf if at least one leaf is nil*) - | _ -> raise (Invalid_argument "Should not call Learning meet on decision trees") + (* | _ -> raise (Invalid_argument "Should not call Learning meet on decision trees") *) in let fLeaf cs f1 f2 = let b = match domain with diff --git a/domains/Domain.ml b/domains/Domain.ml index 1491ec4d..9725e579 100644 --- a/domains/Domain.ml +++ b/domains/Domain.ml @@ -63,7 +63,9 @@ module type RANKING_FUNCTION = 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 val robust : diff --git a/main/ASTCTLIterator.ml b/main/ASTCTLIterator.ml index afe1d554..88a19647 100644 --- a/main/ASTCTLIterator.ml +++ b/main/ASTCTLIterator.ml @@ -691,5 +691,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 + Config.tree := D.output_json program.variables programInvariant; + Config.result := D.defined ?condition:precondition programInvariant; D.defined ?condition:precondition programInvariant end diff --git a/main/CTLIterator.ml b/main/CTLIterator.ml index 2f8f7e1b..5c0256a1 100644 --- a/main/CTLIterator.ml +++ b/main/CTLIterator.ml @@ -8,8 +8,8 @@ open Functions open Iterator open ForwardIterator -(* type for CTL properties, instantiated with ControlFlowGraph.bool_expr for atomic - propositions *) +(* type for CTL properties, instantiated with ControlFlowGraph.bool_expr for + atomic propositions *) type ctl_property = ControlFlowGraph.bool_expr CTLProperty.generic_property let rec print_ctl_property ch (property : ctl_property) = @@ -133,7 +133,8 @@ module CTLIterator (D : RANKING_FUNCTION) = struct ( AbstractSyntax.A_var (Conversion.of_var var) , Conversion.of_int_expr expr ) | CFG_elm_assign (var, idx, expr) -> - raise (Invalid_argument "array element assignment is not yet supported") + raise + (Invalid_argument "array element assignment is not yet supported") | CFG_arr_assign (var, aexpr) -> raise (Invalid_argument "array assignment is not yet supported") | CFG_guard bexpr -> filter out_state @@ Conversion.of_bool_expr bexpr @@ -302,9 +303,9 @@ module CTLIterator (D : RANKING_FUNCTION) = struct in abstract_transformer - let compute (cfg : cfg) (main : ControlFlowGraph.func) (loop_heads : bool NodeMap.t) - (domSets : NodeSet.t NodeMap.t) - robust (property : ctl_property) : inv = + let compute (cfg : cfg) (main : ControlFlowGraph.func) + (loop_heads : bool NodeMap.t) (domSets : NodeSet.t NodeMap.t) robust + (property : ctl_property) : inv = let backwardAnalysis = CFGInterpreter.backward_analysis in let env, vars = Conversion.env_vars_of_cfg cfg in let print_inv property inv = @@ -413,10 +414,20 @@ module CTLIterator (D : RANKING_FUNCTION) = struct let analyze ?(precondition = CFG_bool_const true) (cfg : cfg) robust (main : ControlFlowGraph.func) (loop_heads : bool NodeMap.t) - (domSets : NodeSet.t NodeMap.t) - (property : ctl_property) = + (domSets : NodeSet.t NodeMap.t) (property : ctl_property) = let inv = compute cfg main loop_heads domSets robust property in let programInvariant = NodeMap.find main.func_entry inv in let precondition = Conversion.of_bool_expr precondition in - D.defined ~condition:precondition programInvariant + let r = D.defined ~condition:precondition programInvariant in + Config.tree := + D.output_json + (List.map + (fun v -> + let v : AbstractSyntax.var = + {varId= string_of_int v.var_id; varName= v.var_name; varTyp= A_INT} + in + v ) + cfg.cfg_vars ) + programInvariant ; + Config.result := r end diff --git a/main/GuaranteeIterator.ml b/main/GuaranteeIterator.ml index f70d1564..9d95ff8c 100644 --- a/main/GuaranteeIterator.ml +++ b/main/GuaranteeIterator.ml @@ -321,5 +321,7 @@ module GuaranteeIterator (D : RANKING_FUNCTION) = struct Format.fprintf !fmt "\nBackward Analysis (Time: %f s):\n" (stopbwd -. startbwd) else bwdMap_print robust !fmt !bwdInvMap ; + Config.tree := D.output_json vars i; + Config.result := D.defined i; D.defined i ) end diff --git a/main/Main.ml b/main/Main.ml index c1bbafc5..2ec6746a 100644 --- a/main/Main.ml +++ b/main/Main.ml @@ -10,29 +10,7 @@ (* parsing *) open Iterators -let analysis = ref "termination" - -let robust = ref false - -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 @@ -132,160 +110,112 @@ let parseCTLPropertyString (property : string) = @@ parseCTLPropertyString_plain property let parse_args () = - let rec doit args = - match args with - (* General arguments -------------------------------------------*) - | "-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 - | "-joinfwd" :: x :: r -> - (* widening delay in forward analysis *) - Iterator.joinfwd := int_of_string x ; - doit r - | "-joinbwd" :: x :: r -> - (* widening delay in backward analysis *) - Iterator.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 - | "-minimal" :: r -> - (* analysis result only *) - minimal := true ; - Iterator.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 - | "-retrybwd" :: x :: r -> - Iterator.retrybwd := int_of_string x ; - DecisionTree.retrybwd := int_of_string x ; - doit r - - | "-evolve"::x::r -> - Iterator.evolve := true; - DecisionTree.evolve := true; - Iterator.evolvethr := int_of_string x; - DecisionTree.evolvethr := int_of_string x; - doit r - | "-tracebwd" :: r -> - (* backward analysis trace *) - Iterator.tracebwd := true ; - DecisionTree.tracebwd := true ; - CFGInterpreter.trace := true ; - CFGInterpreter.trace_states := true ; - doit r - | "-tracefwd" :: r -> - (* forward analysis trace *) - Iterator.tracefwd := true ; - doit r - - - (* Termination arguments -------------------------------*) - | "-termination" :: r -> - (* guarantee analysis *) - analysis := "termination" ; - doit r - (* Recurrence / Guarantee arguments -------------------------------*) - | "-guarantee" :: x :: r -> - (* guarantee analysis *) - analysis := "guarantee" ; - property := x ; - doit r - | "-robust_ctl" :: x :: r -> - analysis := "ctl" ; - property := x ; - robust := true ; - doit r - | "-robust" :: x :: r -> - analysis := "guarantee" ; - property := x ; - robust := true ; - doit r - | "-robust_termination" :: r -> - analysis := "termination" ; - robust := true ; - doit r - | "-recurrence" :: x :: r -> - (* recurrence analysis *) - analysis := "recurrence" ; - property := x ; - doit r - | "-time" :: r -> - (* track analysis time *) - time := true ; - doit r - | "-timebwd" :: r -> - (* track backward analysis time *) - Iterator.timebwd := true ; - doit r - | "-timefwd" :: r -> - (* track forward analysis time *) - Iterator.timefwd := true ; - doit r - (* CTL arguments - ---------------------------------------------------*) - | "-ctl-cfg" :: x :: r -> - (* CTL analysis *) - analysis := "ctl-cfg" ; - property := x ; - doit r - | "-ctl-ast" :: x :: r -> - (* use AST instead of CFG for analysis *) - analysis := "ctl-ast" ; - property := x ; - doit r - | "-dot" :: r -> - (* print CFG and decision trees in 'dot' format *) - Iterator.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 - | "-noinline" :: r -> - (* don't inline function calls, only for CFG based analysis *) - noinline := true ; - doit r - | "-cda" :: x :: r -> - Iterator.cda := true ; - Iterator.size := int_of_string x ; - Iterator.refine := true ; - doit r - | x :: r -> - filename := x ; - doit r - | [] -> () - in -(* let _ = List.map print_endline (Array.to_list Sys.argv) in *) - doit (List.tl (Array.to_list Sys.argv)) + Arg.parse + [ ( "-config" + , Arg.String (fun s -> Config.from_json s) + , "Set analysis configuration with a json file" ) + ; ( "-domain" + , Arg.String (fun s -> Config.domain := s) + , "Numerical Abstract Domain used" ) + ; ( "-nowrap" + , Arg.Unit (fun _ -> Config.nowrap := true) + , "Refine the backward analysis" ) + ; ( "-timeout" + , Arg.Float (fun d -> Config.timeout := d) + , "Maximal analysis time in seconds" ) + ; ( "-joinfwd" + , Arg.Int (fun i -> Config.joinfwd := i) + , "Widening delay in forward analysis" ) + ; ( "-joinbwd" + , Arg.Int (fun i -> Config.joinbwd := i) + , "Widening delay in backward analysis" ) + ; ( "-main" + , Arg.String (fun s -> Config.main := s) + , "Analysis entry point" ) + ; ( "-meetbwd" + , Arg.Int (fun i -> Config.meetbwd := i) + , "Dual widening delay in backward analysis" ) + ; ( "-minimal" + , Arg.Unit (fun _ -> Config.minimal := true) + , "Output analysis result only" ) + ; ( "-ordinals" + , Arg.Int + (fun i -> + Config.ordmax := i ; + Config.ordinals := true ) + , "Set ordinals based analysis" ) + ; ( "-refine" + , Arg.Unit (fun _ -> Config.refine := true) + , "Refine the backward analysis" ) + ; ( "-retrybwd" + , Arg.Int (fun i -> Config.retrybwd := i) + , "Retry widening heuristic" ) + ; ( "-tracefwd" + , Arg.Unit (fun _ -> Config.tracefwd := true) + , "Forward analysis trace" ) + ; ( "-tracebwd" + , Arg.Unit (fun _ -> Config.tracebwd := true) + , "Backward analysis trace" ) + ; ( "-cda" + , Arg.Int + (fun i -> + Config.cda := true ; + Config.refine := true ; + Config.size := i ) + , "Conflict-driven analysis" ) + ; ( "-termination" + , Arg.Unit (fun _ -> Config.analysis := "termination") + , "Termination analysis" ) + ; ( "-nontermination" + , Arg.Unit (fun _ -> Config.analysis := "non-termination") + , "Non-termination analysis" ) + ; ( "-time" + , Arg.Unit (fun _ -> Config.time := true) + , "Track analysis time" ) + ; ( "-timefwd" + , Arg.Unit (fun _ -> Config.timefwd := true) + , "Track forward analysis time" ) + ; ( "-timebwd" + , Arg.Unit (fun _ -> Config.timefwd := true) + , "Track backward analysis time" ) + ; ( "-ctl" + , Arg.String + (fun s -> + Config.analysis := "ctl" ; + Config.property := s ) + , "CTL analysis" ) + ; ( "-dot" + , Arg.Unit (fun _ -> Config.dot := true) + , "Output decision trees in dot format" ) + ; ( "-precondition" + , Arg.String (fun s -> Config.precondition := s) + , "Optional precondition that holds at the starts of the program" ) + ; ( "-ctl_existential_equivalence" + , Arg.Unit (fun _ -> Config.ctl_existential_equivalence := true) + , "Convert existential ctl properties to universal" ) + ; ( "-vulnerability" + , Arg.Unit (fun _ -> Config.vulnerability := true) + , "Vulnerability analysis" ) + ; ( "-resilience" + , Arg.Unit + (fun _ -> + Config.analysis := "termination" ; + Config.resilience := true ) + , "Termination Resilience analysis" ) + ; ( "-json_output" + , Arg.String + (fun s -> + Config.json_output := true ; + Config.output_dir := s ) + , "Summary of the analysis in a json file" ) + ; ( "-json_output_std" + , Arg.Unit (fun _ -> Config.json_output := true) + , "Summary of the analysis as a json in stdout" ) ] + (fun s -> Config.filename := s) + "" (* do all *) -let result = ref false - let run_analysis analysis_function program () = try let start = Sys.time () in @@ -410,7 +340,8 @@ let ctl_ast () = let analyze = match !domain with | "boxes" -> - if !ordinals then ASTCTLBoxesOrdinals.analyze else ASTCTLBoxes.analyze + if !ordinals then ASTCTLBoxesOrdinals.analyze + else ASTCTLBoxes.analyze | "octagons" -> if !ordinals then ASTCTLOctagonsOrdinals.analyze else ASTCTLOctagons.analyze @@ -421,8 +352,8 @@ let ctl_ast () = in let result = analyze ~precondition program property in ( if !time then - let stoptime = Sys.time () in - Format.fprintf !fmt "\nTime: %f" (stoptime -. starttime) ) ; + let stoptime = Sys.time () in + Format.fprintf !fmt "\nTime: %f" (stoptime -. starttime) ) ; if result then Format.fprintf !fmt "\nAnalysis Result: TRUE\n" else Format.fprintf !fmt "\nAnalysis Result: UNKNOWN\n" @@ -436,7 +367,9 @@ let ctl_cfg () = let mainFunc = ControlFlowGraph.find_func !main cfg in let cfg = ControlFlowGraph.insert_entry_exit_label cfg mainFunc in (* add exit/entry labels to main function *) - let cfg = if !noinline then cfg else ControlFlowGraph.inline_function_calls cfg in + let cfg = + if !noinline then cfg else ControlFlowGraph.inline_function_calls cfg + in (* inline all non recursive functions unless -noinline is used *) let cfg = ControlFlowGraph.add_function_call_arcs cfg in (* insert function call edges for remaining function calls *) @@ -453,9 +386,11 @@ let ctl_cfg () = | "boxes" -> if !ordinals then CTLBoxesOrdinals.analyze else CTLBoxes.analyze | "octagons" -> - if !ordinals then CTLOctagonsOrdinals.analyze else CTLOctagons.analyze + if !ordinals then CTLOctagonsOrdinals.analyze + else CTLOctagons.analyze | "polyhedra" -> - if !ordinals then CTLPolyhedraOrdinals.analyze else CTLPolyhedra.analyze + if !ordinals then CTLPolyhedraOrdinals.analyze + else CTLPolyhedra.analyze | _ -> raise (Invalid_argument "Unknown Abstract Domain") in if not !minimal then ( @@ -468,28 +403,27 @@ let ctl_cfg () = let mainFunc = ControlFlowGraph.find_func !main cfg in let possibleLoopHeads = Loop_detection.possible_loop_heads cfg mainFunc in let domSets = Loop_detection.dominator cfg mainFunc in - let result = - analyze ~precondition cfg !robust mainFunc possibleLoopHeads domSets ctlProperty - in + analyze ~precondition cfg !robust mainFunc possibleLoopHeads domSets + ctlProperty ; ( if !time then - let stoptime = Sys.time () in - Format.fprintf !fmt "\nTime: %f" (stoptime -. starttime) ) ; - if result then Format.fprintf !fmt "\nAnalysis Result: TRUE\n" + let stoptime = Sys.time () in + Format.fprintf !fmt "\nTime: %f" (stoptime -. starttime) ) ; + if !Config.result then Format.fprintf !fmt "\nAnalysis Result: TRUE\n" else Format.fprintf !fmt "\nAnalysis Result: UNKNOWN\n" (*Main entry point for application*) let doit () = parse_args () ; - match !analysis with + ( match !analysis with | "termination" -> termination () | "guarantee" -> guarantee () | "recurrence" -> recurrence () | "ctl-ast" -> ctl_ast () + | "ctl" -> ctl_ast () | "ctl-cfg" -> ctl_cfg () - | _ -> raise (Invalid_argument "Unknown Analysis") + | _ -> raise (Invalid_argument "Unknown Analysis") ) ; + Regression.output_json () let _ = doit () (* DEPRECATED STUFF BELOW *) - - diff --git a/main/RecurrenceIterator.ml b/main/RecurrenceIterator.ml index 42d1f37f..7b5d1014 100644 --- a/main/RecurrenceIterator.ml +++ b/main/RecurrenceIterator.ml @@ -211,5 +211,7 @@ module RecurrenceIterator (D : RANKING_FUNCTION) = struct (stopbwd -. startbwd) else Format.fprintf !fmt "\nBackward Analysis:\n" ; bwdMap_print !fmt !bwdInvMap ) ; + Config.tree := D.output_json vars i; + Config.result := D.defined i; D.defined i end diff --git a/main/TerminationIterator.ml b/main/TerminationIterator.ml index 01233364..b9889642 100644 --- a/main/TerminationIterator.ml +++ b/main/TerminationIterator.ml @@ -409,7 +409,6 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct aux (B.top env vars) (D.bot env vars) 1 let analyze (vars, stmts, funcs) main robust = - let sv = vars in let rec aux xs env = match xs with | [] -> env @@ -467,5 +466,7 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct else Format.fprintf !fmt "\nBackward Analysis:\n" ; bwdMap_print !fmt !bwdInvMap ) ; if robust then bwdMap_robust !fmt vars !bwdInvMap; + Config.tree := D.output_json vars i; + Config.result := D.defined i; D.defined i ) end diff --git a/tests/ctl/and_ef_test.c b/tests/ctl/and_ef_test.c new file mode 100644 index 00000000..0cf4dc88 --- /dev/null +++ b/tests/ctl/and_ef_test.c @@ -0,0 +1,12 @@ +// -domain polyhedra +// -ctl "AND{EF{x == 2}}{EF{x==3}}" + +int main() { + int x; + if (rand()){ + x = 2; + } else { + x = 3; + } + return 0; +} diff --git a/tests/ctl/and_ef_test.json b/tests/ctl/and_ef_test.json new file mode 100644 index 00000000..24c8e264 --- /dev/null +++ b/tests/ctl/and_ef_test.json @@ -0,0 +1,3 @@ +{ + "property": "AND{EF{x == 2}}{EF{x==3}}" +} \ No newline at end of file diff --git a/tests/ctl/and_test.c b/tests/ctl/and_test.c index 21de09f7..b2fc48a0 100644 --- a/tests/ctl/and_test.c +++ b/tests/ctl/and_test.c @@ -1,5 +1,5 @@ // FuncTion arguments: -// -ctl "AND{AG{AF{n==1}}}{AF{n==0}}" +// -ctl_cfg "AND{AG{AF{n==1}}}{AF{n==0}}" // -precondition n > 0 void main() { @@ -9,7 +9,7 @@ void main() { n--; } - while (n == 0) { + while (true) { n++; n--; } diff --git a/tests/ctl/and_test.json b/tests/ctl/and_test.json new file mode 100644 index 00000000..b6b2b4b3 --- /dev/null +++ b/tests/ctl/and_test.json @@ -0,0 +1,4 @@ +{ + "property": "AND{AG{AF{n==1}}}{AF{n==0}}", + "precondition": "n>0" +} \ No newline at end of file diff --git a/tests/ctl/and_test.t2 b/tests/ctl/and_test.t2 deleted file mode 100644 index da3d76a0..00000000 --- a/tests/ctl/and_test.t2 +++ /dev/null @@ -1,37 +0,0 @@ -// -CTL="[AG]([AF](n==1))) && [AF](n==0)" proof failed -// -CTL="[AG]([AF](n==1)))" proof failed -// -CTL="[AF](n==0)" proof succeeds - -START: 1; - -FROM: 1; -TO: 2; -FROM: 2; - nondef.0 := nondet(); - n := nondef.0; - assume (n > 0); -TO: 3; -FROM: 3; - assume(n > 0); -TO: 4; -FROM: 3; - assume(n <= 0); -TO: 5; -FROM: 4; - n := n - 1; -TO: 3; -FROM: 5; - assume(n == 0); -TO: 6; -FROM: 5; - assume(n < 0); -TO: 7; -FROM: 5; - assume(n > 0); -TO: 7; -FROM: 6; - n := n + 1; - n := n - 1; -TO: 5; -FROM: 7; -TO: 8; diff --git a/tests/ctl/existential_test1.c b/tests/ctl/existential_test1.c index 82c32f37..0f79727c 100644 --- a/tests/ctl/existential_test1.c +++ b/tests/ctl/existential_test1.c @@ -5,7 +5,7 @@ int main() { int x; int y; if (2*x <= y+3) { - if (? == 1) { + if (rand() == 1) { r = 1; } } diff --git a/tests/ctl/existential_test1.json b/tests/ctl/existential_test1.json new file mode 100644 index 00000000..53934c34 --- /dev/null +++ b/tests/ctl/existential_test1.json @@ -0,0 +1,4 @@ +{ + "property": "EF{r == 1}", + "precondition":"2*x <= y+3" +} \ No newline at end of file diff --git a/tests/ctl/existential_test1.t2 b/tests/ctl/existential_test1.t2 deleted file mode 100644 index 0b6ad6f6..00000000 --- a/tests/ctl/existential_test1.t2 +++ /dev/null @@ -1,31 +0,0 @@ -// [EF](r == 1) - -START: 1; - -FROM: 1; - r := 0; - x := nondet(); - y := nondet(); - assume(2*x <= y + 3); -TO: 2; - -FROM: 2; - assume(2*x <= y + 3); -TO: 3; - -FROM: 3; - r := 1; -TO: 4; - -FROM: 4; -TO: 5; - -FROM: 3; -TO: 5; - -FROM: 2; - assume(2*x > y + 3); -TO: 5; - -FROM: 5; -TO: 5; diff --git a/tests/ctl/existential_test2.c b/tests/ctl/existential_test2.c index a437c975..75079e35 100644 --- a/tests/ctl/existential_test2.c +++ b/tests/ctl/existential_test2.c @@ -8,7 +8,7 @@ int main() { if (x*x < y*y + 3*x*y) { // here we use non-linear expression that can't be expressed // in any of the domains to validate if FILTER underapproximates correctly - if (?) { + if (rand()){ r = 1; } } diff --git a/tests/ctl/existential_test2.json b/tests/ctl/existential_test2.json new file mode 100644 index 00000000..43f325d7 --- /dev/null +++ b/tests/ctl/existential_test2.json @@ -0,0 +1,4 @@ +{ + "property": "EF{r == 1}", + "domain": "polyhedra" +} \ No newline at end of file diff --git a/tests/ctl/existential_test3.c b/tests/ctl/existential_test3.c index cc82354b..2a51f9c5 100644 --- a/tests/ctl/existential_test3.c +++ b/tests/ctl/existential_test3.c @@ -13,7 +13,7 @@ int main() { int x; while (x > 0) { x = x - 1; - if (?) { + if (rand()){ r = 1; } } diff --git a/tests/ctl/existential_test3.json b/tests/ctl/existential_test3.json new file mode 100644 index 00000000..337ff75c --- /dev/null +++ b/tests/ctl/existential_test3.json @@ -0,0 +1,5 @@ +{ + "property": "EF{r == 1}", + "precondition": "x == 2", + "joinbwd": 5 +} \ No newline at end of file diff --git a/tests/ctl/existential_test3.t2 b/tests/ctl/existential_test3.t2 deleted file mode 100644 index 7ff6df3d..00000000 --- a/tests/ctl/existential_test3.t2 +++ /dev/null @@ -1,34 +0,0 @@ -///*** 1_main ***/// -// [EF](r==1) -START: 1; - -FROM: 1; -TO: 2; - -FROM: 2; - nondef.0 := nondet(); - x := nondet(); - assume(x > 0); -TO: 3; - -FROM: 3; - assume(x > 0); -TO: 4; - -FROM: 3; - assume(x <= 0); -TO: 6; - -FROM: 4; - x := x - 1; -TO: 5; - -FROM: 5; - r := 1; -TO: 3; - -FROM: 5; -TO: 3; - -FROM: 6; -TO: 6; diff --git a/tests/ctl/existential_test4.json b/tests/ctl/existential_test4.json new file mode 100644 index 00000000..8807e4e6 --- /dev/null +++ b/tests/ctl/existential_test4.json @@ -0,0 +1,3 @@ +{ + "property": "EF{r == 1}" +} \ No newline at end of file diff --git a/tests/ctl/existential_test4.t2 b/tests/ctl/existential_test4.t2 deleted file mode 100644 index 7b0da6ef..00000000 --- a/tests/ctl/existential_test4.t2 +++ /dev/null @@ -1,40 +0,0 @@ -/// [EF](r==1) -START: 1; - -FROM: 1; - x := nondet(); - y := nondet(); - r := 0; -TO: 2; - -FROM: 2; - assume(y < 0); -TO: 3; - -FROM: 2; - assume(y >= 0); -TO: 4; - -FROM: 3; - assume(x < 0); -TO: 5; - -FROM: 3; - assume(x >= 0); -TO: 7; - -FROM: 5; - r := 1; -TO: 8; - -FROM: 8; -TO: 9; - -FROM: 7; -TO: 9; - -FROM: 4; -TO: 9; - -FROM: 9; -TO: 9; diff --git a/tests/ctl/fin_ex.c b/tests/ctl/fin_ex.c index cf4392a1..60dccc0d 100644 --- a/tests/ctl/fin_ex.c +++ b/tests/ctl/fin_ex.c @@ -1,5 +1,5 @@ // FuncTion arguments: -// -ctl "EG{EF{n==1}} +// -ctl_cfg "EG{EF{n==1}} // -precondition n > 0 // -domain polyhedra @@ -10,7 +10,7 @@ void main() { n--; } - if (?) { + if (rand()){ while (n == 0) { n++; n--; diff --git a/tests/ctl/fin_ex.json b/tests/ctl/fin_ex.json new file mode 100644 index 00000000..27471c94 --- /dev/null +++ b/tests/ctl/fin_ex.json @@ -0,0 +1,5 @@ +{ + "property": "EG{EF{n==1}}", + "precondition": "n > 0", + "domain": "polyhedra" +} \ No newline at end of file diff --git a/tests/ctl/fin_ex.t2 b/tests/ctl/fin_ex.t2 deleted file mode 100644 index 990bf437..00000000 --- a/tests/ctl/fin_ex.t2 +++ /dev/null @@ -1,50 +0,0 @@ -// -CTL="[EG]([EF](n==1)))" proof failed - -START: 1; - -FROM: 1; -TO: 2; - -FROM: 2; - nondef.0 := nondet(); - n := nondef.0; - assume (n > 0); -TO: 3; - -FROM: 3; - assume(n > 0); -TO: 4; - -FROM: 3; - assume(n <= 0); -TO: 9; - -FROM: 4; - n := n - 1; -TO: 3; - -FROM: 9; -TO: 7; - -FROM: 9; -TO: 5; - -FROM: 5; - assume(n == 0); -TO: 6; - -FROM: 5; - assume(n < 0); -TO: 7; - -FROM: 5; - assume(n > 0); -TO: 7; - -FROM: 6; - n := n + 1; - n := n - 1; -TO: 5; - -FROM: 7; -TO: 8; diff --git a/tests/ctl/global_test_simple.c b/tests/ctl/global_test_simple.c index 6300ee75..64ae01f7 100644 --- a/tests/ctl/global_test_simple.c +++ b/tests/ctl/global_test_simple.c @@ -1,5 +1,5 @@ // FuncTion arguments: -// -ctl "AG{AF{x <= -10}}" +// -ctl_cfg "AG{AF{x <= -10}}" // -joinbwd 4 int main() { int x; diff --git a/tests/ctl/global_test_simple.json b/tests/ctl/global_test_simple.json new file mode 100644 index 00000000..db438ea2 --- /dev/null +++ b/tests/ctl/global_test_simple.json @@ -0,0 +1,4 @@ +{ + "property": "AG{AF{x <= -10}}", + "joinbwd": 4 +} \ No newline at end of file diff --git a/tests/ctl/global_test_simple.t2 b/tests/ctl/global_test_simple.t2 deleted file mode 100644 index dabe1352..00000000 --- a/tests/ctl/global_test_simple.t2 +++ /dev/null @@ -1,33 +0,0 @@ -// "[AG]([AF](x <= -10))" crash -START: 1; - -FROM: 1; -TO: 2; -FROM: 2; - x := nondet(); -TO: 3; -FROM: 3; - assume(x < 0); -TO: 4; -FROM: 3; - assume(x >= 0); -TO: 5; -FROM: 4; - x := x + 1; -TO: 6; -FROM: 6; - assume(x < -3); -TO: 7; -FROM: 6; - assume(x >= -3); -TO: 3; -FROM: 7; - x := x - 1; -TO: 6; - -FROM: 5; - x := -20; -TO: 8; - -FROM: 8; -TO: 8; diff --git a/tests/ctl/koskinen/acqrel.c b/tests/ctl/koskinen/acqrel.c index fa0b44f6..c6befd9f 100644 --- a/tests/ctl/koskinen/acqrel.c +++ b/tests/ctl/koskinen/acqrel.c @@ -11,7 +11,7 @@ // Property: AG(a => AF r) // FuncTion arguments: -// -ctl "AG{OR{A!=1}{AF{R==1}}}" +// -ctl_cfg "AG{OR{A!=1}{AF{R==1}}}" // -precondition "A==0 && R==0" @@ -23,7 +23,7 @@ void main() { while(?) { A = 1; A = 0; - n = ?; + n = rand(); while(n>0) { n--; } diff --git a/tests/ctl/koskinen/acqrel.json b/tests/ctl/koskinen/acqrel.json new file mode 100644 index 00000000..b4228452 --- /dev/null +++ b/tests/ctl/koskinen/acqrel.json @@ -0,0 +1,4 @@ +{ + "property": "AG{OR{A!=1}{AF{R==1}}}", + "precondition":"A==0 && R==0" +} \ No newline at end of file diff --git a/tests/ctl/koskinen/acqrel_mod.json b/tests/ctl/koskinen/acqrel_mod.json new file mode 100644 index 00000000..a05ab309 --- /dev/null +++ b/tests/ctl/koskinen/acqrel_mod.json @@ -0,0 +1,4 @@ +{ + "property": "AG{OR{a!=1}{AF{r==1}}}", + "precondition": "x != 1" +} \ No newline at end of file diff --git a/tests/ctl/koskinen/acqrel_mod.t2 b/tests/ctl/koskinen/acqrel_mod.t2 deleted file mode 100644 index d85cc6a8..00000000 --- a/tests/ctl/koskinen/acqrel_mod.t2 +++ /dev/null @@ -1,45 +0,0 @@ -// -CTL="[AG](a != 1 || [AF](r==1))" - -START: 1; - -FROM: 1; - a := 0; - r := 0; - m := m_init; -TO: 2; - -FROM: 2; - assume (m > 0); -TO: 3; - -FROM: 2; - assume (m <= 0); -TO: 4; - -FROM: 4; -TO: 4; - -FROM: 3; - a := 1; - a := 0; - n := n_init; -TO: 5; - -FROM: 5; - assume (n > 0); -TO: 6; - -FROM: 6; - n := n - 1; -TO: 5; - -FROM: 5; - assume (n <= 0); -TO: 7; - -FROM: 7; - r := 1; - r := 0; -TO: 2; - - diff --git a/tests/ctl/koskinen/fig8-2007.c b/tests/ctl/koskinen/fig8-2007.c deleted file mode 100644 index 78654355..00000000 --- a/tests/ctl/koskinen/fig8-2007.c +++ /dev/null @@ -1,38 +0,0 @@ -// ************************************************************* -// Original Source: -// Byron Cook * Eric Koskinen -// July 2010 -// -// -// Adjusted for FuncTion by Samuel Ueltschi -// ************************************************************* - -// Benchmark: fig8-2007.c -// -// -ctl "OR{set==0}{AF{unset == 1}}" - -int i; int Pdolen; int DName; -int status; - -int set; -int unset; - -void main() { - set = 1; - while (i < Pdolen) { - DName = ?; - if (!DName) { break; } - status = ?; - if (1 != status) { - if (2 == status) { - goto loc_continue; - } - break; - } else { - i++; - } - } -loc_continue: - unset = 1; -} - diff --git a/tests/ctl/koskinen/fig8-2007.ltl.c b/tests/ctl/koskinen/fig8-2007.ltl.c deleted file mode 100644 index d0b69ec4..00000000 --- a/tests/ctl/koskinen/fig8-2007.ltl.c +++ /dev/null @@ -1,30 +0,0 @@ -//#Safe -//@ ltl invariant positive: AP(set == 0) || <>AP(unset == 1); - -extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); - -int i; int Pdolen; int DName; -int status; - -int set = 0; -int unset = 0; - -void main() { - set = 1; - while (i < Pdolen) { - DName = __VERIFIER_nondet_int(); - if (!DName) { break; } - status = __VERIFIER_nondet_int(); - if (1 != status) { - if (2 == status) { - goto loc_continue; - } - break; - } else { - i++; - } - } -loc_continue: - unset = 1; -} - diff --git a/tests/ctl/koskinen/fig8-2007_mod.c b/tests/ctl/koskinen/fig8-2007_mod.c deleted file mode 100644 index b2541791..00000000 --- a/tests/ctl/koskinen/fig8-2007_mod.c +++ /dev/null @@ -1,42 +0,0 @@ -// ************************************************************* -// Original Source: -// Byron Cook * Eric Koskinen -// July 2010 -// -// Modified version of acqrel that can be proven by FuncTion -// ************************************************************* - -// FuncTion arguments: -// -ctl "OR{set==0}{AF{unset == 1}}" - -int i; int Pdolen; int DName; -int status; - -int set; -int unset; - -void main() { - - set = 1; // aquire resource - - while (i < Pdolen) { - // DName = ?; // leads to bad widening behaviour - if (!DName) { break; } - status = ?; - if (1 != status) { - if (2 == status) { - goto loc_continue; - } - break; - } else { - i++; - } - } - -loc_continue: - - // release resource - unset = 1; - -} - diff --git a/tests/ctl/koskinen/fig8-2007_mod.t2 b/tests/ctl/koskinen/fig8-2007_mod.t2 deleted file mode 100644 index 17c8d53e..00000000 --- a/tests/ctl/koskinen/fig8-2007_mod.t2 +++ /dev/null @@ -1,48 +0,0 @@ -///*** 1_main ***/// -// set != 1 || [AF](unset == 1)" - -START: 1; - -FROM: 1; - set := 1; - unset := nondet(); - i := nondet(); - Pdolen := nondet(); - DName := nondet(); - status := nondet(); -TO: 2; - -FROM: 2; - assume(i < Pdolen); -TO: 3; - -FROM: 3; - status := nondet(); -TO: 4; - -FROM: 3; - assume(DName == 0); -TO: 8; - -FROM: 4; - assume (status == 1); -TO: 5; - -FROM: 5; - i := i + 1; -TO: 2; - -FROM: 4; - assume (status != 1); -TO: 6; - -FROM: 6; -TO: 8; - -FROM: 8; - unset := 1; -TO: 9; - -FROM: 9; -TO: 9; - diff --git a/tests/ctl/koskinen/toylin1.c b/tests/ctl/koskinen/toylin1.c index 66b17c6a..a3e81ed3 100644 --- a/tests/ctl/koskinen/toylin1.c +++ b/tests/ctl/koskinen/toylin1.c @@ -7,15 +7,17 @@ // // ************************************************************* -// -ctl "AF{resp > 5}" +// -ctl_cfg "AF{resp > 5}" // -precondition "c > 5" + int c; // assume c > 0 int servers = 4; int resp = 0; int curr_serv = servers; void main() { + while(curr_serv > 0) { if(?) { c--; curr_serv--; diff --git a/tests/ctl/koskinen/toylin1.json b/tests/ctl/koskinen/toylin1.json new file mode 100644 index 00000000..1485fd11 --- /dev/null +++ b/tests/ctl/koskinen/toylin1.json @@ -0,0 +1,4 @@ +{ + "property": "AF{resp > 5}", + "precondition": "c > 5" +} \ No newline at end of file diff --git a/tests/ctl/koskinen/toylin1.t2 b/tests/ctl/koskinen/toylin1.t2 deleted file mode 100644 index 98274723..00000000 --- a/tests/ctl/koskinen/toylin1.t2 +++ /dev/null @@ -1,38 +0,0 @@ -// -CTL="[AF](resp > 5)" - -START: 1; - -FROM: 1; - assume(c > 5); - servers := 4; - resp := 0; - curr_serv := servers; -TO: 2; - -FROM: 2; - assume (curr_serv > 0); -TO: 3; - -FROM: 2; - assume (curr_serv <= 0); -TO: 6; - -FROM: 6; -TO: 6; - -FROM: 3; -TO: 4; - -FROM: 4; - c := c - 1; - curr_serv := curr_serv - 1; - resp := resp + 1; -TO: 2; - -FROM: 3; - assume (c < curr_serv); -TO: 5; - -FROM: 5; - curr_serv := curr_serv - 1; -TO: 2; diff --git a/tests/ctl/koskinen/win4.json b/tests/ctl/koskinen/win4.json new file mode 100644 index 00000000..31e72838 --- /dev/null +++ b/tests/ctl/koskinen/win4.json @@ -0,0 +1,3 @@ +{ + "property": "AF{AG{WItemsNum >= 1}}" +} \ No newline at end of file diff --git a/tests/ctl/koskinen/win4.t2 b/tests/ctl/koskinen/win4.t2 deleted file mode 100644 index 3e81f7e4..00000000 --- a/tests/ctl/koskinen/win4.t2 +++ /dev/null @@ -1,54 +0,0 @@ -// -CTL="[AF]([AG](w >= 1))" - -START: 20; - -FROM: 20; -TO: 1; - -FROM: 1; -TO: 2; - -FROM: 2; - assume (w <= 5); -TO: 3; - -FROM: 2; -TO: 4; - -FROM: 2; -TO: 9; - -FROM: 3; -TO: 5; - -FROM: 4; -TO: 5; - -FROM: 5; - assume (w <= 5); -TO: 6; - -FROM: 5; - assume (w > 5); -TO: 7; - -FROM: 6; -TO: 8; - -FROM: 7; -TO: 8; - -FROM: 8; - w := w + 1; -TO: 2; - -FROM: 9; - assume (w > 2); -TO: 10; - -FROM: 10; - w := w - 1; -TO: 9; - -FROM: 9; -TO: 1; diff --git a/tests/ctl/ltl_automizer/Bug_NoLoopAtEndForTerminatingPrograms_safe.json b/tests/ctl/ltl_automizer/Bug_NoLoopAtEndForTerminatingPrograms_safe.json new file mode 100644 index 00000000..bf39d2e7 --- /dev/null +++ b/tests/ctl/ltl_automizer/Bug_NoLoopAtEndForTerminatingPrograms_safe.json @@ -0,0 +1,4 @@ +{ + "property": "NOT{AF{ap > 2}}", + "precondition": "ap == 0" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/PotentialMinimizeSEVPABug.json b/tests/ctl/ltl_automizer/PotentialMinimizeSEVPABug.json new file mode 100644 index 00000000..1ccc576e --- /dev/null +++ b/tests/ctl/ltl_automizer/PotentialMinimizeSEVPABug.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{x <= 0}{AF{y == 0}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/cav2015.json b/tests/ctl/ltl_automizer/cav2015.json new file mode 100644 index 00000000..1ccc576e --- /dev/null +++ b/tests/ctl/ltl_automizer/cav2015.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{x <= 0}{AF{y == 0}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_1_safe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_1_safe_sfty.json new file mode 100644 index 00000000..f7c74530 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_1_safe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{chainBroken != 1}{AG{chainBroken == 1}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_1_unsafe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_1_unsafe_sfty.json new file mode 100644 index 00000000..f7c74530 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_1_unsafe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{chainBroken != 1}{AG{chainBroken == 1}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_2_safe_lifeness.json b/tests/ctl/ltl_automizer/coolant_basis_2_safe_lifeness.json new file mode 100644 index 00000000..528289c5 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_2_safe_lifeness.json @@ -0,0 +1,3 @@ +{ + "property": "\"AG{AF{otime < time}}\"" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_2_unsafe_lifeness.json b/tests/ctl/ltl_automizer/coolant_basis_2_unsafe_lifeness.json new file mode 100644 index 00000000..61d90888 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_2_unsafe_lifeness.json @@ -0,0 +1,3 @@ +{ + "property": "AG{AF{otime < time}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_3_safe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_3_safe_sfty.json new file mode 100644 index 00000000..c96b5eac --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_3_safe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{init != 3}{AG{AF{time > otime}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_3_unsafe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_3_unsafe_sfty.json new file mode 100644 index 00000000..c96b5eac --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_3_unsafe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{init != 3}{AG{AF{time > otime}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_4_safe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_4_safe_sfty.json new file mode 100644 index 00000000..0813f494 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_4_safe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{init != 3}{OR{temp <= limit}{AF{AG{chainBroken == 1}}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_4_unsafe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_4_unsafe_sfty.json new file mode 100644 index 00000000..0813f494 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_4_unsafe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{init != 3}{OR{temp <= limit}{AF{AG{chainBroken == 1}}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.c b/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.c index e2b6b488..2b0f0a0e 100644 --- a/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.c +++ b/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.c @@ -2,7 +2,7 @@ // //@ ltl invariant positive: AP(init == 0) U( (AP(init == 1) U [] AP(init == 3)) || [] AP(init == 1)); // -// -ctl AU{init == 0}{OR{AU{init == 1}{AG{init == 3}}}{AG{init == 1}}}; +// -ctl_cfg AU{init == 0}{OR{AU{init == 1}{AG{init == 3}}}{AG{init == 1}}}; #include diff --git a/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.json b/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.json new file mode 100644 index 00000000..dd13f38e --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.json @@ -0,0 +1,3 @@ +{ + "property": "AU{init == 0}{OR{AU{init == 1}{AG{init == 3}}}{AG{init == 1}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_5_safe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_5_safe_sfty.json new file mode 100644 index 00000000..dd13f38e --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_5_safe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AU{init == 0}{OR{AU{init == 1}{AG{init == 3}}}{AG{init == 1}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_5_unsafe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_5_unsafe_sfty.json new file mode 100644 index 00000000..ad34e462 --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_5_unsafe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "\"AU{init == 0}{OR{AU{init == 1}{AG{init == 3}}}{AG{init == 1}}}\"" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_6_safe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_6_safe_sfty.json new file mode 100644 index 00000000..6180028d --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_6_safe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{limit <= -273 && limit >= 10}{OR{tempIn >= 0}{AF{ warnLED == 1}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/coolant_basis_6_unsafe_sfty.json b/tests/ctl/ltl_automizer/coolant_basis_6_unsafe_sfty.json new file mode 100644 index 00000000..6180028d --- /dev/null +++ b/tests/ctl/ltl_automizer/coolant_basis_6_unsafe_sfty.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{limit <= -273 && limit >= 10}{OR{tempIn >= 0}{AF{ warnLED == 1}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.c b/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.c index b3998ef8..c00fa62e 100644 --- a/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.c +++ b/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.c @@ -2,11 +2,12 @@ // CHECK( init(main()), LTL( G("i >= n") ) ) extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); -int n; -int i = 1; + int main() -{ +{ + int n; + int i = 1; while(1){ i++; while(i > n){ diff --git a/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.json b/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.json new file mode 100644 index 00000000..31ff46dc --- /dev/null +++ b/tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.json @@ -0,0 +1,3 @@ +{ + "property": "AG{i >= n}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/postgre.c b/tests/ctl/ltl_automizer/postgre.c new file mode 100644 index 00000000..6e90dd0e --- /dev/null +++ b/tests/ctl/ltl_automizer/postgre.c @@ -0,0 +1,349 @@ +//#Safe +//@ ltl invariant positive: <>AP(phi_io_compl == 1) || <>AP(phi_nSUC_ret == 1); + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(); +extern int __VERIFIER_nondet_int(); + +#define NTSTATUS int +#define PIRP int +#define PDEVICE_OBJECT int +#define KIRQL int +#include +#define STATUS_UNSUCCESSFUL 1 +#define STATUS_SUCCESS 2 +#define IOCTL_SERIAL_GET_WAIT_MASK 3 +#define STATUS_BUFFER_TOO_SMALL 4 +#define IOCTL_SERIAL_SET_WAIT_MASK 5 +#define ULONG int +#define IOCTL_SERIAL_WAIT_ON_MASK 6 +#define STATUS_PENDING 7 +#define IOCTL_SERIAL_PURGE 8 +#define PULONG int +#define IOCTL_SERIAL_GET_MODEMSTATUS 9 +#define SERIAL_PURGE_RXABORT 10 +#define STATUS_CANCELLED 11 +#define IOCTL_SERIAL_SET_TIMEOUTS 12 +#define PSERIAL_TIMEOUTS int +#define PSERIAL_STATUS int +#define PSERIAL_BAUD_RATE int +#define SERIAL_TIMEOUTS 14 +#define STATUS_INVALID_PARAMETER 15 +#define IOCTL_SERIAL_GET_TIMEOUTS 16 +#define IOCTL_SERIAL_SET_DTR 17 +#define IOCTL_SERIAL_CLR_DTR 18 +#define IOCTL_SERIAL_GET_COMMSTATUS 19 +#define IOCTL_SERIAL_GET_BAUD_RATE 20 +#define IOCTL_SERIAL_SET_BAUD_RATE 21 +#define IOCTL_SERIAL_SET_QUEUE_SIZE 22 +#define SERIAL_BAUD_RATE int +#define IOCTL_SERIAL_SET_LINE_CONTROL 23 +#define UCHAR int +#define SERIAL_LINE_CONTROL int +#define PSERIAL_LINE_CONTROL int +#define SERIAL_6_DATA 24 +#define SERIAL_7_DATA 25 +#define SERIAL_8_DATA 26 +#define SERIAL_5_DATA 27 +#define NO_PARITY 28 +#define SERIAL_NONE_PARITY 29 +#define EVEN_PARITY 30 +#define SERIAL_EVEN_PARITY 31 +#define ODD_PARITY 32 +#define SERIAL_ODD_PARITY 33 +#define SPACE_PARITY 34 +#define SERIAL_SPACE_PARITY 35 +#define MARK_PARITY 36 +#define SERIAL_MARK_PARITY 37 +#define STOP_BIT_1 28 +#define STOP_BITS_2 29 +#define STOP_BIT_3 30 +#define STOP_BIT_4 31 +#define SERIAL_1_STOP 32 +#define SERIAL_2_STOP 33 +#define SERIAL_3_STOP 34 +#define SERIAL_4_STOP 35 +#define STOP_BITS_1_5 36 +#define SERIAL_1_5_STOP 37 +#define SERIAL_LCR_BREAK 38 +#define IOCTL_SERIAL_GET_LINE_CONTROL 39 +#define IOCTL_SERIAL_SET_RTS 40 +#define STATUS_NOT_SUPPORTED 41 +#define PDEVICE_EXTENSION int +#define PCROM_DATA int +#define PASYNC_ADDRESS_DATA int +#define PISOCH_DETACH_DATA int +#define PISOCH_RESOURCE_DATA int +#define TRUE 1 +#define FALSE 0 +#define PIRB int +#define IRB int +#define CCHAR int +#define PBUS_RESET_IRP int +#define PDRIVER_CANCEL int +#define NonPagedPool 1 +#define IO_NO_INCREMENT 2 + + +int lock1; +int lock2; +int lock3; +int lock4; +int lock5; +int lock6; +int CancelIrql; +int irql; +int csl; +PDEVICE_OBJECT DeviceObject; +PIRP Irp; +NTSTATUS ntStatus; +PDEVICE_EXTENSION deviceExtension; +KIRQL Irql; +int k1; +int k2; +int k3; +int k4; +int k5; +PCROM_DATA CromData; +PASYNC_ADDRESS_DATA AsyncAddressData; +PISOCH_RESOURCE_DATA IsochResourceData; +PISOCH_DETACH_DATA IsochDetachData; +ULONG i; +PIRB pIrb; +PIRP ResourceIrp; +CCHAR StackSize; +PBUS_RESET_IRP BusResetIrp; +PDRIVER_CANCEL prevCancel; + + + +int keA; int keR; int ioA; int ioR; +int phi_nSUC_ret; int phi_io_compl; + +unsigned int pc; +// AG(A => AF(R) +//int __phi() { return CAG(COR( CAF(CAP(keR == 1)), CAP(keA != 1) )); } +//int __phi() { return CAG(COR( CAF(CAP(ioR == 1)), CAP(ioA != 1) )); } +/* prove that either IoCompleteRequest is called, + or a value other than STATUS_SUCCESS is returned. */ +/*int __phi() { return COR( + CAF(CAP(phi_io_compl == 1)), + CAF(CAP(phi_nSUC_ret == 1))); }*/ + + + keA = keR = ioA = ioR = 0; + phi_nSUC_ret = 0; + phi_io_compl = 0; + + +void KeAcquireSpinLock(int * lp, int * ip) { keA = 1; keA = 0; + (*lp) = 1; + (*ip) = irql; +} + +void KeReleaseSpinLock(int * lp, int i) { keR = 1; keR = 0; + (*lp) = 0; + irql = i; +} + +void IoAcquireCancelSpinLock(int * ip) { ioA = 1; ioA = 0; + csl = 1; + (*ip) = irql; +} + +void IoReleaseCancelSpinLock(int ip) { ioR = 1; ioR = 0; + csl = 0; + irql = ip; +} + +int t1394_IsochCleanup(int a) { } +int ExAllocatePool(int a, int b) { } +int t1394Diag_PnpStopDevice(int a,int b) { } +int t1394_SubmitIrpSynch(int a, int b) { } +int IoFreeIrp(int a) { } +int IoSetDeviceInterfaceState() { } +int RtlZeroMemory(int a, int b) { } +int KeCancelTimer() { } +int IoAllocateIrp(int a, int b) { } +int IoFreeMdl() { } +int IoSetCancelRoutine(int a) { } +int ExFreePool0() { } +int ExFreePool1(int a) { } +int ExFreePool2(int a, int b) { } +int IoCompleteRequest(int a) { phi_io_compl = 1; } + +int main() { + if (__VERIFIER_nondet_int()) { + + // haven't stopped yet, lets do so + ntStatus = t1394Diag_PnpStopDevice(DeviceObject, Irp); + } + + ntStatus = IoSetDeviceInterfaceState(); + + + // lets free up any crom data structs we've allocated... + KeAcquireSpinLock(&lock3, &Irql); + + k1 = __VERIFIER_nondet_int(); + while (k1>0) { + + CromData = __VERIFIER_nondet_int(); + + // get struct off list + k1--; + + // need to free up everything associated with this allocate... + if (CromData) + { + if (__VERIFIER_nondet_int()) + ExFreePool0(); + + if (__VERIFIER_nondet_int()) + IoFreeMdl(); + + // we already checked CromData + ExFreePool1(CromData); + } + } + + KeReleaseSpinLock(&lock3, Irql); + + KeAcquireSpinLock(&lock1, &Irql); + + k2 = __VERIFIER_nondet_int(); + while (k2>0) { + + AsyncAddressData = __VERIFIER_nondet_int(); + + // get struct off list + AsyncAddressData = __VERIFIER_nondet_int(); + k2--; + + // need to free up everything associated with this allocate... + if (__VERIFIER_nondet_int()) + IoFreeMdl(); + + if (__VERIFIER_nondet_int()) + ExFreePool0(); + + if (__VERIFIER_nondet_int()) + ExFreePool0(); + + if (AsyncAddressData) + ExFreePool0(); + } + + KeReleaseSpinLock(&lock1, Irql); + + // free up any attached isoch buffers + while (TRUE) { + + KeAcquireSpinLock(&lock4, &Irql); + + k3 = __VERIFIER_nondet_int(); + if (k3>0) { + + IsochDetachData = __VERIFIER_nondet_int(); + i = __VERIFIER_nondet_int(); + + IsochDetachData = __VERIFIER_nondet_int(); + k3--; + + + KeCancelTimer(); + KeReleaseSpinLock(&lock4, Irql); + + + t1394_IsochCleanup(IsochDetachData); + } + else { + + KeReleaseSpinLock(&lock4, Irql); + break; + } + } + + // remove any isoch resource data + + k4 = __VERIFIER_nondet_int(); + while (TRUE) { + + KeAcquireSpinLock(&lock5, &Irql); + if (k4>0) { + + IsochResourceData = __VERIFIER_nondet_int(); + k4--; + + KeReleaseSpinLock(&lock5, Irql); + + + if (IsochResourceData) { + + pIrb = __VERIFIER_nondet_int(); + ResourceIrp = __VERIFIER_nondet_int(); + StackSize = __VERIFIER_nondet_int(); + ResourceIrp = IoAllocateIrp(StackSize, FALSE); + + if (ResourceIrp == NULL) { + + } + else { + + pIrb = ExAllocatePool(NonPagedPool, sizeof(IRB)); + + if (!pIrb) { + + IoFreeIrp(ResourceIrp); + } + else { + + RtlZeroMemory (pIrb, sizeof (IRB)); + + ntStatus = t1394_SubmitIrpSynch(ResourceIrp, pIrb); + + + ExFreePool1(pIrb); + IoFreeIrp(ResourceIrp); + } + } + } + } + else { + + KeReleaseSpinLock(&lock5, Irql); + break; + } + } + + // get rid of any pending bus reset notify requests + KeAcquireSpinLock(&lock6, &Irql); + + k5 = __VERIFIER_nondet_int(); + while (k5>0) { + + prevCancel = NULL; + + // get the irp off of the list + BusResetIrp = __VERIFIER_nondet_int(); + k5--; + + + // make this irp non-cancelable... + prevCancel = IoSetCancelRoutine(NULL); + + + // and complete it... + IoCompleteRequest(IO_NO_INCREMENT); + + ExFreePool1(BusResetIrp); + } + + KeReleaseSpinLock(&lock6, Irql); + + // free up the symbolic link + if(ntStatus != STATUS_SUCCESS) { + phi_nSUC_ret = 1; + } + while(1) {} +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/postgre.json b/tests/ctl/ltl_automizer/postgre.json new file mode 100644 index 00000000..752fe128 --- /dev/null +++ b/tests/ctl/ltl_automizer/postgre.json @@ -0,0 +1,3 @@ +{ + "property": "resp > 5" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/prop.json b/tests/ctl/ltl_automizer/prop.json new file mode 100644 index 00000000..20537f23 --- /dev/null +++ b/tests/ctl/ltl_automizer/prop.json @@ -0,0 +1,3 @@ +{ + "property": "x == 4" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/simple-1.json b/tests/ctl/ltl_automizer/simple-1.json new file mode 100644 index 00000000..efc8eb2b --- /dev/null +++ b/tests/ctl/ltl_automizer/simple-1.json @@ -0,0 +1,3 @@ +{ + "property": "AF{x > 10000}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/simple-2.json b/tests/ctl/ltl_automizer/simple-2.json new file mode 100644 index 00000000..d9ab697e --- /dev/null +++ b/tests/ctl/ltl_automizer/simple-2.json @@ -0,0 +1,3 @@ +{ + "property": "AF{x > 100}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/someNonterminating.json b/tests/ctl/ltl_automizer/someNonterminating.json new file mode 100644 index 00000000..8a89e86d --- /dev/null +++ b/tests/ctl/ltl_automizer/someNonterminating.json @@ -0,0 +1,3 @@ +{ + "property": "EG{x > 0}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/timer-intermediate.json b/tests/ctl/ltl_automizer/timer-intermediate.json new file mode 100644 index 00000000..40bf4d07 --- /dev/null +++ b/tests/ctl/ltl_automizer/timer-intermediate.json @@ -0,0 +1,3 @@ +{ + "property": "AG{OR{input_1 >= 1000}{AF{output_1 == 1}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/timer-simple.json b/tests/ctl/ltl_automizer/timer-simple.json new file mode 100644 index 00000000..086b8a33 --- /dev/null +++ b/tests/ctl/ltl_automizer/timer-simple.json @@ -0,0 +1,3 @@ +{ + "property": "NOT{AG{OR{timer_1 != 0}{AF{output_1 == 1}}}}" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/togglecounter_true-valid-ltl.json b/tests/ctl/ltl_automizer/togglecounter_true-valid-ltl.json new file mode 100644 index 00000000..fb961a69 --- /dev/null +++ b/tests/ctl/ltl_automizer/togglecounter_true-valid-ltl.json @@ -0,0 +1,3 @@ +{ + "property": "" +} \ No newline at end of file diff --git a/tests/ctl/ltl_automizer/toggletoggle_true-valid-ltl.json b/tests/ctl/ltl_automizer/toggletoggle_true-valid-ltl.json new file mode 100644 index 00000000..985559d4 --- /dev/null +++ b/tests/ctl/ltl_automizer/toggletoggle_true-valid-ltl.json @@ -0,0 +1,4 @@ +{ + "property": "AG{AND{AF{t == 1}{AF{t == 0}}}}", + "precondition": "t >= 0" +} \ No newline at end of file diff --git a/tests/ctl/multi_branch_choice.c b/tests/ctl/multi_branch_choice.c index 8cca3d6e..3c42319c 100644 --- a/tests/ctl/multi_branch_choice.c +++ b/tests/ctl/multi_branch_choice.c @@ -2,15 +2,15 @@ * Samuel Ueltschi: multiple branches with initial non-det choice * * FuncTion arguments: - * -ctl AF{OR{x==4}{x==-4}} - * -ctl EF{x==-4} + * -ctl_cfg AF{OR{x==4}{x==-4}} + * -ctl_cfg EF{x==-4} * */ int main() { int x; - if (?) { + if (rand()){ x = 1; } else { x = -1; diff --git a/tests/ctl/multi_branch_choice.json b/tests/ctl/multi_branch_choice.json new file mode 100644 index 00000000..8e5da762 --- /dev/null +++ b/tests/ctl/multi_branch_choice.json @@ -0,0 +1,3 @@ +{ + "property": "AF{OR{x==4}{x==-4}}" +} \ No newline at end of file diff --git a/tests/ctl/multi_branch_choice.ltl.c b/tests/ctl/multi_branch_choice.ltl.c deleted file mode 100644 index dee01db0..00000000 --- a/tests/ctl/multi_branch_choice.ltl.c +++ /dev/null @@ -1,35 +0,0 @@ -//#Safe -//@ ltl invariant positive: <>(AP(x == 4 || x == -4)); - -extern int __VERIFIER_nondet_int() __attribute__ ((__noreturn__)); - -int x; - -int main() { - - if (__VERIFIER_nondet_int()) { - x = 1; - } else { - x = -1; - } - - if (x > 0) { - x = x + 1; - } else { - x = x - 1; - } - - if (x > 0) { - x = x + 1; - } else { - x = x - 1; - } - - if (x > 0) { - x = x + 1; - } else { - x = x - 1; - } - - -} diff --git a/tests/ctl/multi_branch_choice.t2 b/tests/ctl/multi_branch_choice.t2 deleted file mode 100644 index 02e451b3..00000000 --- a/tests/ctl/multi_branch_choice.t2 +++ /dev/null @@ -1,49 +0,0 @@ -///*** 1_main ***/// -// [AF](x == 4 || x == -4) -// [EF](x==4) -START: 1; - -FROM: 1; - x := nondet(); -TO: 2; - -FROM: 2; - x := 1; -TO: 3; - -FROM: 2; - x := -1; -TO: 3; - -FROM: 3; - assume(x>0); - x := x + 1; -TO: 4; - -FROM: 3; - assume(x<=0); - x := x - 1; -TO: 4; - -FROM: 4; - assume(x>0); - x := x + 1; -TO: 5; - -FROM: 4; - assume(x<=0); - x := x - 1; -TO: 5; - -FROM: 5; - assume(x>0); - x := x + 1; -TO: 6; - -FROM: 5; - assume(x<=0); - x := x - 1; -TO: 6; - - - diff --git a/tests/ctl/next.json b/tests/ctl/next.json new file mode 100644 index 00000000..14e66c0f --- /dev/null +++ b/tests/ctl/next.json @@ -0,0 +1,4 @@ +{ + "property": "AX{x==0}", + "precondition": "x == 0" +} \ No newline at end of file diff --git a/tests/ctl/or_test.json b/tests/ctl/or_test.json new file mode 100644 index 00000000..b570bc2b --- /dev/null +++ b/tests/ctl/or_test.json @@ -0,0 +1,3 @@ +{ + "property": "OR{AF{AG{x < -100}}}{AF{x==20}}" +} \ No newline at end of file diff --git a/tests/ctl/or_test.ltl.c b/tests/ctl/or_test.ltl.c deleted file mode 100644 index 8a2ecaf4..00000000 --- a/tests/ctl/or_test.ltl.c +++ /dev/null @@ -1,10 +0,0 @@ -//#Safe -//@ ltl invariant positive: <>[]AP(x < -100) || <>AP(x == 20); -int x; -int main() { - if (x <= 0) { - while(x <= 0) { x--; } - } else { - x = 20; - } -} diff --git a/tests/ctl/or_test.t2 b/tests/ctl/or_test.t2 deleted file mode 100644 index 3baa5622..00000000 --- a/tests/ctl/or_test.t2 +++ /dev/null @@ -1,32 +0,0 @@ -///*** 1_main ***/// -// [AF]([AG]( x < -100 )) || [AF](x==20) -START: 1; - -FROM: 1; - x := nondet(); -TO: 2; - -FROM: 2; - assume(x <= 0); -TO: 3; - -FROM: 2; - assume(x > 0); - x := 20; -TO: 4; - -FROM: 3; - assume(x <= 0); -TO: 5; - -FROM: 3; - assume(x > 0); -TO: 4; - -FROM: 5; - kittel_old__x := x; - x := x - 1; -TO: 3; - -FROM: 4; -TO: 6; diff --git a/tests/ctl/potential_termination_1.c b/tests/ctl/potential_termination_1.c index 055eb617..18d17aaf 100755 --- a/tests/ctl/potential_termination_1.c +++ b/tests/ctl/potential_termination_1.c @@ -2,7 +2,7 @@ /** * Samuel Ueltschi: example for potential termination * - * -ctl "EF{exit: true}" + * -ctl_cfg "EF{exit: true}" */ int main() { @@ -10,8 +10,8 @@ int main() { int x; int y; y = 1; - i = ?; - x = ?; + i = rand(); + x = rand(); if (i > 10) { x = 1; diff --git a/tests/ctl/potential_termination_1.json b/tests/ctl/potential_termination_1.json new file mode 100644 index 00000000..51e760e3 --- /dev/null +++ b/tests/ctl/potential_termination_1.json @@ -0,0 +1,3 @@ +{ + "property": "EF{exit: true}" +} \ No newline at end of file diff --git a/tests/ctl/potential_termination_1.t2 b/tests/ctl/potential_termination_1.t2 deleted file mode 100644 index 51fb91d7..00000000 --- a/tests/ctl/potential_termination_1.t2 +++ /dev/null @@ -1,40 +0,0 @@ -// [EF](exit == 1) - -START: 1; - -FROM: 1; - exit := 0; - y := 1; - i := nondet(); - x := nondet(); -TO: 2; - -FROM: 2; - assume(i > 10); -TO: 3; - -FROM: 3; - x := 1; -TO: 4; - -FROM: 2; - assume(i <= 10); -TO: 4; - - -FROM: 4; - assume(x == y); -TO: 5; - - -FROM: 5; -TO: 4; - - -FROM: 4; - assume(x != y); -TO: 6; - -FROM: 6; - exit := 1; -TO: 7; diff --git a/tests/ctl/report/test_existential2.json b/tests/ctl/report/test_existential2.json new file mode 100644 index 00000000..8807e4e6 --- /dev/null +++ b/tests/ctl/report/test_existential2.json @@ -0,0 +1,3 @@ +{ + "property": "EF{r == 1}" +} \ No newline at end of file diff --git a/tests/ctl/report/test_existential3.c b/tests/ctl/report/test_existential3.c index cc82354b..2a51f9c5 100644 --- a/tests/ctl/report/test_existential3.c +++ b/tests/ctl/report/test_existential3.c @@ -13,7 +13,7 @@ int main() { int x; while (x > 0) { x = x - 1; - if (?) { + if (rand()){ r = 1; } } diff --git a/tests/ctl/report/test_existential3.json b/tests/ctl/report/test_existential3.json new file mode 100644 index 00000000..d73daedf --- /dev/null +++ b/tests/ctl/report/test_existential3.json @@ -0,0 +1,5 @@ +{ + "property": "EF{r == 1}", + "precondition": "precondition x==2", + "joinbwd": 5 +} \ No newline at end of file diff --git a/tests/ctl/report/test_global.json b/tests/ctl/report/test_global.json new file mode 100644 index 00000000..b6bb063e --- /dev/null +++ b/tests/ctl/report/test_global.json @@ -0,0 +1,3 @@ +{ + "property": "AF{AG{y > 0}}" +} \ No newline at end of file diff --git a/tests/ctl/report/test_until.json b/tests/ctl/report/test_until.json new file mode 100644 index 00000000..73d97ecc --- /dev/null +++ b/tests/ctl/report/test_until.json @@ -0,0 +1,5 @@ +{ + "property": "AU{x >= y}{x == y}", + "precondition": "x >= y", + "domain":"polyhedra" +} \ No newline at end of file diff --git a/tests/ctl/run.sh b/tests/ctl/run.sh index f09929d6..5481c10b 100755 --- a/tests/ctl/run.sh +++ b/tests/ctl/run.sh @@ -1,8 +1,8 @@ -./function -dot -domain polyhedra -joinbwd 4 "./tests/ctl/global_test_simple.c" -ctl_str "AG{AF{x <= -10}}" | python ./pretty.py > ./tests/ctl/global_test_simple.html -./function -dot -domain polyhedra -precondition "x == y + 20" "./tests/ctl/until_test.c" -ctl_str "AU{x >= y}{x==y}"| python ./pretty.py > ./tests/ctl/until_test.html -./function -dot -domain polyhedra -precondition "n > 0" "./tests/ctl/and_test.c" -ctl_str "AND{AG{AF{n==1}}}{AF{n==0}}"| python ./pretty.py > ./tests/ctl/and_test.html -./function -dot -domain polyhedra "./tests/ctl/or_test.c" -ctl_str "OR{AF{AG{x < -100}}}{AF{x==20}}"| python ./pretty.py > ./tests/ctl/or_test.html -./function -dot -domain polyhedra -precondition "x==1" "./tests/ctl/next.c" -ctl_str "AX{x==0}"| python ./pretty.py > ./tests/ctl/next.html -./function -dot -domain polyhedra -precondition "2*x <= y+3" "./tests/ctl/existential_test1.c" -ctl_str "EF{r==1}"| python ./pretty.py > ./tests/ctl/existential_test1.html -./function -dot -domain polyhedra -precondition "a!=1" "./tests/ctl/acqrel.c" -ctl_str "AG{OR{a!=1}{AF{r==1}}}"| python ./pretty.py > ./tests/ctl/acqrel.html -./function -dot -domain polyhedra "./tests/ctl/win4.c" -ctl_str "AF{AG{WItemsNum >= 1}}"| python ./pretty.py > ./tests/ctl/win4.html +./main.exe -dot -domain polyhedra -joinbwd 4 "./tests/ctl/global_test_simple.c" -ctl_str "AG{AF{x <= -10}}" | python ./pretty.py > ./tests/ctl/global_test_simple.html +./main.exe -dot -domain polyhedra -precondition "x == y + 20" "./tests/ctl/until_test.c" -ctl_str "AU{x >= y}{x==y}"| python ./pretty.py > ./tests/ctl/until_test.html +./main.exe -dot -domain polyhedra -precondition "n > 0" "./tests/ctl/and_test.c" -ctl_str "AND{AG{AF{n==1}}}{AF{n==0}}"| python ./pretty.py > ./tests/ctl/and_test.html +./main.exe -dot -domain polyhedra "./tests/ctl/or_test.c" -ctl_str "OR{AF{AG{x < -100}}}{AF{x==20}}"| python ./pretty.py > ./tests/ctl/or_test.html +./main.exe -dot -domain polyhedra -precondition "x==1" "./tests/ctl/next.c" -ctl_str "AX{x==0}"| python ./pretty.py > ./tests/ctl/next.html +./main.exe -dot -domain polyhedra -precondition "2*x <= y+3" "./tests/ctl/existential_test1.c" -ctl_str "EF{r==1}"| python ./pretty.py > ./tests/ctl/existential_test1.html +./main.exe -dot -domain polyhedra -precondition "a!=1" "./tests/ctl/acqrel.c" -ctl_str "AG{OR{a!=1}{AF{r==1}}}"| python ./pretty.py > ./tests/ctl/acqrel.html +./main.exe -dot -domain polyhedra "./tests/ctl/win4.c" -ctl_str "AF{AG{WItemsNum >= 1}}"| python ./pretty.py > ./tests/ctl/win4.html diff --git a/tests/ctl/run_cfg.sh b/tests/ctl/run_cfg.sh deleted file mode 100755 index 84a65d6d..00000000 --- a/tests/ctl/run_cfg.sh +++ /dev/null @@ -1,18 +0,0 @@ -./Main.native -dot -domain polyhedra -joinbwd 10 "./tests/ctl/global_test_simple.c" -ctl "AG{AF{x <= -10}}" | python ./pretty_cfg.py > ./tests/ctl/global_test_simple_cfg.html -./Main.native -dot -domain polyhedra -precondition "x == y + 20" "./tests/ctl/until_test.c" -ctl "AU{x >= y}{x==y}"| python ./pretty_cfg.py > ./tests/ctl/until_test_cfg.html -./Main.native -dot -domain polyhedra -precondition "n > 0" "./tests/ctl/and_test.c" -ctl "AND{AG{AF{n==1}}}{AF{n==0}}"| python ./pretty_cfg.py > ./tests/ctl/and_test_cfg.html -./Main.native -dot -domain polyhedra "./tests/ctl/or_test.c" -ctl "OR{AF{AG{x < -100}}}{AF{x==20}}"| python ./pretty_cfg.py > ./tests/ctl/or_test_cfg.html -./Main.native -dot -domain polyhedra -precondition "x==1" "./tests/ctl/next.c" -ctl "AX{AX{AX{x==0}}}"| python ./pretty_cfg.py > ./tests/ctl/next_cfg.html -./Main.native -dot -domain polyhedra -precondition "2*x <= y+3" "./tests/ctl/existential_test1.c" -ctl "EF{r==1}"| python ./pretty_cfg.py > ./tests/ctl/existential_test1_cfg.html -./Main.native -dot -domain polyhedra -precondition "a!=1" "./tests/ctl/acqrel.c" -ctl "AG{OR{a!=1}{AF{r==1}}}"| python ./pretty_cfg.py > ./tests/ctl/acqrel_cfg.html -./Main.native -dot -domain polyhedra -joinbwd 5 "./tests/ctl/win4.c" -ctl "AF{AG{WItemsNum >= 1}}"| python ./pretty_cfg.py > ./tests/ctl/win4_cfg.html - - -./Main.native -dot -domain polyhedra ./tests/ctl/ltl_automizer/coolant_basis_1_safe_sfty.c -ctl "AG{OR{chainBroken != 1}{AG{chainBroken == 1}}}" -precondition "chainBroken == 0" | python ./pretty_cfg.py > ./tests/ctl/ltl_automizer/coolant_basis_1_safe_sfty.html -./Main.native -dot -domain polyhedra -joinbwd 7 ./tests/ctl/ltl_automizer/coolant_basis_2_safe_lifeness.c -ctl "AG{AF{otime < time}}" | python ./pretty_cfg.py > ./tests/ctl/ltl_automizer/coolant_basis_2_safe_lifeness.html -./Main.native -dot -domain polyhedra tests/ctl/ltl_automizer/coolant_basis_3_safe_sfty.c -ctl "AG{OR{init != 3}{AG{AF{time > otime}}}}" -precondition "init == 0" | python ./pretty_cfg.py > ./tests/ctl/ltl_automizer/coolant_basis_3_safe_sfty.html -./Main.native -dot -domain polyhedra tests/ctl/ltl_automizer/coolant_basis_4_safe_sfty.c -ctl "AG{OR{init != 3}{OR{temp <= limit}{AF{AG{chainBroken == 1}}}}}" -precondition "init == 0 && temp < limit" | python ./pretty_cfg.py > ./tests/ctl/ltl_automizer/coolant_basis_4_safe_sfty.html -./Main.native -dot -domain polyhedra tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.c -ctl "AU{init == 0}{OR{AU{init == 1}{AG{init == 3}}}{AG{init == 1}}}" -precondition "init==0" | python ./pretty_cfg.py > ./tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.html -./Main.native -dot -domain polyhedra tests/ctl/ltl_automizer/coolant_basis_6_safe_sfty.c -ctl "AG{OR{limit <= -273 && limit >= 10}{OR{tempIn >= 0}{AF{ warnLED == 1}}}}" -precondition "init == 0 && temp < limit" | python ./pretty_cfg.py > ./tests/ctl/ltl_automizer/coolant_basis_6_safe_sfty.html - -./main.exe -ctl "AF{exit: true}" -dot -domain polyhedra -joinbwd 3 "./tests/example.c" | python3 ./pretty_cfg.py > ./tests/example.html \ No newline at end of file diff --git a/tests/ctl/sv_comp/Bangalore_false-no-overflow.json b/tests/ctl/sv_comp/Bangalore_false-no-overflow.json new file mode 100644 index 00000000..5e23864e --- /dev/null +++ b/tests/ctl/sv_comp/Bangalore_false-no-overflow.json @@ -0,0 +1,3 @@ +{ + "property": "EF{x < 0}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/Bangalore_false-no-overflow.t2 b/tests/ctl/sv_comp/Bangalore_false-no-overflow.t2 deleted file mode 100644 index 583782e3..00000000 --- a/tests/ctl/sv_comp/Bangalore_false-no-overflow.t2 +++ /dev/null @@ -1,31 +0,0 @@ -// -CTL="[EF](x < 0)" - -START: 1; - -FROM: 1; - x := nondet(); - y := nondet(); -TO: 2; - -FROM: 2; - assume(y < 1); -TO: 3; - -FROM: 3; - assume(x >= 0); -TO: 5; - -FROM: 5; - x := x - y; -TO: 3; - -FROM: 3; - assume(x < 0); -TO: 4; - -FROM: 2; - assume(y >= 1); -TO: 4; - -FROM: 4; -TO: 4; diff --git a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.c b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.c index 64b10421..3383f515 100755 --- a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.c +++ b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.c @@ -4,7 +4,7 @@ extern int __VERIFIER_nondet_int(void); int main() { int i; - //i = __VERIFIER_nondet_int(); + i = __VERIFIER_nondet_int(); while (i > 0) { if (i != 5) { diff --git a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.json b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.json new file mode 100644 index 00000000..da67411c --- /dev/null +++ b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.json @@ -0,0 +1,3 @@ +{ + "property": "OR{i >= 5}{AF{exit: true}}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.ltl.c b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.ltl.c index c36ef664..447191a5 100755 --- a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.ltl.c +++ b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.ltl.c @@ -10,7 +10,7 @@ int exit; int main() { - //i = __VERIFIER_nondet_int(); + i = __VERIFIER_nondet_int(); while (i > 0) { if (i != 5) { diff --git a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.t2 b/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.t2 deleted file mode 100755 index 95d612d4..00000000 --- a/tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.t2 +++ /dev/null @@ -1,30 +0,0 @@ -// -CTL="(i >= 5) || [AF](exit == 1) " - -START: 1; - -FROM: 1; -TO: 2; - -FROM: 2; - assume(i > 0); -TO: 3; - -FROM: 3; - assume(i != 5); -TO: 5; - -FROM: 3; - assume(i == 5); -TO: 2; - -FROM: 5; - i := i - 1; -TO: 2; - -FROM: 2; - assume(i <= 0); -TO: 4; - -FROM: 4; - exit := 1; -TO: 4; diff --git a/tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.json b/tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.json new file mode 100644 index 00000000..6f04e921 --- /dev/null +++ b/tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.json @@ -0,0 +1,3 @@ +{ + "property": "AF{AG{i==0}}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.t2 b/tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.t2 deleted file mode 100755 index 7e45c3de..00000000 --- a/tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.t2 +++ /dev/null @@ -1,34 +0,0 @@ -// -CTL="[AF]([AG](i==0))" - -START: init; - -FROM: init; -TO: 1; - -FROM: 1; - assume(i > 0); -TO: 2; - -FROM: 2; - i := i - 1; -TO: 3; - -FROM: 1; - assume(i <= 0); -TO: 3; - - -FROM: 3; - assume(i > 0); -TO: 4; - -FROM: 4; - i := i + 1; -TO: 5; - -FROM: 3; - assume(i <= 0); -TO: 5; - -FROM: 5; -TO: 1; diff --git a/tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.json b/tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.json new file mode 100644 index 00000000..80248e7d --- /dev/null +++ b/tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.json @@ -0,0 +1,3 @@ +{ + "property": "AF{AND{x==7}{AF{AG{x==2}}}}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.t2 b/tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.t2 deleted file mode 100755 index 9969b9e2..00000000 --- a/tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.t2 +++ /dev/null @@ -1,15 +0,0 @@ -// -CTL="[AF](x==7 && [AF]([AG](x==2)))" - -START: init; - -FROM: init; - x := 7; -TO: 1; - -FROM: 1; - x := 2; -TO: 2; - -FROM: 2; -TO: 1; - diff --git a/tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.json b/tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.json new file mode 100644 index 00000000..6e454588 --- /dev/null +++ b/tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.json @@ -0,0 +1,3 @@ +{ + "property": "EF{EG{j==0}}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.t2 b/tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.t2 deleted file mode 100755 index cf2e1c08..00000000 --- a/tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.t2 +++ /dev/null @@ -1,36 +0,0 @@ -// -CTL="[AF]([AG](j==0))" - -START: init; - -FROM: init; - i := 0; -TO: 1; - - -FROM: 1; - assume(i < 100); -TO: 2; - -FROM: 2; - j := 0; -TO: 4; - -FROM: 4; - assume(j < 1); -TO: 5; - -FROM: 5; - j := j + 0; -TO: 4; - -FROM: 4; - assume(j >= 1); -TO: 6; - -FROM: 6; - i := i + 1; -TO: 1; - -FROM: 1; - assume(i >= 100); -TO: 3; diff --git a/tests/ctl/sv_comp/afnp2014.c b/tests/ctl/sv_comp/afnp2014.c new file mode 100644 index 00000000..385fd441 --- /dev/null +++ b/tests/ctl/sv_comp/afnp2014.c @@ -0,0 +1,15 @@ +// Source: E. De Angelis, F. Fioravanti, J. A. Navas, M. Proietti: +// "Verification of Programs by Combining Iterated Specialization with +// Interpolation", HCVS 2014 , https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loop-lit/afnp2014.c +#include "assert.h" +int main() { + int x = 1; + int y = 0; + while (y < 1000 && ?) { + x = x + y; + y = y + 1; + } + here: + return 0; + +} diff --git a/tests/ctl/sv_comp/afnp2014.json b/tests/ctl/sv_comp/afnp2014.json new file mode 100644 index 00000000..dbc72865 --- /dev/null +++ b/tests/ctl/sv_comp/afnp2014.json @@ -0,0 +1,3 @@ +{ + "property": "AF{here: x < y}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/as2013-hybrid.c b/tests/ctl/sv_comp/as2013-hybrid.c new file mode 100644 index 00000000..3418faff --- /dev/null +++ b/tests/ctl/sv_comp/as2013-hybrid.c @@ -0,0 +1,24 @@ +// Source: Gianluca Amato, Francesca Scozzari: "Localizing Widening and Narrowing", SAS 2013. +// Example hybrid. https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loop-lit/as2013-hybrid.c + +#include +extern void abort(void); +//void reach_error() { assert(0); } +//void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } } + +int main() { + int i = 0; + while (1) { + i = i + 1; + int j = 0; + while (j < 10) { +// __VERIFIER_assert(0 <= i); +// __VERIFIER_assert(i <= 10); + bug: + j++; + } + if (i > 9) + i = 0; + } + return 0; +} diff --git a/tests/ctl/sv_comp/as2013-hybrid.json b/tests/ctl/sv_comp/as2013-hybrid.json new file mode 100644 index 00000000..db2da029 --- /dev/null +++ b/tests/ctl/sv_comp/as2013-hybrid.json @@ -0,0 +1,3 @@ +{ + "property": "AND{AG{AF{assert:0 > i}}{AF{assert: i > 10 }}}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/bh2017-ex-add.c b/tests/ctl/sv_comp/bh2017-ex-add.c new file mode 100644 index 00000000..c96590e2 --- /dev/null +++ b/tests/ctl/sv_comp/bh2017-ex-add.c @@ -0,0 +1,45 @@ +// Source: Rémy Boutonnet, Nicolas Halbwachs: "Improving the results of program analysis by abstract interpretation beyond the decreasing sequence", FMSD 2017. +// Example "additional". + +#include +extern void abort(void); +// void reach_error() { assert(0); } +// void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } } +extern _Bool __VERIFIER_nondet_bool(); + +int main() { + int m = 0; + int n = 0; + while (1) { + + //__VERIFIER_assert(m <= 60); + //__VERIFIER_assert(n <= 60); + assert1: + if (__VERIFIER_nondet_bool()) { + if (__VERIFIER_nondet_bool()) { + if (m < 60) { + m++; + } + else { + assert2: + //__VERIFIER_assert(m == 60); + m = 0; + } + } + } + if (__VERIFIER_nondet_bool()) { + if (__VERIFIER_nondet_bool()) { + if (n < 60) { + n++; + } + else { + //__VERIFIER_assert(n == 60); + assert3: + n = 0; + } + } + } + } + return 0; +} + diff --git a/tests/ctl/sv_comp/bh2017-ex-add.json b/tests/ctl/sv_comp/bh2017-ex-add.json new file mode 100644 index 00000000..a0953b82 --- /dev/null +++ b/tests/ctl/sv_comp/bh2017-ex-add.json @@ -0,0 +1,3 @@ +{ + "property": "AF{assert1: n <= 60}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/bhmr2007.c b/tests/ctl/sv_comp/bhmr2007.c new file mode 100644 index 00000000..37eb6b1e --- /dev/null +++ b/tests/ctl/sv_comp/bhmr2007.c @@ -0,0 +1,23 @@ +// Source: Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey +// Rybalchenko: "Path Invariants", PLDI 2007. + +#include "assert.h" +int main() { + + int i, n, a, b; + i = 0; a = 0; b = 0; n = __VERIFIER_nondet_int(); + if (!(n >= 0 && n <= 1000000)) return 0; + while (i < n) { + if (__VERIFIER_nondet_int()) { + a = a + 1; + b = b + 2; + } else { + a = a + 2; + b = b + 1; + } + i = i + 1; + } + assert1: + //__VERIFIER_assert(a + b == 3*n); + return 0; +} diff --git a/tests/ctl/sv_comp/bhmr2007.json b/tests/ctl/sv_comp/bhmr2007.json new file mode 100644 index 00000000..d2e60abe --- /dev/null +++ b/tests/ctl/sv_comp/bhmr2007.json @@ -0,0 +1,3 @@ +{ + "property": "AF{assert3:a + b == 3*n}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/cggmp2005.c b/tests/ctl/sv_comp/cggmp2005.c new file mode 100644 index 00000000..08bd03f0 --- /dev/null +++ b/tests/ctl/sv_comp/cggmp2005.c @@ -0,0 +1,18 @@ +// Source: A. Costan, S. Gaubert, E. Goubault, M. Martel, S. Putot: "A Policy +// Iteration Algorithm for Computing Fixed Points in Static Analysis of +// Programs", CAV 2005 + +#include "assert.h" + +int main() { + int i,j; + i = 1; + j = 10; + while (j >= i) { + i = i + 2; + j = -1 + j; + } + //__VERIFIER_assert(j == 6); + assert1: + return 0; +} diff --git a/tests/ctl/sv_comp/cggmp2005.json b/tests/ctl/sv_comp/cggmp2005.json new file mode 100644 index 00000000..7ba9b228 --- /dev/null +++ b/tests/ctl/sv_comp/cggmp2005.json @@ -0,0 +1,3 @@ +{ + "property": "AF{j == 6}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.json b/tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.json new file mode 100644 index 00000000..beeabacc --- /dev/null +++ b/tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.json @@ -0,0 +1,3 @@ +{ + "property": "AF{AND{AF{j >= 21}}{i==100}}" +} \ No newline at end of file diff --git a/tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.t2 b/tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.t2 deleted file mode 100755 index 01f76858..00000000 --- a/tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.t2 +++ /dev/null @@ -1,41 +0,0 @@ -// -CTL="[AF]([AF](j >= 21) && i == 100)" - -START: init; - -FROM: init; - c := 0; - i := 0; -TO: 1; - -FROM: 1; - assume(i < 100); -TO: 2; - -FROM: 2; - c := c + 1; - i := i + 1; -TO: 1; - -FROM: 1; - assume(i >= 100); -TO: 3; - -FROM: 3; - j := 5; -TO: 4; - -FROM: 4; - assume(j < 21); -TO: 5; - -FROM: 5; - c := c + 1; - j := j + 3; -TO: 4; - -FROM: 4; - assume(j >= 21); -TO: 6; - -FROM: 6; -TO: 6; diff --git a/tests/ctl/t2_cav13/P25.c b/tests/ctl/t2_cav13/P25.c index 3e4cdda3..699c1ceb 100644 --- a/tests/ctl/t2_cav13/P25.c +++ b/tests/ctl/t2_cav13/P25.c @@ -1,6 +1,6 @@ // OK // (varC <= 5) || ([AF](varR > 5)) -// -ctl "OR{varC <= 5}{AF{varR > 5}} +// -ctl_cfg "OR{varC <= 5}{AF{varR > 5}} // -joinbwd 6 void main() { diff --git a/tests/ctl/t2_cav13/P25.json b/tests/ctl/t2_cav13/P25.json new file mode 100644 index 00000000..cbd56212 --- /dev/null +++ b/tests/ctl/t2_cav13/P25.json @@ -0,0 +1,4 @@ +{ + "property": "OR{varC <= 5}{AF{varR > 5}}", + "joinbwd": 6 +} \ No newline at end of file diff --git a/tests/ctl/t2_cav13/P25.t2 b/tests/ctl/t2_cav13/P25.t2 deleted file mode 100644 index 371fbcd8..00000000 --- a/tests/ctl/t2_cav13/P25.t2 +++ /dev/null @@ -1,41 +0,0 @@ -//init(C,R,CS,PC):=C>=1,R=0,CS=8,PC=1. -//next(C,R,CS,PC,Cp,Rp,CSp,PCp):= -// PC=1,CS=<0,Cp=C,Rp=R,CSp=CS,PCp=2; -// PC=1,CS>0,Cp=C,Rp=R,CSp=CS,PCp=3; -// PC=3,C>=CS,Cp=C-1,Rp=R+1,CSp=CS-1,PCp=1; -// PC=3,C= 1); -varR := 0; -varCS := 8; -TO: loc1; - -FROM: loc1; -assume(varCS <= 0); -TO: loc2; - -FROM: loc1; -assume(varCS > 0); -TO: loc3; - -FROM: loc3; -assume(varC >= varCS); -varC := varC - 1; -varR := varR + 1; -varCS := varCS - 1; -TO: loc1; - -FROM: loc3; -assume(varC < varCS); -varC := varC - 1; -varR := varR + 1; -varCS := varCS - 1; -TO: loc1; - -FROM: loc3; -assume(varC < varCS); -varCS := varCS - 1; -TO: loc1; diff --git a/tests/ctl/t2_cav13/P26.c b/tests/ctl/t2_cav13/P26.c index fee0d58d..4328c1c4 100644 --- a/tests/ctl/t2_cav13/P26.c +++ b/tests/ctl/t2_cav13/P26.c @@ -3,7 +3,7 @@ // // (varC > 5) && [EG](varR <= 5) // -// -ctl "OR{varC > 5}{EG{varR <= 5}} +// -ctl_cfg "OR{varC > 5}{EG{varR <= 5}} void main() { int varC; // assume varC >= 1 diff --git a/tests/ctl/t2_cav13/P26.json b/tests/ctl/t2_cav13/P26.json new file mode 100644 index 00000000..0f3002b3 --- /dev/null +++ b/tests/ctl/t2_cav13/P26.json @@ -0,0 +1,3 @@ +{ + "property": "OR{varC > 5}{EG{varR <= 5}}" +} \ No newline at end of file diff --git a/tests/ctl/t2_cav13/P26.t2 b/tests/ctl/t2_cav13/P26.t2 deleted file mode 100644 index 8e67c849..00000000 --- a/tests/ctl/t2_cav13/P26.t2 +++ /dev/null @@ -1,41 +0,0 @@ -//init(C,R,CS,PC):=C>=1,R=0,CS=4,PC=1. -//next(C,R,CS,PC,Cp,Rp,CSp,PCp):= -// PC=1,CS=<0,Cp=C,Rp=R,CSp=CS,PCp=2; -// PC=1,CS>0,Cp=C,Rp=R,CSp=CS,PCp=3; -// PC=3,C>=CS,Cp=C-1,Rp=R+1,CSp=CS-1,PCp=1; -// PC=3,C= 1); -varR := 0; -varCS := 4; -TO: loc1; - -FROM: loc1; -assume(varCS <= 0); -TO: loc2; - -FROM: loc1; -assume(varCS > 0); -TO: loc3; - -FROM: loc3; -assume(varC >= varCS); -varC := varC - 1; -varR := varR + 1; -varCS := varCS - 1; -TO: loc1; - -FROM: loc3; -assume(varC < varCS); -varC := varC - 1; -varR := varR + 1; -varCS := varCS - 1; -TO: loc1; - -FROM: loc3; -assume(varC < varCS); -varCS := varCS - 1; -TO: loc1; diff --git a/tests/ctl/t2_cav13/P3.c b/tests/ctl/t2_cav13/P3.c index 4a57e713..7a2a2431 100644 --- a/tests/ctl/t2_cav13/P3.c +++ b/tests/ctl/t2_cav13/P3.c @@ -1,6 +1,6 @@ // NOK // -// -ctl "OR{varA != 1}{EF{varR==1}" +// -ctl_cfg "OR{varA != 1}{EF{varR==1}" // -precondition "varA == 0" diff --git a/tests/ctl/t2_cav13/P3.json b/tests/ctl/t2_cav13/P3.json new file mode 100644 index 00000000..48b4f6c1 --- /dev/null +++ b/tests/ctl/t2_cav13/P3.json @@ -0,0 +1,4 @@ +{ + "property": "OR{varA != 1}{EF{varR==1}}", + "precondition": "varA == 0" +} \ No newline at end of file diff --git a/tests/ctl/t2_cav13/P3.t2 b/tests/ctl/t2_cav13/P3.t2 deleted file mode 100644 index fe143c8f..00000000 --- a/tests/ctl/t2_cav13/P3.t2 +++ /dev/null @@ -1,43 +0,0 @@ -//init(A,R,N,PC):=A=0,R=0,PC=1. -//next(A,R,N,PC,Ap,Rp,Np,PCp):= -// PC=1,Ap=A,Rp=R,Np=N,PCp=5; -// PC=1,Ap=1,Rp=R,Np=N,PCp=2; -// PC=2,Ap=0,Rp=R,Np=N,PCp=3; -// PC=3,Ap=A,Rp=R,Np=N,PCp=3; -// PC=3,Ap=A,Rp=1,Np=N,PCp=4; -// PC=4,Ap=A,Rp=0,Np=N,PCp=1. - -//init(A,R,N,PC):=A=0,R=0,PC=1. -START: init; -FROM: init; -varA := 0; -varR := 0; -TO: loc1; - -// PC=1,Ap=A,Rp=R,Np=N,PCp=5; -FROM: loc1; -TO: loc5; - -// PC=1,Ap=1,Rp=R,Np=N,PCp=2; -FROM: loc1; -varA := 1; -TO: loc2; - -// PC=2,Ap=0,Rp=R,Np=N,PCp=3; -FROM: loc2; -varA := 0; -TO: loc3; - -// PC=3,Ap=A,Rp=R,Np=N,PCp=3; -FROM: loc3; -TO: loc3; - -// PC=3,Ap=A,Rp=1,Np=N,PCp=4; -FROM: loc3; -varR := 1; -TO: loc4; - -// PC=4,Ap=A,Rp=0,Np=N,PCp=1. -FROM: loc4; -varR := 0; -TO: loc1; diff --git a/tests/ctl/t2_cav13/P3_cheat.c b/tests/ctl/t2_cav13/P3_cheat.c index 51f11110..8477074d 100644 --- a/tests/ctl/t2_cav13/P3_cheat.c +++ b/tests/ctl/t2_cav13/P3_cheat.c @@ -2,7 +2,7 @@ // // // '[AG](varA != 1 || [EF](varR == 1))' -// -ctl "OR{varA != 1}{EF{varR==1}" +// -ctl_cfg "OR{varA != 1}{EF{varR==1}" // -precondition "varA == 0 && varR == 0" // diff --git a/tests/ctl/t2_cav13/P3_cheat.json b/tests/ctl/t2_cav13/P3_cheat.json new file mode 100644 index 00000000..0a3a752d --- /dev/null +++ b/tests/ctl/t2_cav13/P3_cheat.json @@ -0,0 +1,4 @@ +{ + "property": "OR{varA != 1}{EF{varR==1}}", + "precondition": "varA == 0 && varR == 0" +} \ No newline at end of file diff --git a/tests/ctl/t2_cav13/P4.c b/tests/ctl/t2_cav13/P4.c index fb9932e0..93db8084 100644 --- a/tests/ctl/t2_cav13/P4.c +++ b/tests/ctl/t2_cav13/P4.c @@ -1,6 +1,6 @@ // OK // -precondition "varN > 0" -// -ctl "EF{AND{varA == 1}{AG{varR != 1}}" +// -ctl_cfg "EF{AND{varA == 1}{AG{varR != 1}}" void main() { diff --git a/tests/ctl/t2_cav13/P4.json b/tests/ctl/t2_cav13/P4.json new file mode 100644 index 00000000..b88c066a --- /dev/null +++ b/tests/ctl/t2_cav13/P4.json @@ -0,0 +1,4 @@ +{ + "property": "EF{AND{varA == 1}{AG{varR != 1}}}", + "precondition": "varN > 0" +} \ No newline at end of file diff --git a/tests/ctl/t2_cav13/P4.t2 b/tests/ctl/t2_cav13/P4.t2 deleted file mode 100644 index e69de29b..00000000 diff --git a/tests/ctl/until_existential.c b/tests/ctl/until_existential.c index ec4e8b7d..687fc165 100644 --- a/tests/ctl/until_existential.c +++ b/tests/ctl/until_existential.c @@ -6,7 +6,7 @@ int main() { int x; int y; - if (?) { + if (rand()){ // loop invariant: x >= y while (x > y) { x = x - 1; diff --git a/tests/ctl/until_existential.json b/tests/ctl/until_existential.json new file mode 100644 index 00000000..0b016952 --- /dev/null +++ b/tests/ctl/until_existential.json @@ -0,0 +1,5 @@ +{ + "property": "EU{x >= y}{x == y}", + "precondition": "x > y", + "domain":"polyhedra" +} \ No newline at end of file diff --git a/tests/ctl/until_existential.t2 b/tests/ctl/until_existential.t2 deleted file mode 100644 index a5457032..00000000 --- a/tests/ctl/until_existential.t2 +++ /dev/null @@ -1,39 +0,0 @@ -///*** 1_main ***/// -// [EU] (x >= y), (x == y)" - -START: 1; - -FROM: 1; - y := nondet(); - x := nondet(); - assume(x > y); -TO: 2; - - -FROM: 2; -TO: 7; - -FROM: 7; - x := y - 1; -TO: 8; - -FROM: 8; -TO: 6; - -FROM: 2; -TO: 3; - -FROM: 3; - assume(x > y); -TO: 4; - -FROM: 3; - assume(x <= y); -TO: 5; - -FROM: 4; - x := x - 1; -TO: 3; - -FROM: 5; -TO: 6; diff --git a/tests/ctl/until_test.json b/tests/ctl/until_test.json new file mode 100644 index 00000000..8c3ecefb --- /dev/null +++ b/tests/ctl/until_test.json @@ -0,0 +1,5 @@ +{ + "property": "AU{x >= y}{x == y}", + "precondition": "x == y + 20", + "domain":"polyhedra" +} \ No newline at end of file diff --git a/tests/ctl/until_test.ltl.c b/tests/ctl/until_test.ltl.c deleted file mode 100644 index 987e6f2b..00000000 --- a/tests/ctl/until_test.ltl.c +++ /dev/null @@ -1,16 +0,0 @@ -//#Safe -//@ ltl invariant positive: (AP(x >= y) U AP(x == y)); - -int y; -int x; - -int main() { - - // assume x > y - x = y + 10000; - - while (x > y) { - x = x - 1; - } - // now x == y -} diff --git a/tests/ctl/until_test.t2 b/tests/ctl/until_test.t2 deleted file mode 100644 index 9c8eaef7..00000000 --- a/tests/ctl/until_test.t2 +++ /dev/null @@ -1,25 +0,0 @@ -///*** 1_main ***/// -// [AF](x >= y) && [AW] (x >= y), (x == y)" - - -START: 1; - -FROM: 1; - y := nondet(); - x := nondet(); - assume(x > y); -TO: 2; - -FROM: 2; -TO: 3; -FROM: 3; - assume(x > y); -TO: 4; -FROM: 3; - assume(x <= y); -TO: 5; -FROM: 4; - x := x - 1; -TO: 3; -FROM: 5; -TO: 6; diff --git a/tests/termination/boolean.c b/tests/termination/boolean.c index b363f7d9..9ae1bae6 100644 --- a/tests/termination/boolean.c +++ b/tests/termination/boolean.c @@ -8,7 +8,7 @@ suggested parameters: */ int main() { - int x; + int x = 10; while (x) { if (x > 0) { x = x - 1; diff --git a/tests/termination/boolean.json b/tests/termination/boolean.json new file mode 100644 index 00000000..42a44427 --- /dev/null +++ b/tests/termination/boolean.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain":"polyhedra" +} diff --git a/tests/termination/cacm2009a.c b/tests/termination/cacm2009a.c index b6e7e5a0..371b25a4 100644 --- a/tests/termination/cacm2009a.c +++ b/tests/termination/cacm2009a.c @@ -7,10 +7,11 @@ suggested parameters: - backward widening delay = 2 [default] */ + void main() { - int x, y; + int x, y,b; while (x > 0 && y > 0) - if (?) { + if (b) { x = x - 1; y = y + 1; } else diff --git a/tests/termination/cacm2009a.json b/tests/termination/cacm2009a.json new file mode 100644 index 00000000..42a44427 --- /dev/null +++ b/tests/termination/cacm2009a.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain":"polyhedra" +} diff --git a/tests/termination/cacm2009b.c b/tests/termination/cacm2009b.c index e3e8c115..add915ce 100644 --- a/tests/termination/cacm2009b.c +++ b/tests/termination/cacm2009b.c @@ -7,12 +7,19 @@ suggested parameters: - backward widening delay = 3 */ -void main() { +int f() { int x, y; while (x > 0 && y > 0) - if (?) { + if (rand()) { x = x - 1; - y = ?; + y = rand(); } else y = y - 1; + + return 1; +} + + +int main() { + return f(); } \ No newline at end of file diff --git a/tests/termination/cacm2009b.json b/tests/termination/cacm2009b.json new file mode 100644 index 00000000..42a44427 --- /dev/null +++ b/tests/termination/cacm2009b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain":"polyhedra" +} diff --git a/tests/termination/cav2006.c b/tests/termination/cav2006.c index c564b04b..81e16438 100644 --- a/tests/termination/cav2006.c +++ b/tests/termination/cav2006.c @@ -9,7 +9,6 @@ suggested parameters: void main() { int x, y; - while (x >= 0) { if (y <= 50) x = x + 1; diff --git a/tests/termination/cav2006.json b/tests/termination/cav2006.json new file mode 100644 index 00000000..a0cacf81 --- /dev/null +++ b/tests/termination/cav2006.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain":"boxes" +} diff --git a/tests/termination/cda0.c b/tests/termination/cda0.c deleted file mode 100644 index b10e635c..00000000 --- a/tests/termination/cda0.c +++ /dev/null @@ -1,31 +0,0 @@ -int step(int x ){ - if ( x > 20 ){ - return 3; - } - else if ( x > 10) { - return 2; - - }else { - return 1; - - } -} - - -int main () { - int y; int i; - if (y > 0 ){ - i = - step(y); - }else { - i = step(-y); - } - - while( y < -3 || y > 3 ){ - y = y + i; - } - - - - - return 0 ; -} \ No newline at end of file diff --git a/tests/termination/countdown.c b/tests/termination/countdown.c deleted file mode 100644 index 34e1b7ac..00000000 --- a/tests/termination/countdown.c +++ /dev/null @@ -1,19 +0,0 @@ -/* from Urban Miné VMCAI 2015 paper -GUARANTEE/RECURRENCE (x == 0) - -suggested parameters: -- partition abstract domain = boxes [default] -- function abstract domain = affine [default] -- backward widening delay = 2 [default] -*/ - -void main() { - int x, c = 1; - while (true) { - x = c; - while (x > 0) { - x = x - 1; - c = c + 1; - } - } -} \ No newline at end of file diff --git a/tests/termination/countdown_recurrence.actl b/tests/termination/countdown_recurrence.actl deleted file mode 100644 index f4fe9cef..00000000 --- a/tests/termination/countdown_recurrence.actl +++ /dev/null @@ -1 +0,0 @@ -AG{AF{x == 0}} diff --git a/tests/termination/euclid.c b/tests/termination/euclid.c index 7db96829..d728500e 100644 --- a/tests/termination/euclid.c +++ b/tests/termination/euclid.c @@ -16,4 +16,5 @@ int main() { else y = y - x; return x; + } diff --git a/tests/termination/euclid.json b/tests/termination/euclid.json new file mode 100644 index 00000000..ca5611e9 --- /dev/null +++ b/tests/termination/euclid.json @@ -0,0 +1,6 @@ +{ + "property":"AF{exit:true}", + "precondition":"x > 0 && y > 0", + "domain":"polyhedra" + +} diff --git a/tests/termination/example0.json b/tests/termination/example0.json new file mode 100644 index 00000000..6b952972 --- /dev/null +++ b/tests/termination/example0.json @@ -0,0 +1,4 @@ +{ + "property": "AF{exit:true}", + "precondition": "x > 10" +} diff --git a/tests/termination/example1.c b/tests/termination/example1.c index 59b989ea..e702c57c 100644 --- a/tests/termination/example1.c +++ b/tests/termination/example1.c @@ -9,7 +9,6 @@ suggested parameters: int main() { int x; - while (x <= 10) - x = x + 1; + while (x <= 10) x = x + 1; return 0; } \ No newline at end of file diff --git a/tests/termination/example1.json b/tests/termination/example1.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example1.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example10.c b/tests/termination/example10.c index 595f4ad8..e96a4042 100755 --- a/tests/termination/example10.c +++ b/tests/termination/example10.c @@ -11,17 +11,17 @@ int main() { int x1, x2; while (x1 != 0 && x2 > 0) if (x1 > 0) { - if (?) { + if (rand()) { x1 = x1 - 1; - x2 = ?; + x2 = rand(); } else x2 = x2 - 1; } else { - if (?) + if (rand()) x1 = x1 + 1; else { x2 = x2 - 1; - x1 = ?; + x1 = rand(); } } return 0; diff --git a/tests/termination/example10.json b/tests/termination/example10.json new file mode 100644 index 00000000..a4d95bfc --- /dev/null +++ b/tests/termination/example10.json @@ -0,0 +1 @@ +{"property":"AF{exit:true}"} diff --git a/tests/termination/example1a.c b/tests/termination/example1a.c index 2176b5c1..03e79d07 100644 --- a/tests/termination/example1a.c +++ b/tests/termination/example1a.c @@ -18,7 +18,7 @@ int main() { if (y > 0) { step = -step; } - while(y < -1 || y > 1) { + while(y < 1 || y > 1) { y = y + step; } return 0; diff --git a/tests/termination/example1a.json b/tests/termination/example1a.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example1a.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example1b.json b/tests/termination/example1b.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example1b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example1c.json b/tests/termination/example1c.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example1c.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example1d.json b/tests/termination/example1d.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example1d.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example1e.json b/tests/termination/example1e.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example1e.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example2.json b/tests/termination/example2.json new file mode 100644 index 00000000..adafad9a --- /dev/null +++ b/tests/termination/example2.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra", + "ordinals": 3 +} diff --git a/tests/termination/example2a.json b/tests/termination/example2a.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example2a.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example2b.json b/tests/termination/example2b.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example2b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example2c.json b/tests/termination/example2c.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example2c.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example2d.json b/tests/termination/example2d.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example2d.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example2e.json b/tests/termination/example2e.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/example2e.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/example5.json b/tests/termination/example5.json new file mode 100644 index 00000000..8eaf5451 --- /dev/null +++ b/tests/termination/example5.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x > 10", + "domain": "boxes" +} diff --git a/tests/termination/example7.json b/tests/termination/example7.json new file mode 100644 index 00000000..a19ccfd5 --- /dev/null +++ b/tests/termination/example7.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x > 6", + "domain": "polyhedra" +} diff --git a/tests/termination/example8.c b/tests/termination/example8.c index 4db25ea8..f386b92c 100644 --- a/tests/termination/example8.c +++ b/tests/termination/example8.c @@ -8,9 +8,9 @@ suggested parameters: */ int main() { - int x = ?; + int x = rand(); while (x <= 100) { - if (?) + if (rand()) x = -2 * x + 2; else x = -3 * x - 2; diff --git a/tests/termination/example8.json b/tests/termination/example8.json new file mode 100644 index 00000000..af2ee12d --- /dev/null +++ b/tests/termination/example8.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "joinbwd": 7, + "domain": "polyhedra" +} diff --git a/tests/termination/gen.bash b/tests/termination/gen.bash new file mode 100644 index 00000000..908270a4 --- /dev/null +++ b/tests/termination/gen.bash @@ -0,0 +1,7 @@ +yourfilenames=`ls ./*.c` +for eachfile in $yourfilenames +do + base=$(basename "$eachfile" .c) + json="${base}.json" + echo '{"property":"AF{exit:true}"}' > "$json" +done diff --git a/tests/termination/increment_one.c b/tests/termination/increment_one.c new file mode 100644 index 00000000..59b989ea --- /dev/null +++ b/tests/termination/increment_one.c @@ -0,0 +1,15 @@ +/* +TERMINATION + +suggested parameters: +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int main() { + int x; + while (x <= 10) + x = x + 1; + return 0; +} \ No newline at end of file diff --git a/tests/termination/increment_one.json b/tests/termination/increment_one.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/increment_one.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/increment_two_a.c b/tests/termination/increment_two_a.c new file mode 100644 index 00000000..b38d739b --- /dev/null +++ b/tests/termination/increment_two_a.c @@ -0,0 +1,18 @@ +/* +TERMINATION for x > 10 OR (x <= 10 AND x odd) + +suggested parameters: +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int main() { + int x; + while (x <= 10) { + if (x <= 9) { + x = x + 2; + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/increment_two_a.json b/tests/termination/increment_two_a.json new file mode 100644 index 00000000..5ef6f3a8 --- /dev/null +++ b/tests/termination/increment_two_a.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x > 10", + "domain": "polyhedra" +} diff --git a/tests/termination/increment_two_b.c b/tests/termination/increment_two_b.c new file mode 100644 index 00000000..fc657b4c --- /dev/null +++ b/tests/termination/increment_two_b.c @@ -0,0 +1,18 @@ +/* +TERMINATION for x > 6 + +suggested parameters: +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int main() { + int x; + while (x <= 10) { + if (x > 6) { + x = x + 2; + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/increment_two_b.json b/tests/termination/increment_two_b.json new file mode 100644 index 00000000..a19ccfd5 --- /dev/null +++ b/tests/termination/increment_two_b.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x > 6", + "domain": "polyhedra" +} diff --git a/tests/termination/issue8.json b/tests/termination/issue8.json new file mode 100644 index 00000000..77247c02 --- /dev/null +++ b/tests/termination/issue8.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "y >= 1", + "domain": "polyhedra" +} diff --git a/tests/termination/mccarthy91.c b/tests/termination/mccarthy91.c index 319b93a2..4553ec1e 100644 --- a/tests/termination/mccarthy91.c +++ b/tests/termination/mccarthy91.c @@ -1,8 +1,6 @@ int main() { - int x1; int x2; - x1 = 1; - x2 = 1; + int x1, x2 = 1; while (x2 >= 1) { if (x1 > 100) { x1 = x1 - 10; @@ -12,5 +10,6 @@ int main() { x2 = x2 + 1; } } + exit: return x2; } \ No newline at end of file diff --git a/tests/termination/mccarthy91.json b/tests/termination/mccarthy91.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/mccarthy91.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/mine.c b/tests/termination/mine.c deleted file mode 100644 index ced4e7bb..00000000 --- a/tests/termination/mine.c +++ /dev/null @@ -1,26 +0,0 @@ -int main(){ - int y ; - int z ; - int w ; - int x ; - int k ; - while( x + y + w > 0 ){ - y = k + z ; - x = x - w ; - if ( x < 0 ){ - k = k +1 ; - } - else { - - k = k + 1; - } - if( k > z ){ - z = z + 2 + x ; - }else - { - z = z + 1 ; - } - - - } -} diff --git a/tests/termination/multiply_two.c b/tests/termination/multiply_two.c new file mode 100644 index 00000000..17810902 --- /dev/null +++ b/tests/termination/multiply_two.c @@ -0,0 +1,15 @@ +/* +TERMINATION for x > 0 + +suggested parameters: +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 5 +*/ + +int main() { + int x; + while (x < 10) + x = 2 * x; + return 0; +} \ No newline at end of file diff --git a/tests/termination/multiply_two.json b/tests/termination/multiply_two.json new file mode 100644 index 00000000..a13a0122 --- /dev/null +++ b/tests/termination/multiply_two.json @@ -0,0 +1,6 @@ +{ + "property":"AF{exit:true}", + "precondition": "x > 0", + "joinbwd": 5, + "domain": "polyhedra" +} diff --git a/tests/termination/postdecrement.json b/tests/termination/postdecrement.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/postdecrement.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/postincrement.json b/tests/termination/postincrement.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/postincrement.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/predecrement.json b/tests/termination/predecrement.json new file mode 100644 index 00000000..a4d95bfc --- /dev/null +++ b/tests/termination/predecrement.json @@ -0,0 +1 @@ +{"property":"AF{exit:true}"} diff --git a/tests/termination/preincrement.json b/tests/termination/preincrement.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/preincrement.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/recursion.c b/tests/termination/recursion.c index 5dcc3e21..20e2695e 100644 --- a/tests/termination/recursion.c +++ b/tests/termination/recursion.c @@ -6,11 +6,14 @@ suggested parameters: - function abstract domain = affine [default] - backward widening delay = 2 [default] */ - -int main(int x) { +int f(int x); +int f(int x){ if (x <= 0) { return 0; } else { - main(x - 1); - } + f(x - 1); + }} +int main(int x) { + f(x); + return 1; } \ No newline at end of file diff --git a/tests/termination/recursion.json b/tests/termination/recursion.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/recursion.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/sas2010.c b/tests/termination/sas2010.c index 498213b5..54c86cfa 100644 --- a/tests/termination/sas2010.c +++ b/tests/termination/sas2010.c @@ -10,8 +10,8 @@ suggested parameters: int main() { int x1, x2; while (x1 >= 0 && x2 >= 0) { - if (?) { - while (x2 <= 10 && ?) { + if (rand()){ + while (x2 <= 10 && rand()) { x2 = x2 + 1; } x1 = x1 - 1; diff --git a/tests/termination/sas2010.json b/tests/termination/sas2010.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/sas2010.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/sas2014a.json b/tests/termination/sas2014a.json new file mode 100644 index 00000000..d78f630b --- /dev/null +++ b/tests/termination/sas2014a.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "r <= 0", + "domain": "polyhedra" +} diff --git a/tests/termination/sas2014b.json b/tests/termination/sas2014b.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/sas2014b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/sas2014c.json b/tests/termination/sas2014c.json new file mode 100644 index 00000000..f5aca780 --- /dev/null +++ b/tests/termination/sas2014c.json @@ -0,0 +1,3 @@ +{ + "property":"AF{exit:true}" +} diff --git a/tests/termination/sorting4.json b/tests/termination/sorting4.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/sorting4.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_1a.c b/tests/termination/squeez_interval_1a.c new file mode 100644 index 00000000..dd793ed5 --- /dev/null +++ b/tests/termination/squeez_interval_1a.c @@ -0,0 +1,23 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + + +int main() { + int y, step; + step = 1; + if (y > 0) { + step = -step; + } + while(y < -1 || y > 1) { + y = y + step; + } + exit: + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_1a.json b/tests/termination/squeez_interval_1a.json new file mode 100644 index 00000000..a4d95bfc --- /dev/null +++ b/tests/termination/squeez_interval_1a.json @@ -0,0 +1 @@ +{"property":"AF{exit:true}"} diff --git a/tests/termination/squeez_interval_1b.c b/tests/termination/squeez_interval_1b.c new file mode 100644 index 00000000..ba29959d --- /dev/null +++ b/tests/termination/squeez_interval_1b.c @@ -0,0 +1,32 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + + +int main() { + int y, step; + if (y > 0) { + if (y > 10) { + step = -2; + }else { + step = -1; + } + } else { + if (y < -10) { + step = 2; + }else { + step = 1; + } + } + while(y < -2 || y > 2) { + y = y + step; + } + exit: + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_1b.json b/tests/termination/squeez_interval_1b.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_1b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_1c.c b/tests/termination/squeez_interval_1c.c new file mode 100644 index 00000000..eb2fb30f --- /dev/null +++ b/tests/termination/squeez_interval_1c.c @@ -0,0 +1,32 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 20) { + return 3; + } else if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, step; + if (y > 0) { + step = -get_step(y); + } else { + step = get_step(-y); + } + while(y < -3 || y > 3) { + y = y + step; + } + exit: + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_1c.json b/tests/termination/squeez_interval_1c.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_1c.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_1d.c b/tests/termination/squeez_interval_1d.c new file mode 100644 index 00000000..e6252f64 --- /dev/null +++ b/tests/termination/squeez_interval_1d.c @@ -0,0 +1,33 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 30) { + return 4; + } else if (x > 20) { + return 3; + } else if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, step; + if (y > 0) { + step = -get_step(y); + } else { + step = get_step(-y); + } + while(y < -4 || y > 4) { + y = y + step; + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_1d.json b/tests/termination/squeez_interval_1d.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_1d.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_1e.c b/tests/termination/squeez_interval_1e.c new file mode 100644 index 00000000..a29c5954 --- /dev/null +++ b/tests/termination/squeez_interval_1e.c @@ -0,0 +1,35 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 40) { + return 5; + } else if (x > 30) { + return 4; + } else if (x > 20) { + return 3; + } else if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, step; + if (y > 0) { + step = -get_step(y); + } else { + step = get_step(-y); + } + while(y < -5 || y > 5) { + y = y + step; + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_1e.json b/tests/termination/squeez_interval_1e.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_1e.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_2a.c b/tests/termination/squeez_interval_2a.c new file mode 100644 index 00000000..f58ab1ba --- /dev/null +++ b/tests/termination/squeez_interval_2a.c @@ -0,0 +1,25 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int main() { + int x, y; + while (y< -2 || y > 2) { + if (y < 0 && x > 10) { + y = y + 2; + } else if (y < 0 && x <= 10){ + y = y + 1; + } else if (y >= 0 && x > 10){ + y = y - 2; + } else if (y >= 0 && x <= 10){ + y = y - 1; + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_2a.json b/tests/termination/squeez_interval_2a.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_2a.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_2b.c b/tests/termination/squeez_interval_2b.c new file mode 100644 index 00000000..79ba39b6 --- /dev/null +++ b/tests/termination/squeez_interval_2b.c @@ -0,0 +1,21 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int main() { + int y; + while (y< -1 || y > 1) { + if (y < 0) { + y = y + 1; + } else { + y = y - 1; + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_2b.json b/tests/termination/squeez_interval_2b.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_2b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_2c.c b/tests/termination/squeez_interval_2c.c new file mode 100644 index 00000000..9eebabcb --- /dev/null +++ b/tests/termination/squeez_interval_2c.c @@ -0,0 +1,29 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, x, step; + x = y; + while(y < -2 || y > 2) { + if (x > 0) { + y = y - get_step(x); + } else { + y = y + get_step(-x); + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_2c.json b/tests/termination/squeez_interval_2c.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_2c.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_2d.c b/tests/termination/squeez_interval_2d.c new file mode 100644 index 00000000..f93894ad --- /dev/null +++ b/tests/termination/squeez_interval_2d.c @@ -0,0 +1,31 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 20) { + return 3; + } else if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, x, step; + x = y; + while(y < -3 || y > 3) { + if (x > 0) { + y = y - get_step(x); + } else { + y = y + get_step(-x); + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_2d.json b/tests/termination/squeez_interval_2d.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_2d.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_2e.c b/tests/termination/squeez_interval_2e.c new file mode 100644 index 00000000..31407028 --- /dev/null +++ b/tests/termination/squeez_interval_2e.c @@ -0,0 +1,33 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 30) { + return 4; + } else if (x > 20) { + return 3; + } else if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, x, step; + x = y; + while(y < -4 || y > 4) { + if (x > 0) { + y = y - get_step(x); + } else { + y = y + get_step(-x); + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_2e.json b/tests/termination/squeez_interval_2e.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_2e.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/squeez_interval_2f.c b/tests/termination/squeez_interval_2f.c new file mode 100644 index 00000000..952d6da3 --- /dev/null +++ b/tests/termination/squeez_interval_2f.c @@ -0,0 +1,35 @@ +/* +TERMINATION + +suggested parameters: +- conflict-driven conditional termination +- partition abstract domain = boxes [default] +- function abstract domain = affine [default] +- backward widening delay = 2 [default] +*/ + +int get_step(int x) { + if (x > 40) { + return 5; + } else if (x > 30) { + return 4; + } else if (x > 20) { + return 3; + } else if (x > 10) { + return 2; + } + return 1; +} + +int main() { + int y, x, step; + x = y; + while( x <= -4 || x >= 4) { + if (x > 0) { + y = y - get_step(x); + } else { + y = y + get_step(-x); + } + } + return 0; +} \ No newline at end of file diff --git a/tests/termination/squeez_interval_2f.json b/tests/termination/squeez_interval_2f.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/squeez_interval_2f.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/tacas2013a.json b/tests/termination/tacas2013a.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/tacas2013a.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/tacas2013b.json b/tests/termination/tacas2013b.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/tacas2013b.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/tacas2013c.c b/tests/termination/tacas2013c.c index 7f4291a3..8ad71de8 100755 --- a/tests/termination/tacas2013c.c +++ b/tests/termination/tacas2013c.c @@ -10,11 +10,11 @@ suggested parameters: int main() { int x1, x2, x3; while (x1 > 0 && x2 > 0 && x3 > 0) - if (?) { + if (rand()){ x1 = x1 - 1; - x3 = ?; + x3 = rand(); } else { - x1 = ?; + x1 = rand(); x2 = x2 - 1; x3 = x3 - 1; } diff --git a/tests/termination/tacas2013c.json b/tests/termination/tacas2013c.json new file mode 100644 index 00000000..4d0e9373 --- /dev/null +++ b/tests/termination/tacas2013c.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "joinbwd": 3, + "domain": "polyhedra" +} diff --git a/tests/termination/tacas2013d.c b/tests/termination/tacas2013d.c index e6100ebc..4ef3448f 100755 --- a/tests/termination/tacas2013d.c +++ b/tests/termination/tacas2013d.c @@ -10,14 +10,14 @@ suggested parameters: int main() { int x1, x2, x3; while (x1 > 0 && x2 > 0 && x3 > 0) - if (?) { + if (rand()){ x1 = x1 - 1; - } else if (?) { + }else if (rand()){ x2 = x2 - 1; - x3 = ?; + x3 = rand(); } else { x3 = x3 - 1; - x1 = ?; + x1 = rand(); } return 0; } \ No newline at end of file diff --git a/tests/termination/tacas2013d.json b/tests/termination/tacas2013d.json new file mode 100644 index 00000000..4d0e9373 --- /dev/null +++ b/tests/termination/tacas2013d.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "joinbwd": 3, + "domain": "polyhedra" +} diff --git a/tests/termination/tap2008a.json b/tests/termination/tap2008a.json new file mode 100644 index 00000000..575559c2 --- /dev/null +++ b/tests/termination/tap2008a.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition":"x < 25", + "domain": "polyhedra" +} diff --git a/tests/termination/tap2008b.json b/tests/termination/tap2008b.json new file mode 100644 index 00000000..972c2a4b --- /dev/null +++ b/tests/termination/tap2008b.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x > 35", + "domain": "polyhedra" +} diff --git a/tests/termination/tap2008c.json b/tests/termination/tap2008c.json new file mode 100644 index 00000000..d33d18ce --- /dev/null +++ b/tests/termination/tap2008c.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x < 30", + "domain": "polyhedra" +} diff --git a/tests/termination/tap2008d.json b/tests/termination/tap2008d.json new file mode 100644 index 00000000..747baf69 --- /dev/null +++ b/tests/termination/tap2008d.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x <= 0", + "domain": "polyhedra" +} diff --git a/tests/termination/tap2008e.json b/tests/termination/tap2008e.json new file mode 100644 index 00000000..4a8bad94 --- /dev/null +++ b/tests/termination/tap2008e.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x <= 11", + "domain": "polyhedra" +} diff --git a/tests/termination/tap2008f.json b/tests/termination/tap2008f.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/tap2008f.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/vijay.c b/tests/termination/vijay.c index c45cda21..26effc37 100644 --- a/tests/termination/vijay.c +++ b/tests/termination/vijay.c @@ -23,4 +23,4 @@ int main() { y = y + x; } return 0; -} +} \ No newline at end of file diff --git a/tests/termination/vijay.json b/tests/termination/vijay.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/vijay.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/vmcai2004a.json b/tests/termination/vmcai2004a.json new file mode 100644 index 00000000..19fd2c36 --- /dev/null +++ b/tests/termination/vmcai2004a.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "joinbwd": 5, + "domain": "boxes" +} diff --git a/tests/termination/vmcai2004b.json b/tests/termination/vmcai2004b.json new file mode 100644 index 00000000..19fd2c36 --- /dev/null +++ b/tests/termination/vmcai2004b.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "joinbwd": 5, + "domain": "boxes" +} diff --git a/tests/termination/widening1.json b/tests/termination/widening1.json new file mode 100644 index 00000000..a4d95bfc --- /dev/null +++ b/tests/termination/widening1.json @@ -0,0 +1 @@ +{"property":"AF{exit:true}"} diff --git a/tests/termination/widening2.json b/tests/termination/widening2.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/widening2.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/termination/widening3.json b/tests/termination/widening3.json new file mode 100644 index 00000000..747baf69 --- /dev/null +++ b/tests/termination/widening3.json @@ -0,0 +1,5 @@ +{ + "property":"AF{exit:true}", + "precondition": "x <= 0", + "domain": "polyhedra" +} diff --git a/tests/termination/zune.c b/tests/termination/zune.c index 23881606..3ad5740b 100644 --- a/tests/termination/zune.c +++ b/tests/termination/zune.c @@ -1,17 +1,16 @@ /* http://techcrunch.com/2008/12/31/zune-bug-explained-in-detail/ suggested parameters: -- conflict-driven analysis 3 - partition abstract domain = boxes [default] - function abstract domain = affine [default] - backward widening delay = 2 [default] */ int main() { - int days; - int year = 1980; + int days, year = 1980; + int isLeapYear; while (days > 365) { - if ( isLeapYear(year) ) { + if ( isLeapYear ) { if (days > 366) { days -= 366; year += 1; @@ -22,7 +21,4 @@ int main() { } } return 0; -} - - - +} \ No newline at end of file diff --git a/tests/termination/zune.json b/tests/termination/zune.json new file mode 100644 index 00000000..5013adac --- /dev/null +++ b/tests/termination/zune.json @@ -0,0 +1,4 @@ +{ + "property":"AF{exit:true}", + "domain": "polyhedra" +} diff --git a/tests/test.c b/tests/test.c new file mode 100644 index 00000000..0bfd562a --- /dev/null +++ b/tests/test.c @@ -0,0 +1,9 @@ +int main(){ + int x , y; + while ( x > 0 ){ + x = x - 1; + } + y = 3; + return 1; + +} \ No newline at end of file diff --git a/utils/Config.ml b/utils/Config.ml new file mode 100644 index 00000000..3bc21da7 --- /dev/null +++ b/utils/Config.ml @@ -0,0 +1,79 @@ +let joinbwd = ref 2 +let joinfwd = ref 2 +let learn = ref false (* conflict-driven conditional termination *) +let meetbwd = ref 2 +let version = ref false +let minimal = ref false +let refine = ref false +let retrybwd = ref 5 +let analysis = ref "termination" +let domain = ref "boxes" +let filename = ref "" +let main = ref "main" +let minimal = ref false +let compress = ref false (* false *) +let ordinals = ref false +let ordmax = ref 2 +let cda = ref false +let cdamax = ref 0 +let property = ref "" +let precondition = ref "true" +let time = ref true +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 vulnerability = ref false +let resilience = ref false +let nowrap = ref false + +let robust = ref false +exception Abort +exception Timeout + +let json_output = ref false +let output_dir = ref "logs/" +let exectime = ref "1" +let ctltype = ref "" +let logfile = ref "" +let result = ref false +let f_log = ref stdout +let tree : Yojson.Safe.t ref = ref `Null +let vuln_res : Yojson.Safe.t ref = ref @@ `String "Not analyzed" + +let from_json filename = + let json = Yojson.Safe.from_file filename in + let rec aux (json : Yojson.Safe.t) = + match json with + | `Assoc [] -> () + | `Assoc (("analysis", `String a) :: q) -> + analysis := a; + aux (`Assoc q) + | `Assoc (("property", `String a) :: q) -> + property := a; + aux (`Assoc q) + | `Assoc (("domain", `String a) :: q) -> + domain := a; + aux (`Assoc q) + | `Assoc (("precondition", `String a) :: q) -> + precondition := a; + aux (`Assoc q) + | `Assoc (("ordinals", `Int i) :: q) -> + ordmax := i; + ordinals := true; + aux (`Assoc q) + | `Assoc (("joinbwd", `Int i) :: q) -> + joinbwd := i; + aux (`Assoc q) + | _ -> raise (Invalid_argument "Wrong config json format.") + in + aux json diff --git a/utils/Regression.ml b/utils/Regression.ml new file mode 100644 index 00000000..2c4d1104 --- /dev/null +++ b/utils/Regression.ml @@ -0,0 +1,67 @@ +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 !Config.ordmax else "") + ^ (if !refine then "-refine" else "") + ^ (if !vulnerability then "-vulnerability" else "") + ^ ".out" + in + Config.logfile := name + +let json_string filename analysis property precondition result domain joinbwd + time = + Printf.sprintf + {| + {"filename" : "%s", + "analysis_type": "%s", + "property": "%s", + "precondition": "%s", + "result": "%s", + "domain": "%s", + "joinbwd": %d, + "time": "%s" + }|} + filename analysis property precondition result domain joinbwd time + +let output_json () = + if !Config.resilience then Config.analysis := !analysis ^ "-resilience"; + let dirname = !output_dir ^ Filename.dirname !filename in + let rec mkdir_p filename = + let parent_dir = Filename.dirname filename in + if not (Sys.file_exists parent_dir) then mkdir_p parent_dir + else Unix.mkdir filename 0o755 + in + if not (Sys.file_exists dirname) then mkdir_p dirname; + let jsonfile = + String.concat "" + [ + !output_dir; + !filename; + "-domain"; + !domain; + (if !ordinals then "-ordinals" ^ string_of_int !Config.ordmax else ""); + (if !refine then "-refine" else ""); + ".json"; + ] + in + let output = + json_string !filename !analysis !property !precondition + (if !Config.result then "TRUE" else "UKNOWN") + !domain !joinbwd !exectime + in + let json : Yojson.Safe.t = + `Assoc + (("Config", Yojson.Safe.from_string output) + :: ("tree", !tree) + :: [ ("vulnerability", !vuln_res) ]) + in + let f = open_out jsonfile in + Yojson.Safe.pretty_to_channel f json; + Yojson.Safe.pretty_to_channel Stdlib.stdout json; + close_out f diff --git a/utils/dune b/utils/dune index 6c9bc85c..67fe68ea 100644 --- a/utils/dune +++ b/utils/dune @@ -1,6 +1,6 @@ (library (name utils) - (libraries frontend) + (libraries yojson str unix apron zarith frontend) (flags (:standard -open Frontend)))