diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 143 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 11 | ||||
| -rw-r--r-- | main.ml | 35 | ||||
| -rwxr-xr-x | tests/source/tst_heater.scade | 53 |
5 files changed, 223 insertions, 21 deletions
@@ -34,7 +34,7 @@ all: $(BIN) $(BIN): $(SRC) ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp -I +str' \ - -lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa' \ + -lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa octMPQ.cmxa' \ main.native \ -classic-display mv main.native $(BIN) diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index a929c0b..58cd544 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -11,7 +11,9 @@ open Apron Mostly direct translation between the two. *) -module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct +(* Polyhedra *) + +module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* manager *) type man = Polka.loose Polka.t @@ -127,9 +129,142 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct (* Pretty-printing *) let print fmt x = - Abstract1.minimize manager x; - Abstract1.print fmt x; - Format.fprintf fmt "@?" + if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x; + Format.fprintf fmt "%a@?" Abstract1.print x + + let print_vars fmt x idl = + let prevars = vars x in + let rm_vars_l = List.filter (fun (id, _) -> not (List.mem id idl)) prevars in + let rm_vars = Array.of_list + (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in + let xx = Abstract1.forget_array manager x rm_vars false in + print fmt xx + + let print_itv = Interval.print + +end + + +(* Octagons *) + +module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct + + (* manager *) + type man = Oct.t + let manager = Oct.manager_alloc() + + type itv = Interval.t + + (* abstract elements *) + type t = man Abstract1.t + + (* direct translation of numerical expressions into Apron tree expressions *) + let rec texpr_of_nexpr = function + | NIdent id -> Texpr1.Var (Var.of_string id) + | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i)) + | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r)) + | NUnary(AST_UPLUS, e, is_real) -> + Texpr1.Unop( + Texpr1.Cast, + texpr_of_nexpr e, + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NUnary(AST_UMINUS, e, is_real) -> + (* APRON bug ? Unary negate seems to not work correctly... *) + Texpr1.Binop( + Texpr1.Sub, + Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")), + (texpr_of_nexpr e), + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NBinary(op, e1, e2, is_real) -> + let f = match op with + | AST_PLUS -> Texpr1.Add + | AST_MINUS -> Texpr1.Sub + | AST_MUL -> Texpr1.Mul + | AST_DIV -> Texpr1.Div + | AST_MOD -> Texpr1.Mod + in + Texpr1.Binop( + f, + (texpr_of_nexpr e1), + (texpr_of_nexpr e2), + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + + (* direct translation of constraints into Apron constraints *) + let tcons_of_cons env (eq, op) = + let op = match op with + | CONS_EQ -> Tcons1.EQ + | CONS_NE -> Tcons1.DISEQ + | CONS_GT -> Tcons1.SUP + | CONS_GE -> Tcons1.SUPEQ + in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op + + (* implementation *) + let v_env vars = + let intv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> not n) vars) in + let realv = List.map + (fun (s, _) -> Var.of_string s) + (List.filter (fun (_, n) -> n) vars) in + (Environment.make (Array.of_list intv) (Array.of_list realv)) + + let top vars = + Abstract1.top manager (v_env vars) + let bottom vars = Abstract1.bottom manager (v_env vars) + let is_bot = Abstract1.is_bottom manager + let is_top = Abstract1.is_top manager + + let forgetvar x id = + let v = [| Var.of_string id |] in + Abstract1.forget_array manager x v false + + let vars x = + let (ivt, fvt) = Environment.vars (Abstract1.env x) in + let ivl = List.map Var.to_string (Array.to_list ivt) in + let fvl = List.map Var.to_string (Array.to_list fvt) in + (List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl) + + let vbottom x = + Abstract1.bottom manager (Abstract1.env x) + + let project x id = + Abstract1.bound_variable manager x (Var.of_string id) + + (* Apply some formula to the environment *) + let apply_cl x cons = + let env = Abstract1.env x in + let tca = Array.of_list (List.map (tcons_of_cons env) cons) in + let ar = Tcons1.array_make env (Array.length tca) in + Array.iteri (Tcons1.array_set ar) tca; + Abstract1.meet_tcons_array manager x ar + + let apply_cons x cons = apply_cl x [cons] + + + let assign x eqs = + let env = Abstract1.env x in + let vars = Array.of_list + (List.map (fun (id, _) -> Var.of_string id) eqs) in + let vals = Array.of_list + (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in + Abstract1.assign_texpr_array manager x vars vals None + + + (* Ensemblistic operations *) + let join = Abstract1.join manager + let meet = Abstract1.meet manager + let widen = Abstract1.widening manager + + let subset = Abstract1.is_leq manager + let eq = Abstract1.is_eq manager + + (* Pretty-printing *) + let print fmt x = + if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x; + Format.fprintf fmt "%a@?" Abstract1.print x let print_vars fmt x idl = let prevars = vars x in diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index ed029da..dbc17c9 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -33,9 +33,14 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | NIdent id -> get_var env id | NIntConst i -> V.const i | NRealConst f -> V.const (int_of_float f) (* TODO floats *) - | NUnary (AST_UPLUS, e, _) -> eval env e - | NUnary (AST_UMINUS, e, _) -> V.neg (eval env e) - | NBinary (op, e1, e2, _) -> + | NUnary (AST_UPLUS, e, isreal) -> + if isreal then not_implemented "real type for nonrelationnal domain"; + eval env e + | NUnary (AST_UMINUS, e, isreal) -> + if isreal then not_implemented "real type for nonrelationnal domain"; + V.neg (eval env e) + | NBinary (op, e1, e2, isreal) -> + if isreal then not_implemented "real type for nonrelationnal domain"; let f = match op with | AST_PLUS -> V.add | AST_MINUS -> V.sub @@ -16,19 +16,21 @@ module Interpret = Interpret.I module ItvND = Nonrelational.ND(Intervals_domain.VD) module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND) -module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND) +module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Poly) +module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Oct) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) -module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND) +module AI_Poly_EDD = Abs_interp_edd.I(Apron_domain.ND_Poly) +module AI_Oct_EDD = Abs_interp_edd.I(Apron_domain.ND_Oct) module AI_S_Itv_DP = Abs_interp_dynpart.I (Enum_domain.MultiValuation)(ItvND) module AI_S_Rel_DP = Abs_interp_dynpart.I - (Enum_domain.MultiValuation)(Apron_domain.ND) + (Enum_domain.MultiValuation)(Apron_domain.ND_Poly) module AI_EDD_Itv_DP = Abs_interp_dynpart.I (Enum_domain_edd.EDD)(ItvND) module AI_EDD_Rel_DP = Abs_interp_dynpart.I - (Enum_domain_edd.EDD)(Apron_domain.ND) + (Enum_domain_edd.EDD)(Apron_domain.ND_Poly) (* command line options *) let times = ref false @@ -37,9 +39,11 @@ let dumprn = ref false let test = ref false let vtest = ref false let ai_itv = ref false -let ai_rel = ref false +let ai_poly = ref false +let ai_oct = ref false let ai_itv_edd = ref false -let ai_rel_edd = ref false +let ai_poly_edd = ref false +let ai_oct_edd = ref false let ai_s_itv_dp = ref false let ai_s_rel_dp = ref false let ai_edd_itv_dp = ref false @@ -68,12 +72,15 @@ let options = [ "--test", Arg.Set test, "Simple testing (direct interpret)."; "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals."; - "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron."; + "--ai-poly", Arg.Set ai_poly, "Do abstract analysis using Apron polyhedra domain."; + "--ai-oct", Arg.Set ai_oct, "Do abstract analysis using Apron octagon domain."; "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain."; - "--ai-rel-edd", Arg.Set ai_rel_edd, - "Do abstract analysis using Apron and EDD disjunction domain."; + "--ai-poly-edd", Arg.Set ai_poly_edd, + "Do abstract analysis using Apron polyhedra domain and EDD disjunction domain."; + "--ai-oct-edd", Arg.Set ai_oct_edd, + "Do abstract analysis using Apron octagon domain and EDD disjunction domain."; "--ai-s-itv-dp", Arg.Set ai_s_itv_dp, "Do abstract analysis using dynamic partitionning method, "^ @@ -172,8 +179,8 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv || !ai_rel - || !ai_itv_edd || !ai_rel_edd + if !ai_itv || !ai_poly || !ai_oct + || !ai_itv_edd || !ai_poly_edd || !ai_oct_edd || !ai_s_itv_dp || !ai_s_rel_dp || !ai_edd_itv_dp || !ai_edd_rel_dp then begin @@ -206,10 +213,12 @@ let () = } in if !ai_itv then AI_Itv.do_prog opt rp; - if !ai_rel then AI_Rel.do_prog opt rp; + if !ai_poly then AI_Poly.do_prog opt rp; + if !ai_oct then AI_Oct.do_prog opt rp; if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp; - if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp; + if !ai_poly_edd then AI_Poly_EDD.do_prog opt rp; + if !ai_oct_edd then AI_Oct_EDD.do_prog opt rp; if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp; if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp; diff --git a/tests/source/tst_heater.scade b/tests/source/tst_heater.scade new file mode 100755 index 0000000..c9212e9 --- /dev/null +++ b/tests/source/tst_heater.scade @@ -0,0 +1,53 @@ +const dt : real = 0.001; + +node heater(xi,yi : real) returns (xo, yo: real) +let + automaton + initial state Off + --unless + -- if xi <= 21.0 and yi <= 55.0 restart On; + let + xo = -xi * dt + xi; + yo = -3.0 * yi * dt + yi; + tel + until + if xi <= 21.0 and yi <= 55.0 restart On; + + state On + --unless + -- if xi >= 24.0 or yi >= 75.0 restart Off; + let + xo = (100.0 - xi) * dt + xi; + yo = 2.0 * (150.0 - yi) * dt + yi; + tel + until + if xi >= 24.0 or yi >= 75.0 restart Off; + returns xo, yo; +tel + +node top (ix, iy : real) returns (x,y : real ; safe, stabilized : bool) +var + mem: bool; + reached: bool; + safe_init : bool; + temp: bool; +let + assume init_cond: ix = iy; + + x,y = heater (ix -> pre x, iy -> pre y); + safe_init = (ix=iy and iy < 80.0) -> pre safe_init; + safe = not safe_init or y < 80.0; + + reached = x >= 21.0 and x <= 24.0 and y >= 55.0 and y <= 75.0; + temp = x>=20.0 and x<=25.0; + + mem = + (ix > 21.0 and ix < 24.0 and iy >= 55.0 and iy <= 75.0) + -> reached or pre mem; + + stabilized = not mem or temp; + + guarantee g1: safe; + guarantee g2: stabilized; + +tel |