From c2db27d9de0bda2d9de7c91d89a7c03496421446 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 27 Jun 2024 12:36:49 +0300 Subject: [PATCH] Remove some trailing whitespace --- .../apron/linearTwoVarEqualityDomain.apron.ml | 24 +++++++++---------- src/cdomains/apron/sharedFunctions.apron.ml | 2 +- src/common/domains/printable.ml | 10 ++++---- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 5558bc2c96..3a9e2d3e11 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -158,7 +158,7 @@ module EqualitiesConjunction = struct let (newref,offs,divi) = (get_rhs d head) in let (coeff,y) = BatOption.get newref in let (y,yrhs) = inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *) - let shifted_cluster = (List.fold (fun map i -> + let shifted_cluster = (List.fold (fun map i -> let irhs = (get_rhs d i) in (* old entry is i = irhs *) Rhs.subst yrhs y irhs |> (* new entry for i is irhs [yrhs/y] *) set_rhs map i @@ -222,7 +222,7 @@ module EqualitiesConjunction = struct | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)-> (match get_rhs ts j with (* ts[x_j]=o2/d2 ========> ... *) - | (None , o2, divi2) -> + | (None , o2, divi2) -> let newxi = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in let newxh1 = snd @@ inverse i (coeff1,h1,o1,divi1) in let newxh1 = Rhs.subst newxi i newxh1 in @@ -251,7 +251,7 @@ module EqualitiesConjunction = struct else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *) (* so now, we transform with the inverse of the transformer: *) let inv = snd (inverse i (coeff,j,offs,divi)) in - IntMap.fold (fun k v acc -> + IntMap.fold (fun k v acc -> match v with | (Some (c,x),o,d) when x=i-> set_rhs acc k (Rhs.subst inv i v) | _ -> acc @@ -281,7 +281,7 @@ struct let multiply a b = (* if one of them is a constant, then multiply. Otherwise, the expression is not linear *) match a, b with - | [(None,coeff, divi)], c + | [(None,coeff, divi)], c | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c | _ -> raise NotLinearExpr in @@ -314,7 +314,7 @@ struct | x -> Some(x) (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *) - let simplified_monomials_from_texp (t: t) texp = + let simplified_monomials_from_texp (t: t) texp = BatOption.bind (monomials_from_texp t texp) (fun monomiallist -> let d = Option.get t.d in @@ -323,7 +323,7 @@ struct | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi) | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConj.get_rhs d idx) idx (v,offs,divi) in (* normalize! *) let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in - let gcdee = Z.gcd adiv divi in + let gcdee = Z.gcd adiv divi in (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)) in let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *) @@ -339,7 +339,7 @@ struct BatOption.bind (simplified_monomials_from_texp t texp ) (fun (sum_of_terms, (constant,divisor)) -> (match sum_of_terms with - | [] -> Some (None, constant,divisor) + | [] -> Some (None, constant,divisor) | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi)) |_ -> None)) @@ -447,7 +447,7 @@ struct let t1 = change_d t1 sup_env ~add:true ~del:false in let t2 = change_d t2 sup_env ~add:true ~del:false in match t1.d, t2.d with - | Some d1', Some d2' -> + | Some d1', Some d2' -> EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*) | _ -> {d = None; env = sup_env} @@ -489,7 +489,7 @@ struct - lhs itself - criteria A and B that characterize equivalence class, depending on the reference variable and the affine expression parameters wrt. each EConj - rhs1 - - rhs2 + - rhs2 however, we have to account for the sparseity of EConj maps by manually patching holes with default values *) let joinfunction lhs rhs1 rhs2 = ( @@ -516,15 +516,15 @@ struct let varentry ci offi ch offh xh = let (coeff,off,d) = Q.(ci,(offi*ch)-(ci*offh),ch) in (* compute new rhs in Q *) let (coeff,off,d) = Z.(coeff.num*d.den*off.den,off.num*d.den*coeff.den,d. num*coeff.den*off.den) in (* convert that back into Z *) - Rhs.canonicalize (Some(coeff,xh),off,d) + Rhs.canonicalize (Some(coeff,xh),off,d) in (* ci1 = a*ch1+b /\ ci2 = a*ch2+b *) (* ===> a = (ci1-ci2)/(ch1-ch2) b = ci2-a*ch2 *) - let constentry ci1 ci2 ch1 ch2 xh = + let constentry ci1 ci2 ch1 ch2 xh = let a = Q.((ci1-ci2) / (ch1-ch2)) in let b = Q.(ci2 - a*ch2) in Rhs.canonicalize (Some (Z.(a.num*b.den),xh),Z.(b.num*a.den) ,Z.(a.den*b.den) ) in - let iterate map l = + let iterate map l = match l with | (_, _, _, rhs , rhs' ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_) )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 8c94c996b0..8167667293 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -136,7 +136,7 @@ struct let expr = (** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they - might be able to be represented by means of 2 var equalities + might be able to be represented by means of 2 var equalities This simplification happens during a time, when there are temporary variables a#in and a#out part of the expression, but are not represented in the ctx, thus queries may result in top for these variables. Wrapping this in speculative diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 1a642c932a..199113a5d8 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -588,7 +588,7 @@ module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ()) end -module PQueue (Base: S) = +module PQueue (Base: S) = struct type t = Base.t BatDeque.dq include Std @@ -604,22 +604,22 @@ struct let rec loop n q = match BatDeque.front q with | None -> () - | Some (x, xs) -> (BatPrintf.fprintf f "%d\n%a\n" n Base.printXml x; + | Some (x, xs) -> (BatPrintf.fprintf f "%d\n%a\n" n Base.printXml x; loop (n+1) (xs)) in BatPrintf.fprintf f "\n\n"; - loop 0 xs; + loop 0 xs; BatPrintf.fprintf f "\n\n" let to_yojson q = `List (BatDeque.to_list @@ BatDeque.map (Base.to_yojson) q) let hash q = BatDeque.fold_left (fun acc x -> (acc + 71) * (Base.hash x)) 11 q let equal q1 q2 = BatDeque.eq ~eq:Base.equal q1 q2 - let compare q1 q2 = + let compare q1 q2 = match BatDeque.front q1, BatDeque.front q2 with | None, None -> 0 | None, Some(_, _) -> -1 | Some(_, _), None -> 1 - | Some(a1, q1'), Some(a2, q2') -> + | Some(a1, q1'), Some(a2, q2') -> let c = Base.compare a1 a2 in if c <> 0 then c else compare q1' q2'