From 2d21341c73f7deebbd99931489e9906c94dac7eb Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 28 Apr 2023 08:18:04 +0200 Subject: [PATCH] Add fix point with widening --- abstract_interpreter.ml | 10 +++++----- domain_non_rel.ml | 8 ++++++-- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml index 8ade5be..38d68ba 100644 --- a/abstract_interpreter.ml +++ b/abstract_interpreter.ml @@ -46,13 +46,13 @@ module Interprete(D : DOMAIN) = let f = eval_stmt (filter a e false) s2 in D.join t f | Swhile (_, e, b) -> - let rec fix (f:t -> t) (x:t) : t = - let fx = f x in + let rec fix (f:(t -> t -> t) -> t -> t) (op:t -> t -> t) (x:t) (i:int) : t = + let fx = f op x in if D.subset fx x then fx - else fix f fx + else fix f (if i < 3 then D.join else D.widen) fx (i+1) (* widening after 3 iterations *) in - let f x = D.join a (eval_stmt (filter x e true) (Sblock b)) in - let inv = fix f a in + let f op x = op a (eval_stmt (filter x e true) (Sblock b)) in + let inv = fix f D.join a 0 in filter inv e false | Sfor (l,s1,e,s2,b) -> let a1 = eval_stmt a s1 in diff --git a/domain_non_rel.ml b/domain_non_rel.ml index 869301d..8f5f502 100644 --- a/domain_non_rel.ml +++ b/domain_non_rel.ml @@ -98,9 +98,13 @@ module NonRelational(D : VALUE_DOMAIN) = (struct match m1, m2 with | BOTTOM, x | x, BOTTOM -> x | Val m, Val n -> - Val (Env.union (fun k a b -> Some (D.join a b)) m n) + Val (Env.union (fun _ a b -> Some (D.join a b)) m n) - let widen = join + let widen m1 m2 = + match m1, m2 with + | BOTTOM, x | x, BOTTOM -> x + | Val m, Val n -> + Val (Env.union (fun _ a b -> Some (D.widen a b)) m n) let meet m1 m2 = match m1, m2 with