Documentation

Lean.Compiler.LCNF.ElimDeadBranches

The abstract domain of the interpreter. Representing sets of values of a certain type.

  • bot : Value

    Undefined, could be anything we have no information.

  • top : Value

    All values are possible.

  • ctor (i : Name) (vs : Array Value) : Value

    A certain constructor with a certain sets of parameters is possible.

  • choice (vs : List Value) : Value

    A set of values are possible.

Instances For

    Fuse v into vs. That is do not only append but if we see that v is a constructor that is already contained within vs try to detect the difference between these values and merge them accordingly into a choice node further down the tree.

    Merge two values into one. bot is the neutral element, top the annihilator.

    Make sure constructors of recursive inductive datatypes can only occur once in each path. Values at depth > maxValueDepth are also approximated at top. We use this function to implement a simple widening operation for our abstract interpreter. Recall the widening functions is used to ensure termination in abstract interpreters.

    Equations
      Instances For
        partial def Lean.Compiler.LCNF.UnreachableBranches.Value.truncate.go (env : Environment) (v : Value) (forbiddenTypes : NameSet) (remainingDepth : Nat) :

        Widening operator that guarantees termination in our abstract interpreter.

        Equations
          Instances For

            Check whether a certain constructor is part of a Value by name. Note that both top and bot will always true here. For bot this is because we have no information about the Value so just to be sure we don't claim the absence of a certain constructor.

            Obtain the arguments of a certain constructor within the Value.

            Equations
              Instances For

                We say that a Value is a literal iff it is only a tree of Value.ctor nodes.

                Attempt to turn a Value that is representing a literal into a set of auxiliary declarations + the final FVarId of the declaration that contains the actual literal. If it is not a literal return none.

                Equations
                  Instances For
                    @[reducible, inline]

                    A map from function names to the Value that the abstract interpreter produced for them.

                    Equations
                      Instances For

                        Add a Value for a function name.

                        Equations
                          Instances For

                            Obtain the Value for a function name if possible.

                            Equations
                              Instances For
                                @[reducible, inline]

                                A map from variable identifiers to the Value produced by the abstract interpreter for them.

                                Equations
                                  Instances For

                                    The context of InterpM.

                                    • decls : Array Decl

                                      The list of Decls we are operating on in InterpM. This can be a single declaration or a mutual block of declarations where their analysis might influence each other as we approach the fixpoint.

                                    • currFnIdx : Nat

                                      The index of the function we are currently operating on in decls.

                                    Instances For
                                      Instances For
                                        @[reducible, inline]

                                        The monad which powers the abstract interpreter.

                                        Equations
                                          Instances For

                                            Get the variable Assignment of the current function.

                                            Equations
                                              Instances For

                                                Get the Value of a certain function in the current block by index.

                                                Equations
                                                  Instances For

                                                    Run f on the variable Assignment of the current function.

                                                    Equations
                                                      Instances For

                                                        Obtain the Value associated with var from the context of InterpM. If none is available return Value.bot.

                                                        Equations
                                                          Instances For

                                                            Find the value of arg using the logic of findVarValue.

                                                            Equations
                                                              Instances For

                                                                Update the assignment of var by merging the current value with newVal.

                                                                Equations
                                                                  Instances For

                                                                    Set the value of var to bot.

                                                                    Equations
                                                                      Instances For

                                                                        Widen the value of the current function by v.

                                                                        Equations
                                                                          Instances For

                                                                            Return true if the assignment of at least one parameter has been updated. Furthermore if we see that params.size != args.size we know that this is a partial application and set the values of the remaining parameters to top since it is impossible to track what will happen with them from here on.

                                                                            Equations
                                                                              Instances For

                                                                                The actual abstract interpreter on a block of Code.

                                                                                The abstract interpreter on a LetValue.

                                                                                If we see a function being passed as an argument to a higher order function we cannot know what arguments it will be passed further down the line. Hence we set all of its arguments to top since anything is possible.

                                                                                Rerun the abstract interpreter on all declarations except of the unsafe ones. Return whether any Value got updated in the process.

                                                                                Equations
                                                                                  Instances For

                                                                                    Use the information produced by the abstract interpreter to:

                                                                                    • Eliminate branches that we know cannot be hit
                                                                                    • Eliminate values that we know have to be constants.
                                                                                    Equations
                                                                                      Instances For