Documentation

LeanGccJit.Core.Types

Context is the Lean4 representation of gcc_jit_context.

See also Compilation Contexts.

Note #

The top-level of the API is the Context type.

A Context instance encapsulates the state of a compilation.

You can set up options on it, and add types, functions and code. Invoking Context.compile on it gives you a Result.

Lifetime-management #

Contexts are the unit of lifetime-management within the API: objects have their lifetime bounded by the context they are created within, and cleanup of such objects is done for you when the context is released.

Thread-safety #

Instances of Context created via Context.acquire are independent from each other: only one thread may use a given context at once, but multiple threads could each have their own contexts without needing locks.

Contexts created via Context.newChildContext are related to their parent context. They can be partitioned by their ultimate ancestor into independent “family trees”. Only one thread within a process may use a given “family tree” of such contexts at once, and if you’re using multiple threads you should provide your own locking around entire such context partitions.

Error Handling #

Various kinds of errors are possible when using the API, such as mismatched types in an assignment. You can only compile and get code from a context if no errors occur.

Errors are printed on stderr and can be queried using Context.getFirstError.

They typically contain the name of the API entrypoint where the error occurred, and pertinent information on the problem:

./buggy-program: error: gcc_jit_block_add_assignment: mismatching types: assignment to i (type: int) from "hello world" (type: const char *)

In general, if an error occurs when using an API entrypoint, the low-level entrypoint returns NULL. Unlike the original C-API, the lean wrapper is designed to be fast-fail, i.e. it will return an IO error once a step returns NULL.

Instances For

    Result is the Lean4 representation of gcc_jit_result.

    See also gcc_jit_result.

    Note #

    A Result encapsulates the result of compiling a context in-memory, and the lifetimes of any machine code functions or globals that are within the result.

    Instances For

      Object is the Lean4 representation of gcc_jit_object.

      See also Objects.

      Note #

      Almost every entity in the API (with the exception of Context and Result) is a contextual object, thus, inherited from Object.

      A JIT Object:

      • is associated with a Context.
      • is automatically cleaned up for you when its context is released so you don’t need to manually track and cleanup all objects, just the contexts.

      The Object hierarchy is as follows:

      One can upcast a derived object to its base object via APIs such as asObject. For convenience, we provide an AsObject typeclass through which one can use common APIs for objects, e.g. .getDebugString and getContext.

      Instances For

        Location is the Lean4 representation of gcc_jit_location. See also Source Localtions.

        Note #

        A Location encapsulates a source code location, so that you can (optionally) associate locations in your language with statements in the JIT-compiled code, allowing the debugger to single-step through your language.

        Location instances are optional: it is always passed as Option Location to the APIs that use it.

        You can construct them using Context.newLocation.

        You need to enable BoolOption.DebugInfo on the Context for these locations to actually be usable by the debugger.

        Instances For

          JitType is the Lean4 representation of gcc_jit_type. See also Types.

          Instances For

            Func is the Lean4 representation of gcc_jit_function.

            Function is a special namespace in Lean4, so we use Func instead. See also Functions.

            Note #

            A Func represents a function - either one that we’re creating ourselves, or one that we’re referencing.

            Instances For

              FunctionType is the Lean4 representation of gcc_jit_function_type.

              Note #

              FunctionType can be obtained by calling JitType.dyncastFunction on function pointer types. It is typically used in reflection APIs, e.g. FunctionType.getReturnType, FunctionType.getParamCount and FunctionType.getParamType.

              Instances For

                VectorType is the Lean4 representation of gcc_jit_vector_type.

                It represents a simd vector type, e.g. int __attribute__((vector_size(16))).

                Note #

                In GCCJIT, JitType.getVector is the typical way to obtain a vectorized data type. However, that API actually returns a new JitType. Instead, GCCJIT uses VectorType in those reflection APIs, namely VectorType.getNumUnits and VectorType.getElementType. For those two APIs, one can call JitType.dyncastVector to obtain a VectorType instance first.

                Instances For

                  Struct is the Lean4 representation of gcc_jit_struct. See also gcc_jit_struct.

                  Note #

                  A Struct represents a compound type analagous to a C struct.

                  A Struct can be created in mainly two ways:

                  • Context.newStruct creates a new Struct with given fields.
                  • Context.newOpaqueStruct creates a new opaque Struct with given name. The fields of the Struct can be added later using Struct.setFields.

                  Notice that once fields are set, the struct cannot be changed anymore.

                  Instances For

                    Field is the Lean4 representation of gcc_jit_field. See also gcc_jit_field.

                    Note #

                    A Field is used to refer a member of a Struct type.

                    Instances For

                      Block is the Lean4 representation of gcc_jit_block. See also Blocks.

                      Note #

                      A Block represents a basic block within a function i.e. a sequence of statements with a single entry point and a single exit point.

                      The first basic block that you create within a function will be the entrypoint.

                      Each basic block that you create within a function MUST be terminated, either with a conditional, a jump, a return, a switch, or an asm goto.

                      It’s legal to have multiple basic blocks that return within one function.

                      Instances For

                        RValue is the Lean4 representation of gcc_jit_rvalue.

                        See also RValues.

                        Note #

                        A RValue is an expression that can be computed. It can be simple, e.g.:

                        • an integer value e.g. 0 or 42
                        • a string literal e.g. “Hello world”
                        • a variable e.g. i. These are also lvalues (see below).

                        or compound e.g.:

                        • a unary expression e.g. !cond
                        • a binary expression e.g. (a + b)
                        • a function call e.g. get_distance (&player_ship, &target) etc.

                        Every RValue has an associated type, and the API will check to ensure that types match up correctly (otherwise the Context will emit an error).

                        Instances For

                          LValue is the Lean4 representation of gcc_jit_lvalue. See also LValues.

                          Note #

                          An LValue is something that can of the left-hand side of an assignment: a storage area (such as a variable). It is also usable as an RValue (converted with LValue.asRValue), where the rvalue is computed by reading from the storage area.

                          Instances For

                            Param is the Lean4 representation of gcc_jit_param. See also Params.

                            Note #

                            One should NOT reuse a Param in multiple functions.

                            Instances For

                              Case is the Lean4 representation of gcc_jit_case.

                              Note #

                              A Case represents a case within a switch statement, and is created within a particular Context using Context.newCase. Each case expresses a multivalued range of integer values. You can express single-valued cases by passing in the same value for both min_value and max_value.

                              Instances For

                                ExtendedAsm is the Lean4 representation of gcc_jit_extended_asm. See also Extended Asm.

                                ExtendedAsm is designed to be constructed in multiple steps:

                                • An initial call that creates an empty ExtendedAsm with assembly template.
                                  • Block.addExtendedAsm is used to create asm statement with no control flow
                                  • Block.endWithExtendedAsmGoto is used to create asm goto statement with control flow
                                • A series of calls to add operands to the ExtendedAsm or set attributes.
                                Instances For

                                  Timer is the Lean4 representation of gcc_jit_timer. For detailed descriptions, see The Timing API.

                                  Instances For
                                    • ProgName: LeanGccJit.Core.StrOption

                                      The name of the program, for use as a prefix when printing error messages to stderr. If NULL, or default, libgccjit.so is used.

                                    StrOption is the Lean4 representation of gcc_jit_str_option. See also String Options.

                                    Instances For
                                      • OptimizationLevel: LeanGccJit.Core.IntOption

                                        How much to optimize the code. Valid values are 0-3, corresponding to GCC’s command-line options -O0 through -O3. The default value is 0 (unoptimized).

                                      IntOption is the Lean4 representation of gcc_jit_int_option. See also Integer Options.

                                      Instances For
                                        • DebugInfo: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will attempt to do the right thing so that if you attach a debugger to the process, it will be able to inspect variables and step through your code. Note that you can’t step through code unless you set up source location information for the code (by creating and passing in Location instances).

                                        • DumpInitialTree: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will dump its initial tree representation of your code to stderr (before any optimizations).

                                        • DumpInitialGimple: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will dump the gimple representation of your code to stderr, before any optimizations are performed.

                                        • DumpGenereatedCode: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will dump the final generated code to stderr, in the form of assembly language.

                                        • DumpSummary: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will print information to stderr on the actions it is performing.

                                        • DumpEverything: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will dump copious amount of information on what it’s doing to various files within a temporary directory. Use KeepIntermediates (see below) to see the results. The files are intended to be human-readable, but the exact files and their formats are subject to change.

                                        • SelfCheckGC: LeanGccJit.Core.BoolOption

                                          If true, libgccjit will aggressively run its garbage collector, to shake out bugs (greatly slowing down the compile). This is likely to only be of interest to developers of the library. It is used when running the selftest suite.

                                        • KeepIntermediates: LeanGccJit.Core.BoolOption

                                          If true, Context.compile will not clean up intermediate files written to the filesystem, and will display their location on stderr.

                                        BoolOption is the Lean4 representation of gcc_jit_bool_option. See also Boolean Options.

                                        Instances For

                                          The kind of output to generate (corresponds to gcc_jit_output_kind). Available kinds are: | OutputKind | Typical Suffix | |## Note## Note## Note## Note## Note## Note|## Note## Note## Note## Note## Note## Note## Note## Note--| | Assembler | .s | | ObjectFile | .o | | DynamicLibrary | .so, .dll, .dylib | | Executable | .exe, (no suffix) | See also Output Kinds.

                                          Instances For

                                            TypeEnum is the Lean4 representation of gcc_jit_types. See Standard Types for more details.

                                            Instances For
                                              • Exported: LeanGccJit.Core.FunctionKind

                                                GCC_JIT_FUNCTION_EXPORTED: Function is defined by the client code and visible by name outside of the JIT. This value is required if you want to extract machine code for this function from a Result via Result.getCode.

                                              • Internal: LeanGccJit.Core.FunctionKind

                                                GCC_JIT_FUNCTION_INTERNAL: Function is defined by the client code, but is invisible outside of the JIT. Analogous to a static function.

                                              • Imported: LeanGccJit.Core.FunctionKind

                                                GCC_JIT_FUNCTION_IMPORTED: Function is not defined by the client code; we’re merely referring to it. Analogous to using an “extern” function from a header file.

                                              • AlwaysInline: LeanGccJit.Core.FunctionKind

                                                GCC_JIT_FUNCTION_ALWAYS_INLINE: Function is only ever inlined into other functions, and is invisible outside of the JIT. Analogous to prefixing with inline and adding __attribute__((always_inline))

                                                Inlining will only occur when the optimization level is above 0; when optimization is off, this is essentially the same as GCC_JIT_FUNCTION_INTERNAL.

                                              FunctionKind is the Lean4 representation of gcc_jit_function_kind. This enum controls the kind of function created. See also Function Kinds.

                                              Instances For

                                                TlsModel is the Lean4 representation of gcc_jit_tls_model. It is to be used with LValue.setTlsModel.

                                                Instances For
                                                  • Exported: LeanGccJit.Core.GlobalKind

                                                    GCC_JIT_GLOBAL_EXPORTED: Global is defined by the client code and is visible by name outside of this JIT context via Result.getGlobal (and this value is required for the global to be accessible via that entrypoint).

                                                  • Internal: LeanGccJit.Core.GlobalKind

                                                    GCC_JIT_GLOBAL_INTERNAL: Global is defined by the client code, but is invisible outside of it. Analogous to a static global within a .c file. Specifically, the variable will only be visible within this context and within child contexts.

                                                  • Imported: LeanGccJit.Core.GlobalKind

                                                    GCC_JIT_GLOBAL_IMPORTED: Global is not defined by the client code; we’re merely referring to it. Analogous to using an extern global from a header file.

                                                  GlobalKind is the Lean4 representation of gcc_jit_global_kind. It is to be used with Context.newGlobal. See also Global Variables.

                                                  Instances For

                                                    UnaryOp is the Lean4 representation of gcc_jit_unary_op. It is to be used with Context.newUnaryOp. See also Unary Operations.

                                                    Instances For

                                                      BinaryOp is the Lean4 representation of gcc_jit_binary_op. It is to be used with Context.newBinaryOp or Block.addAssignmentOp. See also Binary Operations.

                                                      Instances For

                                                        Comparison is the Lean4 representation of gcc_jit_comparison. It is to be used with Context.newComparison. See also Comparisons.

                                                        Instances For

                                                          A DynamicBuffer is a buffer used to store a string. This is to be used with Context.registerDumpBuffer. In the backstage, this is just a wrapper around char **.

                                                          Instances For
                                                            @[extern lean_gcc_jit_dynamic_buffer_acquire]

                                                            Create a DynamicBuffer. This will allocate a word as the same size as char *. The initial value of the word is set to NULL.

                                                            @[extern lean_gcc_jit_dynamic_buffer_release]

                                                            Release a DynamicBuffer. This will free the memory allocated by DynamicBuffer.acquire.

                                                            Note #

                                                            The inner string is not freed by this function. It is recommended to call DynamicBuffer.releaseInner before calling this function.

                                                            @[extern lean_gcc_jit_dynamic_buffer_release_inner]

                                                            Release the memory associated with the string stored in the DynamicBuffer. This string is set by libgccjit via Context.compile or Context.compileToFile. It is safe to call this function multiple times as it will reset the string to NULL after its first call.

                                                            @[extern lean_gcc_jit_dynamic_buffer_get_string]

                                                            Get the string stored in the DynamicBuffer. This function returns none if the string is NULL.