Foto de capa de Laboratório de Compiladores
Laboratório de Compiladores

Laboratório de Compiladores

Pesquisa

Belo Horizonte, Minas Gerais 8.023 seguidores

Criar 'pontes' que conectam pessoas a máquinas

Sobre nós

O Laboratório de Compiladores (LaC) tem por missão aumentar a produtividade dos programadores, permitindo-lhes utilizar linguagens de programação cada vez mais expressivas para controlar processadores cada vez mais complexos. Com tal intuito, os pesquisadores do LaC criam 'pontes' que conectam pessoas a máquinas, por meio de uma linguagem comum entendida nesses dois mundos. Para cumprir a missão do laboratório, seus participantes desenvolvem técnicas de análise de programas e de otimização de código. Várias dessas técnicas são utilizadas em compiladores importantes, como a análise de divergências, presente em LLVM, e a especialização de valores, usada no Firefox. Algumas das ferramentas desenvolvidas no laboratório têm hoje muitos usuários, como o compilador DawnCC, que paraleliza programas automaticamente, Psyche-c, que faz a inferência de tipos na linguagem de programação C e Enfield, um alocador de qubits para computadores quânticos. Tais ferramentas, e a teoria por trás delas, surge de pesquisa de ponta, atualmente aplicada no desenvolvimento de compiladores para sistemas embarcados, para navegadores web, para GPUs ou até mesmo para aceleradores quânticos. Vários desses projetos são financiados por empresas privadas, como Intel, Google, Nvidia e LG Electronics. Essas mesmas empresas absorvem os mestres e doutores formados pelo laboratório. Aliando prática e teoria, os pesquisadores do LaC contribuem para aumentar a qualidade de programas, tornando-os mais rápidos, mais energeticamente eficientes e mais seguros.

Site
http://lac.dcc.ufmg.br/
Setor
Pesquisa
Tamanho da empresa
11-50 funcionários
Sede
Belo Horizonte, Minas Gerais
Tipo
Órgão governamental
Fundada em
2015
Especializações
Compiladores, Otimização de código de máquina, Paralelização de algoritmos e Teoria de compilação

Localidades

  • Principal

    Rua Reitor Píres Albuquerque, ICEx

    Belo Horizonte, Minas Gerais 31270-901, BR

    Como chegar

Funcionários da Laboratório de Compiladores

Atualizações

  • Church Booleans encode the Boolean values true and false, e.g.: True = \a.\b.a False = \a.\b.b Using this convention, we can define all Boolean operations (AND, OR, NOT, etc, etc). We can even write programs with them. However, in practice, this style works more smoothly in dynamically typed languages. In statically typed languages, the type system can get in the way. For instance, try defining XOR in Standard ML/NJ and observe what happens. More generally, Church encoding is a technique introduced by Alonzo Church for representing data (such as booleans, numbers, and pairs) purely using functions in the λ-calculus: https://lnkd.in/d4fSduus #programming #mathematics #academia #logic

    • Não foi fornecido texto alternativo para esta imagem
  • Thompson's "Trusting Trust" attack is a circular exploit where a malicious compiler recognizes when it is compiling a specific program, such as a login utility [1,3], and injects a backdoor into the binary. To remain invisible, the compiler is also programmed to recognize when it is compiling its own source code; in this case, it injects the malicious "backdoor-inserting" logic into the new version of the compiler binary. Because this secondary payload exists only in the executable and not in the source code, developers will not find anything wrong if they audit the source code, yet every version of the compiler they build from that "clean" source will continue to compromise any software it processes. The Gödel-based certification process [2, 4] proposed by Guilherme Silva works by mapping the structure of a program's source code and its compiled binary into a unique integer (a Gödel number) using a series of injective prime-power products. Each programming construct, such as an assignment or a loop, and its position in the abstract syntax tree are assigned specific prime factors, ensuring that any modification, deletion, or reordering of instructions results in a different final integer. The Göde-based certification prevents the "trusting trust" attack because it establishes a mathematical contract that is independent of the compiler's internal logic. Hence, if a malicious compiler attempts to inject a backdoor into the binary, the resulting Gödel number derived from that binary will not match the number derived from the original source code. Because the certification rules are simple enough to be verified by a small, auditable "checker" or even by hand for critical sections, the attacker cannot hide unauthorized code changes within the translation process without breaking the structural identity of the program. References: [1] Russ Cox: Running the “Reflections on Trusting Trust” Compiler - Revisiting Ken Thompson’s sourceless backdoor. ACM Queue Volume 23, Issue 6, 2026 - This paper shows how to run Thompson's Hack on a real-world setting. https://lnkd.in/dHXa6zqX [2] Guilherme Silva, Fernando Pereira: Certified Compilation based on Gödel Numbers. CoRR abs/2508.12054 (2025) https://lnkd.in/dyRVtGcs Code: [3] An earlier description of Thompson's Hack, also by Russ Cox: https://lnkd.in/eZ9KR9At [4] The Charon Compiler implements the Gödel-based certification approach: https://lnkd.in/eNJ4bTk7

    • Thompson's "Trusting Trust" attack is a circular exploit where a malicious compiler recognizes when it is compiling a specific program, such as a login utility [1,3], and injects a backdoor into the binary.

To remain invisible, the compiler is also programmed to recognize when it is compiling its own source code; in this case, it injects the malicious "backdoor-inserting" logic into the new version of the compiler binary. Because this secondary payload exists only in the executable and not in the source code, developers will not find anything wrong if they audit the source code, yet every version of the compiler they build from that "clean" source will continue to compromise any software it processes.

The Gödel-based certification process [2, 4] proposed by Guilherme Oliveira works by mapping the structure of a program's source code and its compiled binary into a unique integer (a Gödel number) using a series of injective prime-power products.
  • Global Value Numbering (GVN) is a classic compiler optimization that detects when different expressions compute the same value. The idea is to assign a "value number" to each expression such that two expressions get the same number if they are guaranteed to produce the same result. Using these numbers, the compiler can eliminate redundant computations (a form of common subexpression elimination) and sometimes simplify code further. Want to know how it works? LLVM has a production-quality GVN pass. Here are some pointers: * Header: https://lnkd.in/dtW2pki8 * Implementation: https://lnkd.in/ddy__7n3 In LLVM, Global Value Numbering (GVN) assigns a value number to each SSA value based on the computation it represents, so that different instructions that compute the same result receive the same number. It builds canonical representations of expressions (opcode + operands, normalized when possible), uses hashing to detect previously seen equivalent expressions, and then reuses existing values instead of recomputing them. Notice that value numbers are not restricted to expressions within a single basic block. Whole program slices can receive value numbers. Take a look into the paper below to see how that's done: Rafael Alvarenga, Daniel Augusto Costa de Sá, Rodrigo Rocha, Fernando Pereira: Idempotent Slices with Applications to Code-Size Reduction. https://lnkd.in/eyZ9f5Ea

    • Global Value Numbering (GVN) is a classic compiler optimization that detects when different expressions compute the same value.

The idea is to assign a "value number" to each expression such that two expressions get the same number if they are guaranteed to produce the same result. Using these numbers, the compiler can eliminate redundant computations (a form of common subexpression elimination) and sometimes simplify code further.

Want to know how it works? LLVM has a production-quality GVN pass. Here are some pointers:
* Header: https://llvm.org/doxygen/GVN_8h_source.html
* Implementation: https://llvm.org/doxygen/GVN_8cpp_source.html
  • In this new chapter (https://lnkd.in/dGpuPvUn), Douglas Viana Coutinho explains how we can solve liveness analysis using a neural network. Liveness is a classic compiler analysis: a variable is considered live at a program point if its current value may be used along some path in the future before being redefined. Compilers need this information to carry out optimizations such as register allocation, dead-code elimination, and the elision of uninitialized variables. Liveness has a simple, polynomial-time solution. Yet, Douglas shows how to solve it using a stochastic model, revisiting an experiment earlier reported by Cummins et al. [1]. Douglas translates MLIR programs to a code representation called ProGraML, and uses liveness information to train a graph neural network, which is then able to predict liveness information for unseen programs. Douglas is not trying to produce a new solution to liveness analysis. Rather, he is showing how to tune a neural network to solve compiler-related tasks. The same approach could be used, for instance, to solve tasks that are statistical in nature, such as profile prediction [2], choice of optimization sequences [3], or binary diffing [4]. References [1] Chris Cummins et al. ProGraML: A Graph-based Program Representation for Data Flow Analysis and Compiler Optimizations. ICML 2021. https://lnkd.in/d5vr-hbt [2] Angelica Moreira, Ph.D. et al. VESPA: Static Profiling for Binary Optimization. OOPSLA 2021. https://lnkd.in/eHm-JKhq [3] Anderson Faustino et al. Exploring the Space of Optimization Sequences for Code-Size Reduction: Insights and Tools. Compiler Construction 2021. https://lnkd.in/dqRXtRU [4] VenkataKeerthy S et al. VexIR2Vec: An Architecture-Neutral Embedding Framework for Binary Similarity. ACM Transactions on Software Engineering and Methodology. 2025. https://lnkd.in/drvxg7dt.

    • Não foi fornecido texto alternativo para esta imagem
  • The paper "Vectorization of Verilog Designs and its Effects on Verification and Synthesis" is available on arXiv (https://lnkd.in/duRcxp-g). Vectorization is a classic compiler optimization that groups multiple operations into a single operation by leveraging bitwide registers and instructions available in modern architectures. At first glance, one might think that vectorization does not make much sense in Verilog; after all, the underlying hardware must ultimately represent bits as individual signals. However, vectorization has an important side effect: it reduces the symbolic complexity of Verilog designs, thereby greatly helping EDA tools such as Jasper and Genus. In this paper [1], Maria Fernanda Guimarães explains how to implement vectorization for Verilog designs. Vectorization in this domain differs significantly from what is done in classic programming languages such as C or Rust. In both settings, vectorization involves identifying recurring computation patterns and collapsing them into a more compact representation. However, traditional compiler vectorization focuses on temporal recurrences, that is, repeated executions of the same operations across loop iterations. In contrast, the vectorization presented in this paper targets spatial recurrences that arise in RTL designs. Verilog descriptions often express word-level behavior through replicated bit-level assignments that differ only in constant indices. Our approach detects groups of assignments that are structurally equivalent but operate on distinct signals, and rewrites them as single vector-level expressions. Thus, while traditional vectorization is loop-centric, our technique identifies structurally replicated logic even in the absence of explicit iteration constructs. The vectorizer was implemented in CIRCT. Part of it is already available in the CIRCT code base. The complete implementation, including artifacts to reproduce the experiments in the paper, is available at https://lnkd.in/dzdknhpG. This project is sponsored by Cadence at UFMG's Compilers Lab. References: [1] Maria Fernanda Guimarães, Ulisses Rosa, Ian Trudel, João Victor Amorim Vieira, Augusto Mafra, Mirlaine Crepalde, Fernando Pereira: Vectorization of Verilog Designs and its Effects on Verification and Synthesis. https://lnkd.in/duRcxp-g

    • The paper "Vectorization of Verilog Designs and its Effects on Verification and Synthesis" is available on arXiv (https://doi.org/10.48550/arXiv.2603.17099).
  • Dynamic dispatch is one of the quintessential features of object-oriented programs: the implementation of a method depends on the dynamic type of the object. The implementation of dynamic dispatch is not exactly trivial. Given a call such as "o.m()", there might be multiple implementations of "m" as potential targets. The runtime environment must determine the correct one! How is dynamic dispatch implemented in different languages? The answer can vary depending on whether the language is statically or dynamically typed. Dynamic dispatch can have a very efficient implementation in statically typed languages: that is the beauty of virtual tables. What is a virtual table, and how can it speed up the implementation of method calls? It is also possible to implement dynamic dispatch efficiently in some dynamically typed languages. In these cases, one popular technique is the use of polymorphic inline caches. For an overview of virtual tables, see Chapter 20, "Code Generation for Object-Oriented Features", in UFMG's Lecture Notes for Compiler Construction: https://lnkd.in/dK9NYaae For an overview of polymorphic inline caches, see the DCC888 class on Just-in-Time Code Optimizations: https://lnkd.in/d-rAHM4N

    • Não foi fornecido texto alternativo para esta imagem
  • Since March 2026, BarraCUDA implements divergence-aware register allocation! GPU code may contain either divergent or uniform variables. Uniform variables hold the same value for every thread in a warp. When spilling uniform variables, the register allocator can keep a single copy of the value instead of replicating it for each thread in the warp. This optimization is known as divergence-aware register allocation. To determine which variables are divergent, the compiler uses a static analysis called Divergence Analysis [1]. Divergence-aware register allocation can lead to impressive results. When compiling Moa, a Monte Carlo neutron transport code, it reduces the number of instructions in the final binary by 28.4% (from 9,448 to 6,761). For those interested in advanced compiler construction, we cannot recommend BarraCUDA enough. Its register allocator (ra_ssa.c, available at https://lnkd.in/dkypcYNg) is a treasure trove. You will find everything there: SSA construction and destruction, liveness and divergence analysis, and register allocation. BarraCUDA is distributed under the Apache-2.0 license and is written in C99 by Zane Hambly. Link: https://lnkd.in/d5uZNMaQ [1] Diogo Sampaio, Rafael M., Caroline Collange, Fernando Pereira: Divergence Analysis. ACM Transactions on Programming Languages and Systems, 35(4): 13:1–13:36 (2013). Link: https://lnkd.in/dNtnD4kt

    • Since March 2026, BarraCUDA implements divergence-aware register allocation!
  • Given a program P and an assignment `a = ...` within P, the idempotent slice for `a` is the smallest subprogram of P that always produces the same value for `a` as the original program. Program slices are useful for many purposes, including redundancy elimination, reordering computations, and outlining code to reduce program size. In the paper "Idempotent Slices with Applications to Code-Size Reduction", Rafael Alvarenga shows how to compute such slices both soundly and efficiently. The key idea is to use a program representation called "Gated Static Single Assignment (GSA)" form. GSA converts control dependencies into data dependencies by associating the predicates that control branches with the assignments whose execution depends on those branches. Rafael Alvarenga, Daniel Augusto Costa de Sá, Rodrigo Rocha, Fernando Pereira. Idempotent Slices with Applications to Code-Size Reduction. Link: https://lnkd.in/eyZ9f5Ea

    • Given a program P and an assignment `a = ...` within P, the idempotent slice for `a` is the smallest subprogram of P that always produces the same value for `a` as the original program.

Program slices are useful for many purposes, including redundancy elimination, reordering computations, and outlining code to reduce program size.

In the paper "Idempotent Slices with Applications to Code-Size Reduction", Rafael Alvarenga shows how to compute such slices both soundly and efficiently. The key idea is to use a program representation called "Gated Static Single Assignment (GSA)" form. GSA converts control dependencies into data dependencies by associating the predicates that control branches with the assignments whose execution depends on those branches.

Rafael Alvarenga de Azevedo, Daniel Augusto Costa de Sá, Rodrigo Caetano Rocha, Fernando Pereira. Idempotent Slices with Applications to Code-Size Reduction.
Link: https://arxiv.org/abs/2603.09726
  • One way to learn something about a program is to run it. However, this approach has limitations: execution might not terminate, and even when it does, it may never reach the program point we care about. Abstract interpretation addresses this problem. Instead of executing the program on concrete values, it “runs” the program on abstract values that summarize many concrete states at once. This allows the analysis to explore all program paths and program points. The trade-off is that the results are approximate: the abstract execution over-approximates the program’s possible behaviors. To “run” the program, the static analysis builds an interpreter—albeit an abstract one. Instead of evaluating variables to their concrete values, the abstract interpreter evaluates them to abstract values. But the interpreter is itself a program! We can execute it, and when it terminates it yields a sound approximation of the program’s behavior. For instance, consider the assignment: `a = b + c` A concrete interpreter evaluates this statement as follows: * Look up the concrete values of `b` and `c` in the current state, and update the value of `a` to `b + c`. An abstract interpreter that tracks constants evaluates it differently: * Look up the abstract values of `b` and `c` in the abstract state. * Update the value of `a` to  (i) `V[b] + V[c]` if both `V[b]` and `V[c]` are constants, or  (ii) `NotAConstant` otherwise. Static Program Analysis at UFMG: https://lnkd.in/dG8Wrv5k

    • One way to learn something about a program is to run it. However, this approach has limitations: execution might not terminate, and even when it does, it may never reach the program point we care about.

Abstract interpretation addresses this problem. Instead of executing the program on concrete values, it “runs” the program on abstract values that summarize many concrete states at once. This allows the analysis to explore all program paths and program points. The trade-off is that the results are approximate: the abstract execution over-approximates the program’s possible behaviors.

To “run” the program, the static analysis builds an interpreter—albeit an abstract one. Instead of evaluating variables to their concrete values, the abstract interpreter evaluates them to abstract values. But the interpreter is itself a program! We can execute it, and when it terminates it yields a sound approximation of the program’s behavior.
  • Modern programming languages are typically designed using the theory of context-free grammars. In practice, however, almost no widely used general-purpose language is strictly context-free. Go comes close. Its parser (https://lnkd.in/eMfvDpeT) looks very much like a context-free parser (though we would be curious to hear from people who know the implementation well). Still, there are a few interesting compromises. For instance, the parseCallOrConversion routine feels a bit like a workaround. In Go, an expression such as Foo(x) can denote either a function call or a type conversion. The grammar appears to be deliberately structured so that both cases share the same syntactic shape in the parse tree; the distinction is resolved later. In this sense, the grammar avoids introducing additional context sensitivity, even though the language semantics ultimately require it. This trick, a context-free structure followed by a disambiguation phase, is pretty much what we did when parsing C snippets in Psyche-C, a type inference engine for C [1]. Leandro T. C. Melo, Rodrigo G. Ribeiro, Breno Campos and Fernando Pereira. Type Inference for C: Applications to the Static Analysis of Incomplete Programs. ACM TOPLAS, 2020. Link: https://lnkd.in/d3N3rxt #compiler #programming #parsing #theory

    • Modern programming languages are typically designed using the theory of context-free grammars. In practice, however, almost no widely used general-purpose language is strictly context-free.

Páginas semelhantes

Visualizar vagas