Commit graph

734 commits

Author SHA1 Message Date
Joachim Breitner
b1f2fcf758 fix: Escape ? in C literal strings to avoid trigraphs
This fixes #3829
2023-11-06 16:25:00 +01:00
Siddharth Bhat
0b37bad2cb feat: split bitcode optimization and object file building to be outside lean 2023-11-02 23:21:47 +01:00
Mauricio Collares
cfe5a5f188
chore: change simp default to decide := false (#2722) 2023-11-02 10:06:38 +11:00
int-y1
8d7520b36f chore: fix typos in comments 2023-10-08 10:46:05 +02:00
Sebastian Ullrich
4e52283728 fix: FFI signature mismatches 2023-08-18 19:34:21 +02:00
Sebastian Ullrich
f22695fdc5 fix: interpret module initializer at most once 2023-08-16 10:11:50 -07:00
Henrik
35aa2c91a2 feat: LLVM backend: implement the equivalent of -fstack-clash-protection 2023-08-15 14:45:58 +02:00
Siddharth Bhat
0054f6bfac feat: link 'llvm.h.bc' and then set linkage to internal
This obviates the need to play weak linkage games when
we build `lean.h.bc` from `lean.h`. We perform the following steps:

1. We remove the `static` modifier from all definitions in `lean.h`.
   This makes all definitions have `extern` linkage. Thus, when we build
   a `lean.h.bc` using `clang`, we will actually get definitions
   (instead of an empty file)
2. We build `lean.h.bc` from `lean.h` using `clang`.
3. When it comes time to link, we link
   `current_module.bc := LLVMLinkModules2(current_module.bc, lean.h.bc)`.
4. We loop over every symbol that arrived from `lean.h.bc`
   in `current_module.bc` and we then set this symbol to have
   `internal` linkage. This simulates the effect of
   `#include <lean.h>` where every definition in `lean.h`
   has internal linkage.

This yajna, one hopes, pleases the linker gods.
2023-08-14 13:33:46 +02:00
Tobias Grosser
736a21cd5a chore: remove trailing whitespaces in EmitLLVM
For some reason, these two were missed in the last commit.
2023-08-13 16:18:23 +02:00
Tobias Grosser
a0c0c486fd chore: remove trailing whitespace in EmitLLVM
This patch should not result in any functional changes, but
will reduce the diff of an upcoming PR.
2023-08-13 11:07:14 +02:00
Siddharth Bhat
0eddc167b9 feat: LLVM linkage bindings 2023-08-12 16:51:58 +02:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM (#2363) 2023-07-30 10:39:40 +02:00
Siddharth Bhat
073c8fed86 feat: LLVM backend: support for visibility Style & DLL storage
Changes peeled from:
https://github.com/leanprover/lean4/pull/2340

to allow a `stage0` bump on master before merging in the
changes that allow LLVM to build in stage1+.
2023-07-25 11:03:16 +02:00
Mario Carneiro
76023a7c6f fix: don't run [builtin_init] when builtin = false 2023-07-10 08:58:02 -07:00
Leonardo de Moura
4036be4f50 fix: add missing check at IR checker 2023-06-23 08:43:39 -07:00
Mario Carneiro
e0893b70e5 fix: incorrect type for SpecInfo.argKinds 2023-06-21 22:50:29 -07:00
Sebastian Ullrich
90e2288187 fix: interpret initializers in order 2023-06-05 15:46:35 -07:00
Leonardo de Moura
ebcab266c6 chore: remove empty line 2023-05-05 12:18:36 -07:00
Henrik Böving
0e042d8ef6 fix: LCNF simp forgot to mark normalized decls as simplified 2023-05-05 12:17:26 -07:00
Henrik Böving
36f0acfc51 feat: add timing profiling to the new compiler 2023-04-18 12:20:27 +02:00
Siddharth
5349a089e5
feat: add --target flag for LLVM backend to build objects of a different architecture (#2034)
* feat: add --target flag for LLVM backend to build objects of a different architecture

* chore: remove dead comment

* Update src/Lean/Compiler/IR/EmitLLVM.lean

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* chore: normalize indentation in src/util/shell.cpp

* chore: strip trailing whitespace

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2023-01-15 12:00:10 -08:00
Siddharth Bhat
26edfc33f5 chore: remove unused isTaggedPtr from IR.
This reduces the surface area of `unimplemented` in the LLVM backend,
and also removes dead code in the compiler.
2023-01-15 09:24:41 -08:00
Siddharth Bhat
ae4f2de951 fix: metadata codegen for LLVM 2023-01-12 17:39:56 +01:00
Siddharth Bhat
0900aa1348 feat: implement unreachable codegen for LLVM
Also add a test case that exercises `unreachable` code
generation.
2023-01-12 09:17:41 +01:00
Siddharth
5615ba6606
feat: implement uset for LLVM (#2025)
Fixes #1958.
2023-01-09 12:25:37 +00:00
Siddharth
a0a0463451
fix: codegen initUnboxed correctly in LLVM backend (#2015)
Closes #2004.

In porting the bugfix from
6eb852e28f,
I noticed that the LLVM backend was incorrectly generating declaration
initializers (in `callIODeclInitFn`), by assuming the return type of the
initializer is the return type of the declaration. Rather, it must be be
`lean_object`, since the initializer returns an `IO a` value which must be unpacked.

TODO: stop using the `getOrCreateFunction` pattern pervasively.
  perform the `create` at the right location, and the `get`
  at the correct location.
2023-01-07 16:26:53 +01:00
Leonardo de Moura
069f08e3a3 chore: move getUnboxOpName 2023-01-04 08:07:32 -08:00
Leonardo de Moura
6eb852e28f fix: fixes #1998 2023-01-03 16:01:27 -08:00
Siddharth
b6eb780144
feat: LLVM backend (#1837) 2022-12-30 12:45:30 +01:00
Leonardo de Moura
0a031fc9bb chore: replace Expr.forEach with Expr.forEachWhere 2022-12-01 05:19:32 -08:00
Leonardo de Moura
7c5d91ebc3 fix: avoid hygienic ++ hygienic at Specialize.lean 2022-11-30 06:31:03 -08:00
Henrik Böving
5286c2b5aa feat: optimize mul/div into shift operations 2022-11-29 01:05:06 +01:00
Siddharth
4d47c8abc6
feat: add LLVM C API bindings (#1497)
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-11-21 09:50:01 +01:00
Sebastian Ullrich
a4abbf07b8 chore: remove remnants of C++ format 2022-11-18 06:11:24 -08:00
Henrik Böving
6fe52cac41 doc: explain some decisions in ElimDeadBranches 2022-11-16 08:17:13 -08:00
Henrik Böving
66009a5cd3 feat: constant folding for decision procedures 2022-11-16 08:17:13 -08:00
Henrik Böving
5a397c8525 feat: ElimDeadBranches for LCNF 2022-11-16 08:17:13 -08:00
Leonardo de Moura
5654d8465d fix: fixes #1822 2022-11-13 18:13:29 -08:00
Leonardo de Moura
a87f0e25de feat: add compiler.checkTypes for sanity checking 2022-11-13 17:45:21 -08:00
Leonardo de Moura
854e655940 chore: document implementedBy := true use at phase 1 2022-11-13 15:47:13 -08:00
Leonardo de Moura
c147059fd7 fix: fixes #1812 2022-11-10 08:58:09 -08:00
Leonardo de Moura
9b02f982e2 chore: add ppCode' 2022-11-10 08:07:35 -08:00
Leonardo de Moura
b4d13a8946 refactor: LetExpr => LetValue
We use "let value" in many other places in the code base.
2022-11-07 18:51:07 -08:00
Leonardo de Moura
e8b4a8875c fix: type argument that is a fvar at FixedParams.lean 2022-11-07 18:18:07 -08:00
Leonardo de Moura
9399164201 fix: simpCasesOnCtor? 2022-11-07 18:18:06 -08:00
Leonardo de Moura
a5dadfdb7a feat: activate all passes 2022-11-07 16:18:36 -08:00
Leonardo de Moura
828a815821 fix: simpAppApp? 2022-11-07 16:18:36 -08:00
Leonardo de Moura
92faeec832 fix: add Simp.findFunDecl'?
It may look like a simple optimization but affects the inlining
heuristics. Example:
```
fun f ... := ...
let x_1 := f
let x_2 := x_1 a
let x_3 := x_1 b
...
```
Before this commit, `f` was not being marked as being used multiple times.
2022-11-07 16:18:36 -08:00
Leonardo de Moura
f342d0ea35 fix: avoid unnecessary whitespace at LCNF pretty printer 2022-11-07 16:18:36 -08:00
Leonardo de Moura
cf13b29760 fix: nasty bug due to #1804 2022-11-07 16:18:36 -08:00