chore: CI: enable leak sanitizer again (#11339)

Author: Kha

.github/workflows/build-template.yml

@@ -46,8 +46,6 @@ jobs:
       CCACHE_MAXSIZE: 400M
       # squelch error message about missing nixpkgs channel
       NIX_BUILD_SHELL: bash
-      # TODO
-      ASAN_OPTIONS: detect_leaks=0
       LSAN_OPTIONS: max_leaks=10
       # somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
       CXX: c++

.github/workflows/ci.yml

@@ -153,7 +153,7 @@ jobs:
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
       # 2: nightlies
-      # 2: PRs with `release-ci` label, full releases
+      # 3: PRs with `release-ci` label, full releases
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -259,15 +259,15 @@ jobs:
               },
               {
                 "name": "Linux fsanitize",
-                "os": "ubuntu-latest",
+                // Always run on large if available, more reliable regarding timeouts
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
-                // do not have nightly release wait for this
-                "secondary": level <= 2,
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // exclude seriously slow/problematic tests (laketests crash, async_base_functions timeouts)
-                "CTEST_OPTIONS": "-E '(interactive|pkg|lake|bench)/|treemap|StackOverflow|async_base_functions'"
+                // `StackOverflow*` correctly triggers ubsan
+                // `reverse-ffi` fails to link in sanitizers
+                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi'"
               },
               {
                 "name": "macOS",

CMakePresets.json

@@ -41,7 +41,7 @@
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 ASAN_OPTIONS=detect_leaks=0"
+        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/sanitize"

src/Lean/Compiler/IR/Boxing.lean

@@ -26,12 +26,6 @@ Assumptions:
   `Expr.isShared`, `Expr.isTaggedPtr`, and `FnBody.set`.
 -/
 
-def mkBoxedName (n : Name) : Name :=
-  Name.mkStr n "_boxed"
-
-def isBoxedName (name : Name) : Bool :=
-  name matches .str _ "_boxed"
-
 abbrev N := StateM Nat
 
 private def N.mkFresh : N VarId :=

src/Lean/Compiler/IR/CompilerM.lean

@@ -139,10 +139,20 @@ def findEnvDecl (env : Environment) (declName : Name) (includeServer := false):
 private def findInterpDecl (env : Environment) (declName : Name) : Option Decl :=
   findEnvDecl (includeServer := true) env declName
 
+namespace ExplicitBoxing
+
+def mkBoxedName (n : Name) : Name :=
+  Name.mkStr n "_boxed"
+
+def isBoxedName (name : Name) : Bool :=
+  name matches .str _ "_boxed"
+
+end ExplicitBoxing
+
 /-- Like ``findInterpDecl env (declName ++ `_boxed)`` but with optimized negative lookup. -/
 @[export lean_ir_find_env_decl_boxed]
 private def findInterpDeclBoxed (env : Environment) (declName : Name) : Option Decl :=
-  let boxed := declName ++ `_boxed
+  let boxed := ExplicitBoxing.mkBoxedName declName
   -- Important: get module index of base name, not boxed version. Usually the interpreter never
   -- does negative lookups except in the case of `call_boxed` which must check whether a boxed
   -- version exists. If `declName` exists as an imported declaration but `declName'` doesn't, the

src/Lean/Environment.lean

@@ -1718,7 +1718,7 @@ passing (a prefix of) the file names to `readModuleDataParts`. `mod` is used to
 arbitrary but deterministic base address for `mmap`.
 -/
 @[extern "lean_save_module_data_parts"]
-opaque saveModuleDataParts (mod : @& Name) (parts : Array (System.FilePath × ModuleData)) : IO Unit
+opaque saveModuleDataParts (mod : @& Name) (parts : @& Array (System.FilePath × ModuleData)) : IO Unit
 
 /--
 Loads the module data from the given file names. The files must be (a prefix of) the result of a

src/Std/Data/ByteSlice.lean

@@ -182,7 +182,7 @@ def toByteArray (s : ByteSlice) : ByteArray :=
 Comparison function
 -/
 @[extern "lean_byteslice_beq"]
-protected def beq (a b : ByteSlice) : Bool :=
+protected def beq (a b : @& ByteSlice) : Bool :=
   a.toByteArray == b.toByteArray
 
 instance : BEq ByteSlice := ⟨ByteSlice.beq⟩

src/Std/Internal/UV/System.lean

@@ -138,7 +138,7 @@ opaque cwd : IO String
 Changes the current working directory.
 -/
 @[extern "lean_uv_chdir"]
-opaque chdir : String → IO Unit
+opaque chdir : @& String → IO Unit
 
 /--
 Gets the path to the current user's home directory.

src/kernel/environment.cpp

@@ -28,7 +28,7 @@ extern "C" object* lean_kernel_set_diag(object*, object*);
 extern "C" uint8* lean_kernel_diag_is_enabled(object*);
 
 void diagnostics::record_unfold(name const & decl_name) {
-    m_obj = lean_kernel_record_unfold(to_obj_arg(), decl_name.to_obj_arg());
+    m_obj = lean_kernel_record_unfold(m_obj, decl_name.to_obj_arg());
 }
 
 scoped_diagnostics::scoped_diagnostics(environment const & env, bool collect) {

src/library/ir_interpreter.cpp

@@ -216,7 +216,8 @@ string_ref get_symbol_stem(elab_environment const & env, name const & fn) {
 
 extern "C" object * lean_ir_format_fn_body_head(object * b);
 std::string format_fn_body_head(fn_body const & b) {
-    return string_to_std(lean_ir_format_fn_body_head(b.to_obj_arg()));
+    object_ref s(lean_ir_format_fn_body_head(b.to_obj_arg()));
+    return string_to_std(s.raw());
 }
 
 static bool type_is_scalar(type t) {