diff --git a/domains/reduced_product.ml b/domains/reduced_product.ml new file mode 100644 index 0000000..842de5d --- /dev/null +++ b/domains/reduced_product.ml @@ -0,0 +1,47 @@ +open Value_domain + +module type CROSS_REDUCTION = sig + module V : VALUE_DOMAIN + module W : VALUE_DOMAIN + val cr : V.t * W.t -> V.t*W.t +end + +module ReducedProduct (C : CROSS_REDUCTION) : VALUE_DOMAIN = struct + type t = C.V.t * C.W.t + let top = C.V.top, C.W.top + let bottom = C.V.bottom, C.W.bottom (* other representations possible; this one is cr - stable.*) + + let const z = C.V.const z, C.W.const z + let rand a b = C.V.rand a b, C.W.rand a b + let unary p uop = let p = C.cr p in C.cr ((C.V.unary (fst p) uop),(C.W.unary (snd p) uop)) + let binary p p' binop = let p, p' = C.cr p, C.cr p' in C.cr ( + (C.V.binary (fst p) (fst p') binop), + (C.W.binary (snd p) (snd p') binop)) + let compare p p' cop = let p, p' = C.cr p, C.cr p' in + let vp, vp' = (C.V.compare (fst p) (fst p') cop) in + let wp, wp' = (C.W.compare (snd p) (snd p') cop) in + C.cr (vp, wp), C.cr (vp', wp') + let bwd_unary p uop r = let p = C.cr p in C.cr ( + (C.V.bwd_unary (fst p) uop (fst r)), + (C.W.bwd_unary (snd p) uop (snd r))) + let bwd_binary p p' bop r = let p,p' = C.cr p, C.cr p' in + let vp, vp' = C.V.bwd_binary (fst p) (fst p') bop (fst r) in + let wp, wp' = C.W.bwd_binary (snd p) (snd p') bop (snd r) in + C.cr (vp, wp), C.cr (vp', wp') + let join p p' = let p,p' = C.cr p,C.cr p' in C.cr ( + (C.V.join (fst p) (fst p')), + (C.W.join (snd p) (snd p'))) + let meet p p' = let p,p' = C.cr p,C.cr p' in C.cr ( + (C.V.meet (fst p) (fst p')), + (C.W.meet (snd p) (snd p'))) + + (* we do NOTC.cross-reduce p : it would not guarantee convergence anymore *) + let widen p p' = let p' = C.cr p' in C.V.widen (fst p) (fst p'), C.W.widen (snd p) (snd p') + let narrow p p' = let p' = C.cr p' in C.V.narrow (fst p) (fst p'), C.W.narrow (snd p) (snd p') + + let subset p p' = let p, p' = C.cr p, C.cr p' in + C.V.subset (fst p) (fst p') && C.W.subset (snd p) (snd p') + let is_bottom p = (C.cr p) = bottom + let print fmt p = + Format.fprintf fmt "@[(%a, %a)@]@ " C.V.print (fst p) C.W.print (snd p) +end