chore: disable benchtest at debug and fsanitize

.github/workflows/ci.yml

@@ -67,13 +67,13 @@ jobs:
             os: ubuntu-latest
             CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
             # exclude seriously slow tests
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: Linux fsanitize
             os: ubuntu-latest
             # turn off custom allocator & symbolic functions to make LSAN do its magic
             CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF
             # exclude seriously slow/problematic tests (laketests crash)
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: macOS
             os: macos-latest
             release: true

src/Init/Data/Hashable.lean

@@ -58,3 +58,7 @@ instance : Hashable Int where
 
 instance (P : Prop) : Hashable P where
   hash _ := 0
+
+/-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
+@[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
+  mixHash u 11

src/Lean/Util/FindExpr.lean

@@ -4,52 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Expr
+import Lean.Util.PtrSet
 
 namespace Lean
 namespace Expr
-
 namespace FindImpl
 
-abbrev cacheSize : USize := 8192 - 1
+unsafe abbrev FindM := StateT (PtrSet Expr) Id
 
-structure State where
-  keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
+@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+  if (← get).contains e then
+    failure
+  modify fun s => s.insert e
 
-abbrev FindM := StateT State Id
-
-unsafe def visited (e : Expr) (size : USize) : FindM Bool := do
-  let s ← get
-  let h := ptrAddrUnsafe e
-  let i := h % size
-  let k := s.keys.uget i lcProof
-  if ptrAddrUnsafe k == h then
-    pure true
-  else
-    modify fun s => { keys := s.keys.uset i e lcProof }
-    pure false
-
-unsafe def findM? (p : Expr → Bool) (size : USize) (e : Expr) : OptionT FindM Expr :=
+unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
   let rec visit (e : Expr) := do
-    if (← visited e size)  then
-      failure
-    else if p e then
+    checkVisited e
+    if p e then
       pure e
     else match e with
-      | Expr.forallE _ d b _   => visit d <|> visit b
-      | Expr.lam _ d b _       => visit d <|> visit b
-      | Expr.mdata _ b         => visit b
-      | Expr.letE _ t v b _    => visit t <|> visit v <|> visit b
-      | Expr.app f a           => visit f <|> visit a
-      | Expr.proj _ _ b        => visit b
-      | _                      => failure
+      | .forallE _ d b _ => visit d <|> visit b
+      | .lam _ d b _     => visit d <|> visit b
+      | .mdata _ b       => visit b
+      | .letE _ t v b _  => visit t <|> visit v <|> visit b
+      | .app f a         => visit f <|> visit a
+      | .proj _ _ b      => visit b
+      | _                => failure
   visit e
 
-
-unsafe def initCache : State :=
-  { keys    := mkArray cacheSize.toNat (cast lcProof ()) }
-
 unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  Id.run <| findM? p cacheSize e |>.run' initCache
+  Id.run <| findM? p e |>.run' mkPtrSet
 
 end FindImpl
 
@@ -59,13 +43,13 @@ def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
   if p e then
     some e
   else match e with
-    | Expr.forallE _ d b _   => find? p d <|> find? p b
-    | Expr.lam _ d b _       => find? p d <|> find? p b
-    | Expr.mdata _ b         => find? p b
-    | Expr.letE _ t v b _    => find? p t <|> find? p v <|> find? p b
-    | Expr.app f a           => find? p f <|> find? p a
-    | Expr.proj _ _ b        => find? p b
-    | _                      => none
+    | .forallE _ d b _ => find? p d <|> find? p b
+    | .lam _ d b _     => find? p d <|> find? p b
+    | .mdata _ b       => find? p b
+    | .letE _ t v b _  => find? p t <|> find? p v <|> find? p b
+    | .app f a         => find? p f <|> find? p a
+    | .proj _ _ b      => find? p b
+    | _                => none
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
@@ -81,32 +65,31 @@ inductive FindStep where
 
 namespace FindExtImpl
 
-unsafe def findM? (p : Expr → FindStep) (size : USize) (e : Expr) : OptionT FindImpl.FindM Expr :=
+unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
   visit e
 where
   visitApp (e : Expr) :=
     match e with
-    | Expr.app f a .. => visitApp f <|> visit a
+    | .app f a .. => visitApp f <|> visit a
     | e => visit e
 
   visit (e : Expr) := do
-    if (← FindImpl.visited e size)  then
-      failure
-    else match p e with
-      | FindStep.done  => failure
-      | FindStep.found => pure e
-      | FindStep.visit =>
+    FindImpl.checkVisited e
+    match p e with
+      | .done  => failure
+      | .found => pure e
+      | .visit =>
         match e with
-        | Expr.forallE _ d b _   => visit d <|> visit b
-        | Expr.lam _ d b _       => visit d <|> visit b
-        | Expr.mdata _ b         => visit b
-        | Expr.letE _ t v b _    => visit t <|> visit v <|> visit b
-        | Expr.app ..            => visitApp e
-        | Expr.proj _ _ b        => visit b
-        | _                      => failure
+        | .forallE _ d b _ => visit d <|> visit b
+        | .lam _ d b _     => visit d <|> visit b
+        | .mdata _ b       => visit b
+        | .letE _ t v b _  => visit t <|> visit v <|> visit b
+        | .app ..          => visitApp e
+        | .proj _ _ b      => visit b
+        | _                => failure
 
 unsafe def findUnsafe? (p : Expr → FindStep) (e : Expr) : Option Expr :=
-  Id.run <| findM? p FindImpl.cacheSize e |>.run' FindImpl.initCache
+  Id.run <| findM? p e |>.run' mkPtrSet
 
 end FindExtImpl
 

src/Lean/Util/PtrSet.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2023 Leonardo de Moura. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Data.HashSet
+
+namespace Lean
+
+structure Ptr (α : Type u) where
+  value : α
+
+unsafe instance : Hashable (Ptr α) where
+  hash a := hash64 (ptrAddrUnsafe a).toUInt64
+
+unsafe instance : BEq (Ptr α) where
+  beq a b := ptrAddrUnsafe a == ptrAddrUnsafe b
+
+/--
+Set of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
+-/
+unsafe def PtrSet (α : Type) :=
+  HashSet (Ptr α)
+
+unsafe def mkPtrSet {α : Type} (capacity : Nat := 64) : PtrSet α :=
+  mkHashSet capacity
+
+unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α :=
+  HashSet.insert s { value := a }
+
+unsafe abbrev PtrSet.contains (s : PtrSet α) (a : α) : Bool :=
+  HashSet.contains s { value := a }
+
+end Lean

tests/bench/dag_hassorry_issue.lean

@@ -0,0 +1,57 @@
+import Lean
+
+open Lean
+
+def mkEqX (bidx : Nat) : Expr :=
+  mkApp3 (mkConst ``Eq [levelOne]) (mkConst ``Nat []) (.bvar bidx) (.bvar bidx)
+
+def mkReflX (bidx : Nat) : Expr :=
+  mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Nat []) (.bvar bidx)
+
+def mkAnds (n : Nat) : Expr :=
+  match n with
+  | 0 => mkConst ``True []
+  | n+1 => mkAnd (mkEqX n) (mkAnds n)
+
+def mkAndIntro (p q h₁ h₂ : Expr) : Expr :=
+  mkApp4 (mkConst ``And.intro []) p q h₁ h₂
+
+def mkRefls (n : Nat) (ands : List Expr) : Expr :=
+  match n, ands with
+  | n+1, and::ands => mkAndIntro (mkEqX n) and (mkReflX n) (mkRefls n ands)
+  | _, _ => mkConst ``True.intro []
+
+def mkLambdas (n : Nat) (p : Expr) : Expr :=
+  match n with
+  | 0 => p
+  | n+1 => .lam `x (mkConst ``Nat []) (mkLambdas n p) .default
+
+def mkForalls (n : Nat) (p : Expr) : Expr :=
+  match n with
+  | 0 => p
+  | n+1 => .forallE `x (mkConst ``Nat []) (mkForalls n p) .default
+
+partial def toAndList (ands : Expr) (acc : List Expr) : List Expr :=
+  if ands.isAppOf ``And then
+    toAndList (ands.getArg! 1) (ands.getArg! 1 :: acc)
+  else
+    (ands :: acc).reverse
+
+def test (n : Nat) : CoreM Unit := do
+  let and := mkAnds n
+  let type := mkForalls n and
+  let andList := toAndList and []
+  let value := mkLambdas n (mkRefls n andList)
+  addDecl <| .thmDecl {
+    name := (`test_abst).appendIndexAfter n
+    levelParams := []
+    type, value
+  }
+  return ()
+
+def main (args : List String) : IO Unit := do
+  let [size] := args | throw (IO.userError s!"unexpected number of arguments, numeral expected")
+  initSearchPath (← findSysroot)
+  let env ← importModules [{ module := `Init.Prelude }] {} 0
+  discard <| test size.toNat! |>.toIO { fileName := "<test>", fileMap := default } { env }
+  IO.println "ok"

tests/bench/dag_hassorry_issue.lean.args

@@ -0,0 +1 @@
+10000

tests/bench/dag_hassorry_issue.lean.expected.out

@@ -0,0 +1 @@
+ok