úÎ!ˆ"|žš      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~  € ‚ ƒ „ … † ‡ ˆ ‰ Š ‹ Œ Ž ‘ ’ “ ” • – — ˜ ™ (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone8>HVÚdatafixChooses an appropriate  for a given key type.MonoMapGs should all be ordered maps, which feature efficient variants of the  and  combinators. This unifies  Data.Maybe, Data.IntMap.Strict, Data.Map.Strict and Data.POMap.Strictg under a common type class, for which instances can delegate to the most efficient variant available. Because of D, this class lends itself well to approximating monotone functions.(The default implementation delegates to š€, so when there is no specially crafted map data-structure for your key type, all you need to do is to make sure it satisfies ›. Then you can doimport Data.IntSetinstance MonoMapKey IntSet*to make use of the default implementation.datafixBThe particular ordered map implementation to use for the key type k.(The default implementation delegates to š.datafix^Key point of this interface! Note that it returns a list of lower bounds, to account for the › case.datafix Delegates to œ.datafix Delegates to .    (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone1>½ždatafix7Highest priority node and lowest element of the domain k first.Ÿ ¡¢£¤¥¦§ž¨©ª«¬­(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone1>8 ®¯°±²³´µ¶·(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone&',-.=>?HSUVX!¤datafix.A representation of the quantified constraint  forall a. p a.datafix Given that a :- b(, derive something that needs a context b, using the context a1(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone#¸¹º»¼½(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone&',-.=>?@AHUVXk7/ datafix Currying as b# witnesses the isomorphism between  Arrows as b and Products as -> bO. It is defined as a type class rather than by recursion on a singleton for asX so all of that these conversions are inlined at compile time for concrete arguments.$datafixUsing IsBase we can define notions of  ParamTypes and  ReturnTypes. which *reduce* under positive information IsBase t ~ 'True even though the shape of t is not formally exposed%datafixIsBase t is 'True whenever t is *not* a function space.&datafix Products [] corresponds to (),  Products [a] corresponds to a, Products [a1,..,an] corresponds to (a1, (..,( an)..)).`So, not quite a right fold, because we want to optimize for the empty, singleton and pair case.'datafixArrows [a1,..,an] r corresponds to a1 -> .. -> an -> r,datafix Version of FoldrV taking a defunctionalised argument so that we can use partially applied functions.-datafixOn Lists.datafix On Booleans/datafixAll p as ensures that the constraint p is satisfied by all the types in asZ. (Types is between scare-quotes here because the code is actually kind polymorphic) !"#$%&'()*+,-./0/.-,+*)('0&%$#"! (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNoneUV;×¾datafix entailment for ChangeDetectors.¿datafix entailment for  LiftedFuncs.Àdatafix# entailment for abortion functions.Ádatafix entailment for pure functions.¾¿ÀÁ(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone,>@AHSVXk€œ4datafix)A constraint synonym for constraints the domain has to suffice.IThis is actually a lot less scary than you might think. Assuming we got  +http://i.cs.hku.hk/~bruno/papers/hs2017.pdfquantified class constraints instead of hackery from the  _https://hackage.haskell.org/package/constraints-0.10/docs/Data-Constraint-Forall.html#t:ForallF@constraints@ package,  Datafixable" is a specialized version of this: ¨type Datafixable domain = ( forall r. Currying (ParamTypes domain) r , MonoMapKey (Products (ParamTypes domain)) , BoundedJoinSemiLattice (ReturnType domain) ) Now, let's assume a concrete domain ~ String -> Bool -> Int , so that $ (String -> Bool -> Int) expands to the type-level list '[String, Bool] and & '[String, Bool] reduces to (String, Bool)..Then this constraint makes sure we are able to Curry the domain of String -> Bool -> r for all r to e.g. (String, Bool) -> r . See a. This constraint should always be discharged automatically by the type-checker as soon as $ and  ReturnTypes reduce for the 61 argument, which happens when the concrete MonadDependency m is known.We want to use a  0https://en.wikipedia.org/wiki/Monotonic_functionmonotone map of (String, Bool) to Int (the ReturnType domain ). This is ensured by the  (String, Bool) constraint.uThis constraint has to be discharged manually, but should amount to a single line of boiler-plate in most cases, see .WNote that the monotonicity requirement means we have to pull non-monotone arguments in Domain m into the Node portion of the DataFlowFramework.nFor fixed-point iteration to work at all, the values which we iterate naturally have to be instances of ÂL. That type-class allows us to start iteration from a most-optimistic Ãj value and successively iterate towards a conservative approximation using the '(/)' operator.5datafixA monad with an associated 6G. This class exists mostly to share the associated type-class between MonadDependency and  MonadDatafix.Also it implies that m satisfies 4, which is common enough6datafixàThe abstract domain in which nodes of the data-flow graph are denoted. When this reduces to a function, then all functions of this domain are assumed to be monotone wrt. the (at least) partial order of all occuring types!NIf you can't guarantee monotonicity, try to pull non-monotone arguments into Nodes.7datafix9A function that checks points of some function with type domain for changes. If this returns Ä7, the point of the function is assumed to have changed.SAn example is worth a thousand words, especially because of the type-level hackery:5cd = (\a b -> even a /= even b) :: ChangeDetector Int}This checks the parity for changes in the abstract domain of integers. Integers of the same parity are considered unchanged.cd 4 5Truecd 7 13False&Now a (quite bogus) pointwise example:Jcd = (\x fx gx -> x + abs fx /= x + abs gx) :: ChangeDetector (Int -> Int) cd 1 (-1) 1False cd 15 1 2Truecd 13 35 (-35)FalseThis would consider functions id and negate unchanged, so the sequence iterate negate :: Int -> Int- would be regarded immediately as convergent:f x = iterate negate x !! 0let g x = iterate negate x !! 1cd 123 (f 123) (g 123)False8datafixData-flow problems denote Node9s in the data-flow graph by monotone transfer functions.This type alias alone carries no semantic meaning. However, it is instructive to see some examples of how this alias reduces to a normal form: ´ LiftedFunc Int m ~ m Int LiftedFunc (Bool -> Int) m ~ Bool -> m Int LiftedFunc (a -> b -> Int) m ~ a -> b -> m Int LiftedFunc (a -> b -> c -> Int) m ~ a -> b -> c -> m Int m" will generally be an instance of MonadDependency' and the type alias effectively wraps m around domainw's return type. The result is a function that produces its return value while potentially triggering side-effects in m!, which amounts to depending on 8 s of other Node s for the MonadDependency case.9datafixA 7 that delegates to the Å instance of the node values.:datafixA 7 that always returns Ä.ŽUse this when recomputing a node is cheaper than actually testing for the change. Beware of cycles in the resulting dependency graph, though! 456789:;< 879:564;<(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone >@AHSVXµ3=datafix'A monad with a single impure primitive ># that expresses a dependency on a C of a data-flow graph.The associated 61 type is the abstract domain in which we denote Cs.eThink of it like memoization on steroids. You can represent dynamic programs with this quite easily::{[ transferFib :: forall m . (MonadDependency m, Domain m ~ Int) => Node -> LiftedFunc Int m! transferFib (Node 0) = return 0! transferFib (Node 1) = return 1V transferFib (Node n) = (+) <$> dependOn @m (Node (n-1)) <*> dependOn @m (Node (n-2))& -- sparing the negative n error case:}$We can construct a description of a ? with this  transferFib function::{\ dataFlowFramework :: forall m . (MonadDependency m, Domain m ~ Int) => DataFlowFramework mL dataFlowFramework = DFF transferFib (const (eqChangeDetector @(Domain m))):}We regard the ordinary fib2 function a solution to the recurrence modeled by  transferFib::{ fib :: Int -> Int fib 0 = 0 fib 1 = 1! fib n = fib (n-1) + fib (n - 2):}E.g., under the assumption of fibj being total (which is true on the domain of natural numbers), it computes the same results as the least  fixed-point7 of the series of iterations of the transfer function  transferFib.!Ostensibly, the nth iteration of  transferFib substitutes each dependOn with  transferFib? repeatedly for n times and finally substitutes all remaining dependOns with a call to Æ.Computing a solution by fixed-point iteration† in a declarative manner is the purpose of this library. There potentially are different approaches to computing a solution, but in Datafix.Worklist‰ we offer an approach based on a worklist algorithm, trying to find a smart order in which nodes in the data-flow graph are reiterated.®The concrete MonadDependency depends on the solution algorithm, which is in fact the reason why there is no satisfying data type in this module: We are only concerned with  declaring data-flow problems here.’The distinguishing feature of data-flow graphs is that they are not necessarily acyclic (data-flow graphs of dynamic programs always are!), but  8https://en.wikipedia.org/wiki/Kleene_fixed-point_theoremunder certain conditions, even have solutions when there are cycles.ÛCycles occur commonly in data-flow problems of static analyses for programming languages, introduced through loops or recursive functions. Thus, this library mostly aims at making the life of compiler writers easier.>datafixŽExpresses a dependency on a node of the data-flow graph, thus introducing a way of trackable recursion. That's similar to how you would use  to abstract over recursion.?datafix'Models a data-flow problem, where each C is mapped to its denoting 8] and a means to detect when the iterated transfer function reached a fixed-point through a 7.AdatafixA transfer function per each C" of the modeled data-flow problem.BdatafixA 7 for each CT of the modeled data-flow problem. In the simplest case, this just delegates to an Å instance.Cdatafix>This is the type we use to index nodes in the data-flow graph..The connection between syntactic things (e.g. Ids) and Cgs is made implicitly in code in analysis templates through an appropriate allocation mechanism as in  NodeAllocator. =>?@ABCDE CDE?@AB=>(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNoneM¾eIdatafix&A state monad wrapping a mapping from C to some v+ which we will instantiate to appropriate  LiftedFuncs.JdatafixAllocates the next C4, which is greater than any nodes requested before.1The value stored at that node is the result of a I+ computation which may already access the Cˆ associated with that value. This is important for the case of recursive let, where the denotation of an expression depends on itself.Kdatafix4Runs the allocator, beginning with an empty mapping.IJKIJK(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone >HSVXkÑßOdatafix4A denotation of some syntactic entity in a semantic domain, built in a some P context.PdatafixBuilds on an associated Q that is a 5 (like any MonadDependency=) by providing a way to track dependencies without explicit NodeE management. Essentially, this allows to specify a build plan for a DataFlowFramework through calls to R in analogy to fix or mfix.QdatafixZThe monad in which data dependencies are expressed. Can and will be instantiated to some MonadDependency, if you choose to go through FrameworkBuilder.RdatafixCThis is the closest we can get to an actual fixed-point combinator.We need to provide a 7¿ for detecting the fixed-point as well as a function to be iterated. In addition to returning a better approximation of itself in terms of itself, it can return an arbitrary value of type a.. Because the iterated function might want to RU additional times (think of nested let bindings), the return values are wrapped in m.Finally, the arbitrary a" value is returned, in analogy to a in # :: MonadFix m => (a -> m a) -> m a.Sdatafix!Shorthand that partially applies R to an 9.OPQRSPQRSO(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone=>?@AHMSVXkÙÛTdatafixConstructs a build plan for a ? by tracking allocation of C s mapping to 7s and transfer functions.Udatafix)(root, max, dff) = buildFramework builder' executes the build plan specified by builder and returns the resulting ? dff, as well as the root C1 denoting the transfer function returned by the T action and the max7imum node of the problem as a proof for its denseness.TUTU (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone1>HVæ ZdatafixBAbstracts over the concrete representation of the data-flow graph.%There are two instances: The default  for sparse graphs based on an IntMap and " for the dense case, storing the Node mapping in a .^datafixDiff between two ®s.bdatafixMThe data associated with each point in the transfer function of a data-flow Node.ddatafix The value at this point. Can be Ç only when a loop was detected.edatafix6Points this point of the transfer function depends on.fdatafixPoints depending on this point.gdatafixBThe number of times this point has been updated through calls to updateNodeValue.hdatafix The default b.idatafixComputes the diff between two ®s.Z[]\^_a`bcgfedhibcgfedh^_a`iZ[]\ (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone>HVê©ldatafix4Reference to a dense data-flow graph representation.Èdatafix@Models the points of a transfer function of a single data-flow Node.mdatafixAllocates a new dense graph l.lmlm (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone>HVïIodatafix5Reference to a sparse data-flow graph representation.Édatafix'Models a data-flow graph as a map from Node3s to associated points of their transfer function.pdatafixAllocates a new sparse graph o.opop (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone&',>@AHMSVX_kjàrdatafixlExpresses that iteration should or shouldn't stop after a point has been iterated a finite number of times.sdatafixnWill keep on iterating until a precise, yet conservative approximation has been reached. Make sure that your domain satisfies the  7https://en.wikipedia.org/wiki/Ascending_chain_conditionascending chain condition:, e.g. that fixed-point iteration always comes to a halt!tdatafixFor when your domaine doesn't satisfy the ascending chain condition or when you are sensitive about solution performance.The ÊIeger determines the maximum number of iterations of a single point of a Cƒ (with which an entire function with many points may be associated) before iteration aborts in that point by calling the supplied u. The responsibility of the u[ is to find a sufficiently conservative approximation for the current value at that point. When your " is an instance of Ë, „¢ might be a worthwhile option. A more sophisticated solution would trim the current value to a certain cut-off depth, depending on the first parameter, instead.udatafix¶A function that computes a sufficiently conservative approximation of a point in the abstract domain for when the solution algorithm decides to have iterated the node often enough.When domain is a )'BoundedMeetSemilattice'/'BoundedLattice'@, the simplest abortion function would be to constantly return Ì.As is the case for 8 and 7x, this carries little semantic meaning if viewed in isolation, so here are a few examples for how the synonym expands: ± AbortionFunction Int ~ Int -> Int AbortionFunction (String -> Int) ~ String -> Int -> Int AbortionFunction (a -> b -> c -> PowerSet) ~ a -> b -> c -> PowerSet -> PowerSet =E.g., the current value of the point is passed in (the tuple (a, b, c, PowerSet)U) and the function returns an appropriate conservative approximation in that point.vdatafixSpecifies the density- of the problem, e.g. whether the domain of C3s can be confined to a finite range, in which case “ tries to use a  Data.Vector6 based graph representation rather than one based on  Data.IntMap.ydatafixThe iteration state of 'DependencyM'/'solveProblem'.{datafixHConstant. The specification of the data-flow problem we ought to solve.|datafix@Constant. Whether to abort after a number of iterations or not.}datafix,Contextual state. The set of points in the domain of Cs currently in the call stack.~datafix^Constant ref to stateful graph. The data-flow graph, modeling dependencies between data-flow C%s, or rather specific points in the domain of each C.datafixQConstant (but the the wrapped set is stateful). The set of points the currently Œd node references so far.€datafixOConstant (but the the wrapped queue is stateful). Unstable nodes that will be Œ d by the ’list algorithm.datafix The concrete = for this worklist-based solver.JThis essentially tracks the current approximation of the solution to the ? as mutable state while “G makes sure we will eventually halt with a conservative approximation.‚datafixWhy does this use Í? Actually, we only need STS here, but that means we have to carry around the state thread in type signatures.;This ultimately leaks badly into the exported interface in “W: Since we can't have universally quantified instance contexts (yet!), we can' write b(forall s. Datafixable domain => (forall s. DataFlowFramework (DependencyM s graph domain)) -> ...+ and have to instead have the isomorphic q(forall s r. (Datafixable domain => r) -> r) -> (forall s. DataFlowFramework (DependencyM s graph domain)) -> ...0 and urge all call sites to pass a meaningless Î parameter.bAlso, this means more explicit type signatures as we have to make clear to the type-checker that s@ is universally quantified in everything that touches it, e.g. &Analyses.StrAnal.LetDn.buildDenotation from the test suite.So, bottom line: We resort to Í and ÏE and promise not to launch missiles. In particular, we don't export ‚. and also there must never be an instance of MonadIO for this.„datafixAborts iteration of a value by Ðantly returning the Ì element of the assumed Ë of the ".Œdatafix4The first of the two major functions of this module.recompute node args" iterates the value of the passed node at the point argsK by invoking its transfer function. It does so in a way that respects the r.5This function is not exported, and is only called by ’ and 4, for when the iteration strategy decides that the nodeF needs to be (and can be) re-iterated. It performs tracking of which CVs the transfer function depended on, do that the worklist algorithm can do its magic.ŽdatafixšCompute an optimistic approximation for a point of a given node that is as precise as possible, given the other points of that node we already computed.#E.g., it is always valid to return Ö from this, but in many cases we can be more precise since we possibly have computed points for the node that are lower bounds to the current point.datafixscheme 1 (see  Œhttps://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like).-Let the worklist algorithm figure things out.datafixscheme 2 (see  Œhttps://github.com/sgraf812/journal/blob/09f0521dbdf53e7e5777501fc868bb507f5ceb1a/datafix.md.html#how-an-algorithm-that-can-do-3-looks-like). Descend into \bot nodes when there is no cycle to discover the set of reachable nodes as quick as possible. Do *not* descend into unstable, non-(bot) nodes.‘datafixAs long as the supplied Maybeb expression returns "Just _", the loop body will be called and passed the value contained in the Ñ. Results are discarded. Taken from .’datafixODefined as 'work = whileJust_ highestPriorityUnstableNode (uncurry recompute)'.Tries to dequeue the Š and Œs the value of one of its €V points, until the worklist is empty, indicating that a fixed-point has been reached.“datafix$Computes the (pure) solution of the  action act# specified in the last parameter. act may reference (via ) C s of the ? dff1's fixed-point, specified as the first parameter.dff='s fixed-point is determined by its transfer functions, and  solveProblem$ will make sure that all (relevant) Cos will have reached their fixed-point according to their transfer function before computing the solution for act.êWe try to be smart in saving unnecessary iterations of transfer functions by employing a worklist algorithm. For function domains, where each Node denotes a monotone function, each point's dependencies' will be tracked individually. Apart from dff and act, the v! of the data-flow graph and the r can be specified. Pass w and s when in doubt.1If your problem only has finitely many different Cs , consider using the FrameworkBuilder API (e.g. datafix + evalDenotation6) for a higher-level API that let's you forget about CMs and instead let's you focus on building more complex data-flow frameworks.See Datafix.Tutorial and the  examples/ subfolder for examples.”datafixThis allows us to solve (MonadDependency m => DataFlowFramework m descriptions with “.•datafixThe 6$ is extracted from a type parameter.“datafixThe description of the DataFlowFramework.datafix,Describes if the algorithm is free to use a x, Vector1-based graph representation or has to go with a w one based on IntMap.datafixkWhether the solution algorithm should respect a maximum bound on the number of iterations per point. Pass s if you don't care.datafixEThe action for which we want to compute the solution. May reference C s from the DataFlowFramework). If you just want to know the value of C5 42, use `dependOn @(DependecyM _ domain) (Node 42)`."rtsuvwxyz€|{~}‚ƒ„…†‡ˆ‰Š‹ŒŽ‘’“"‚yz€|{~}ƒvwxu„rts…†‡ˆ‰Š‹ŒŽ‘’“ (c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone >@AHSVXkwP™datafixevalDenotation denot ib returns a value in domain& that is described by the denotation denot.It does so by building up the DataFlowFramework corresponding to denot) and solving the resulting problem with “e, the documentation of which describes in detail how to arrive at a stable denotation and what the r ib", domain ~ Domain (DepM m) is for.™datafixoA build plan for computing the denotation, possibly involving fixed-point iteration factored through calls to R.datafixkWhether the solution algorithm should respect a maximum bound on the number of iterations per point. Pass s if you don't care.™™(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNonexz rstvxw“™ vxwrst“™(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone >@AHVXz,< !"#$%&'()*,-./0456789:;<=>?@ABCDEIJKOPQRSTUrstvxw“™ !"#$%&'()*,-./0(c) Sebastian Graf 2017-2020ISCsgraf1337@gmail.comportableNone|šÒ !"#$%&'()*+,-./01234556789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abbcdefghijklmnopqrstuvw x y & ' z z { | } } ~  € ‚ ƒ „ …  † ‡  † ‡ ˆ ‰ Š ‹ Œ  Ž   ‘ ’ “ ” • – — ˜ ™ š › œ ž Ÿ   ¡ ] ¢ £ ¤  ¥ ¦ § ¨ © ª « ¬­®¯°±²³´µ¶·¸¹ºJ»"#$%&)*,+-/'¼½"#$%¾)¿¹ÀÁÂÃÄÅÆÇÈÉ°ÊË°ÊÌÍÎÏÍÐѶÒÓ¶·Ô Õ ÖÍÎ×°ÊØ°ÊÙÍÎÚ¶ÛܶÝÞ¶Û߶·àá&datafix-0.0.1.0-JRa2sB3v9WL1cW4BQiQEg6Datafix.MonoMapDatafix.Utils.ConstraintsDatafix.Utils.TypeLevelDatafix.CommonDatafix.ExplicitDatafix.NodeAllocatorDatafix.DenotationalDatafix.FrameworkBuilderDatafix.Worklist.GraphDatafix.Worklist.Graph.DenseDatafix.Worklist.Graph.SparseDatafix.Worklist.InternalDatafix.Worklist.DenotationalDatafix.IntArgsMonoMapDatafix.IntArgsMonoSetDatafix.Utils.GrowableVectorDatafix.Entailments Data.FunctionfixControl.Monad.FixmfixDatafix.Graph.SparseRefDatafix.Graph.DenseDataIOVectorControl.Monad.Loops whileJust_Datafix.WorklistDatafixDatafix.Tutorial MonoMapKeyMonoMapempty singletoninsertdeletelookuplookupLT lookupMin differencekeys insertWithinsertLookupWithKeyupdateLookupWithKeyalteradjust$fMonoMapKeyInt$fMonoMapKey()Forall:-SubDict\\inst $fForall_kpApply Constant1 Constant0FunctionCurryinguncurryscurrys ReturnType' ReturnType ParamTypes' ParamTypesIsBaseProductsArrowsConstantConsMap1ConsMap0MapFoldr'FoldrIfAll arrowsAxiom $fCurrying:b $fCurrying:b0 $fCurrying[]b Datafixable MonadDomainDomainChangeDetector LiftedFunceqChangeDetectoralwaysChangeDetectorevalAt