From 49ac091f090789b1401c29d74a984a4fe7906a03 Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Thu, 2 May 2024 17:12:45 +0300 Subject: [PATCH 1/9] add tests --- tests/idris2/total/total025/Issue-2995.idr | 18 ++++++++++++++++++ tests/idris2/total/total025/expected | 1 + tests/idris2/total/total025/run | 3 +++ tests/idris2/total/total026/Issue-2995.idr | 18 ++++++++++++++++++ tests/idris2/total/total026/expected | 1 + tests/idris2/total/total026/run | 3 +++ 6 files changed, 44 insertions(+) create mode 100644 tests/idris2/total/total025/Issue-2995.idr create mode 100644 tests/idris2/total/total025/expected create mode 100755 tests/idris2/total/total025/run create mode 100644 tests/idris2/total/total026/Issue-2995.idr create mode 100644 tests/idris2/total/total026/expected create mode 100755 tests/idris2/total/total026/run diff --git a/tests/idris2/total/total025/Issue-2995.idr b/tests/idris2/total/total025/Issue-2995.idr new file mode 100644 index 0000000000..e089a384b4 --- /dev/null +++ b/tests/idris2/total/total025/Issue-2995.idr @@ -0,0 +1,18 @@ +-- see https://github.com/idris-lang/Idris2/issues/2995 + +%default total + +-- %tcinline -- uncomment this, your compiler will hang forever +-- terminate after setting fuel +zs : Stream Nat +zs = Z :: zs + +-- %tcinline -- uncomment this, your compiler will hang forever +-- terminate after setting fuel +zs' : Stream Nat -> Stream Nat +zs' xs = Z :: zs' xs + +-- %tcinline -- uncomment this, your compiler will hang forever +-- terminate after setting fuel +zs'' : Stream Nat -> Stream Nat +zs'' = \xs => Z :: zs'' xs diff --git a/tests/idris2/total/total025/expected b/tests/idris2/total/total025/expected new file mode 100644 index 0000000000..ac470e3ab6 --- /dev/null +++ b/tests/idris2/total/total025/expected @@ -0,0 +1 @@ +1/1: Building Issue-2995 (Issue-2995.idr) diff --git a/tests/idris2/total/total025/run b/tests/idris2/total/total025/run new file mode 100755 index 0000000000..d9d5542e83 --- /dev/null +++ b/tests/idris2/total/total025/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue-2995.idr diff --git a/tests/idris2/total/total026/Issue-2995.idr b/tests/idris2/total/total026/Issue-2995.idr new file mode 100644 index 0000000000..c2888afb7c --- /dev/null +++ b/tests/idris2/total/total026/Issue-2995.idr @@ -0,0 +1,18 @@ +-- see https://github.com/idris-lang/Idris2/issues/2995 + +%default total + +%tcinline +incAll : Stream Nat -> Stream Nat +incAll (x::xs) = S x :: incAll xs + +-- %tcinline -- uncomment this, your compiler will hang forever +-- still hang after setting fuel +incAll' : Stream Nat -> Stream Nat +incAll' = \(x::xs) => S x :: incAll' xs + +-- %tcinline -- uncomment this, your compiler will hang forever +-- still hang after setting fuel +incAll'' : Stream Nat -> Stream Nat +incAll'' = \ys => case ys of + (x :: xs) => S x :: incAll'' xs diff --git a/tests/idris2/total/total026/expected b/tests/idris2/total/total026/expected new file mode 100644 index 0000000000..ac470e3ab6 --- /dev/null +++ b/tests/idris2/total/total026/expected @@ -0,0 +1 @@ +1/1: Building Issue-2995 (Issue-2995.idr) diff --git a/tests/idris2/total/total026/run b/tests/idris2/total/total026/run new file mode 100755 index 0000000000..d9d5542e83 --- /dev/null +++ b/tests/idris2/total/total026/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue-2995.idr From 3f530998bc051b7d0dcae0944b31149389b05292 Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Mon, 15 Apr 2024 18:36:21 +0300 Subject: [PATCH 2/9] add TcInlineFuel in pragmas --- src/Core/Context.idr | 11 +++++++++++ src/Core/Options.idr | 3 ++- src/Idris/Desugar.idr | 1 + src/Idris/Parser.idr | 4 ++++ src/Idris/Syntax.idr | 1 + 5 files changed, 19 insertions(+), 1 deletion(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index c12e21cd2d..739a43ff8c 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2262,6 +2262,17 @@ setNFThreshold : {auto c : Ref Ctxt Defs} -> Nat -> Core () setNFThreshold max = update Ctxt { options->elabDirectives->nfThreshold := max } +export +setTcInlineFuel : {auto c : Ref Ctxt Defs} -> + Nat -> Core () +setTcInlineFuel fuel = update Ctxt { options->elabDirectives->tcInlineFuel := fuel } + +export +getTcInlineFuel : {auto c : Ref Ctxt Defs} -> Core Nat +getTcInlineFuel = do + defs <- get Ctxt + pure (tcInlineFuel (elabDirectives (options defs))) + export setSearchTimeout : {auto c : Ref Ctxt Defs} -> Integer -> Core () diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 5391bb02b8..a5142f69a9 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -132,6 +132,7 @@ record ElabDirectives where -- in addition to postfix (dot) projections -- default: yes prefixRecordProjections : Bool + tcInlineFuel : Nat public export record Session where @@ -230,7 +231,7 @@ defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False export defaultElab : ElabDirectives -defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True +defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True 1000 -- FIXME: This turns out not to be reliably portable, since different systems -- may have tools with the same name but different required arugments. We diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index e26787ea4b..774860bed2 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -1331,6 +1331,7 @@ mutual Overloadable n => pure [IPragma fc [] (\nest, env => setNameFlag fc n Overloadable)] Extension e => pure [IPragma fc [] (\nest, env => setExtension e)] DefaultTotality tot => pure [IPragma fc [] (\_, _ => setDefaultTotalityOption tot)] + TcInlineFuel n => pure [IPragma fc [] (\nest, env => setTcInlineFuel n)] desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name] export diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 4d07f893c9..d5f5021fc3 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1534,6 +1534,10 @@ directive fname indents tot <- totalityOpt fname atEnd indents pure (DefaultTotality tot) + <|> do decoratedPragma fname "tcinline_fuel" + fuel <- decorate fname Keyword $ intLit + atEnd indents + pure (TcInlineFuel (fromInteger fuel)) fix : Rule Fixity fix diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index b09b3e5fd3..dbbe9f6370 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -376,6 +376,7 @@ mutual AutoImplicitDepth : Nat -> Directive NFMetavarThreshold : Nat -> Directive SearchTimeout : Integer -> Directive + TcInlineFuel : Nat -> Directive public export PField : Type From 87d0ddeaf0735007d24a69502ece8b743212f65b Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Mon, 15 Apr 2024 19:17:28 +0300 Subject: [PATCH 3/9] use tcinline_fuel pragma in CallGraph --- src/Core/Termination/CallGraph.idr | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr index 1acf42a08f..2e8684c949 100644 --- a/src/Core/Termination/CallGraph.idr +++ b/src/Core/Termination/CallGraph.idr @@ -343,7 +343,8 @@ findCalls : {auto c : Ref Ctxt Defs} -> Core (List SCCall) findCalls defs (_ ** (env, lhs, rhs_in)) = do let pargs = getArgs (delazy defs lhs) - rhs <- normaliseOpts tcOnly defs env rhs_in + fuel <- getTcInlineFuel + rhs <- normaliseOpts ({fuel := Just fuel} tcOnly) defs env rhs_in findSC defs env Toplevel pargs (delazy defs rhs) getSC : {auto c : Ref Ctxt Defs} -> From 9f07dc841358b5424746392bafb6a9a642aa2caf Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Tue, 9 Apr 2024 19:52:49 +0300 Subject: [PATCH 4/9] fix caseblock looping bug --- src/Core/Termination/CallGraph.idr | 55 ++++++++++++++++-------------- 1 file changed, 29 insertions(+), 26 deletions(-) diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr index 2e8684c949..185292996d 100644 --- a/src/Core/Termination/CallGraph.idr +++ b/src/Core/Termination/CallGraph.idr @@ -70,23 +70,24 @@ mutual findSC : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Guardedness -> + List Name -> -- to avoid caseblock looping List (Term vars) -> -- LHS args Term vars -> -- RHS Core (List SCCall) - findSC {vars} defs env g pats (Bind fc n b sc) + findSC {vars} defs env g cbs pats (Bind fc n b sc) = pure $ !(findSCbinder b) ++ - !(findSC defs (b :: env) g (map weaken pats) sc) + !(findSC defs (b :: env) g cbs (map weaken pats) sc) where findSCbinder : Binder (Term vars) -> Core (List SCCall) - findSCbinder (Let _ c val ty) = findSC defs env g pats val + findSCbinder (Let _ c val ty) = findSC defs env g cbs pats val findSCbinder b = pure [] -- only types, no need to look -- If we're Guarded and find a Delay, continue with the argument as InDelay - findSC defs env Guarded pats (TDelay _ _ _ tm) - = findSC defs env InDelay pats tm - findSC defs env g pats (TDelay _ _ _ tm) - = findSC defs env g pats tm - findSC defs env g pats tm + findSC defs env Guarded cbs pats (TDelay _ _ _ tm) + = findSC defs env InDelay cbs pats tm + findSC defs env g cbs pats (TDelay _ _ _ tm) + = findSC defs env g cbs pats tm + findSC defs env g cbs pats tm = do let (fn, args) = getFnArgs tm -- if it's a 'case' or 'if' just go straight into the arguments Nothing <- handleCase fn args @@ -97,42 +98,42 @@ mutual -- If we're InDelay and find a constructor (or a function call which is -- guaranteed to return a constructor; AllGuarded set), continue as InDelay (InDelay, Ref fc (DataCon _ _) cn, args) => - do scs <- traverse (findSC defs env InDelay pats) args + do scs <- traverse (findSC defs env InDelay cbs pats) args pure (concat scs) -- If we're InDelay otherwise, just check the arguments, the -- function call is okay (InDelay, _, args) => - do scs <- traverse (findSC defs env Unguarded pats) args + do scs <- traverse (findSC defs env Unguarded cbs pats) args pure (concat scs) (Guarded, Ref fc (DataCon _ _) cn, args) => do Just ty <- lookupTyExact cn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Guarded pats fc cn args - findSCcall defs env Guarded pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args (Toplevel, Ref fc (DataCon _ _) cn, args) => do Just ty <- lookupTyExact cn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Guarded pats fc cn args - findSCcall defs env Guarded pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args (_, Ref fc Func fn, args) => do logC "totality" 50 $ pure $ "Looking up type of " ++ show !(toFullNames fn) Just ty <- lookupTyExact fn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Unguarded pats fc fn args - findSCcall defs env Unguarded pats fc fn args + findSCcall defs env Unguarded cbs pats fc fn args + findSCcall defs env Unguarded cbs pats fc fn args (_, f, args) => - do scs <- traverse (findSC defs env Unguarded pats) args + do scs <- traverse (findSC defs env Unguarded cbs pats) args pure (concat scs) where handleCase : Term vars -> List (Term vars) -> Core (Maybe (List SCCall)) handleCase (Ref fc nt n) args = do n' <- toFullNames n if caseFn n' - then Just <$> findSCcall defs env g pats fc n args + then Just <$> findSCcall defs env g cbs pats fc n args else pure Nothing handleCase _ _ = pure Nothing @@ -303,23 +304,24 @@ mutual findSCcall : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Guardedness -> + List Name -> -- to avoid caseblock looping List (Term vars) -> FC -> Name -> List (Term vars) -> Core (List SCCall) - findSCcall defs env g pats fc fn_in args + findSCcall defs env g cbs pats fc fn_in args -- Under 'assert_total' we assume that all calls are fine, so leave -- the size change list empty = do fn <- getFullName fn_in logC "totality.termination.sizechange" 10 $ do pure $ "Looking under " ++ show !(toFullNames fn) aSmaller <- resolved (gamma defs) (NS builtinNS (UN $ Basic "assert_smaller")) cond [(fn == NS builtinNS (UN $ Basic "assert_total"), pure []) - ,(caseFn fn, - do scs1 <- traverse (findSC defs env g pats) args + ,(caseFn fn && not (elem fn cbs), + do scs1 <- traverse (findSC defs env g (fn::cbs) pats) args mps <- getCasePats defs fn pats args - scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps + scs2 <- traverse (findInCase defs g (fn::cbs)) $ fromMaybe [] mps pure (concat (scs1 ++ scs2))) ] - (do scs <- traverse (findSC defs env g pats) args + (do scs <- traverse (findSC defs env g cbs pats) args pure ([MkSCCall fn (fromListList (map (mkChange defs aSmaller pats) args)) @@ -328,15 +330,16 @@ mutual findInCase : {auto c : Ref Ctxt Defs} -> Defs -> Guardedness -> + List Name -> -- to avoid caseblock looping (vs ** (Env Term vs, List (Term vs), Term vs)) -> Core (List SCCall) - findInCase defs g (_ ** (env, pats, tm)) + findInCase defs g cbs (_ ** (env, pats, tm)) = do logC "totality" 10 $ do ps <- traverse toFullNames pats pure ("Looking in case args " ++ show ps) logTermNF "totality" 10 " =" env tm rhs <- normaliseOpts tcOnly defs env tm - findSC defs env g pats (delazy defs rhs) + findSC defs env g cbs pats (delazy defs rhs) findCalls : {auto c : Ref Ctxt Defs} -> Defs -> (vars ** (Env Term vars, Term vars, Term vars)) -> @@ -345,7 +348,7 @@ findCalls defs (_ ** (env, lhs, rhs_in)) = do let pargs = getArgs (delazy defs lhs) fuel <- getTcInlineFuel rhs <- normaliseOpts ({fuel := Just fuel} tcOnly) defs env rhs_in - findSC defs env Toplevel pargs (delazy defs rhs) + findSC defs env Toplevel [] pargs (delazy defs rhs) getSC : {auto c : Ref Ctxt Defs} -> Defs -> Def -> Core (List SCCall) From ecb9f99a7d82d57a86310534a83ede87cf06e0f3 Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Mon, 15 Apr 2024 15:07:56 +0300 Subject: [PATCH 5/9] uncomment %tcinline --- tests/idris2/total/total025/Issue-2995.idr | 9 +++------ tests/idris2/total/total026/Issue-2995.idr | 6 ++---- 2 files changed, 5 insertions(+), 10 deletions(-) diff --git a/tests/idris2/total/total025/Issue-2995.idr b/tests/idris2/total/total025/Issue-2995.idr index e089a384b4..330cc0c41c 100644 --- a/tests/idris2/total/total025/Issue-2995.idr +++ b/tests/idris2/total/total025/Issue-2995.idr @@ -2,17 +2,14 @@ %default total --- %tcinline -- uncomment this, your compiler will hang forever --- terminate after setting fuel +%tcinline zs : Stream Nat zs = Z :: zs --- %tcinline -- uncomment this, your compiler will hang forever --- terminate after setting fuel +%tcinline zs' : Stream Nat -> Stream Nat zs' xs = Z :: zs' xs --- %tcinline -- uncomment this, your compiler will hang forever --- terminate after setting fuel +%tcinline zs'' : Stream Nat -> Stream Nat zs'' = \xs => Z :: zs'' xs diff --git a/tests/idris2/total/total026/Issue-2995.idr b/tests/idris2/total/total026/Issue-2995.idr index c2888afb7c..772bced9e4 100644 --- a/tests/idris2/total/total026/Issue-2995.idr +++ b/tests/idris2/total/total026/Issue-2995.idr @@ -6,13 +6,11 @@ incAll : Stream Nat -> Stream Nat incAll (x::xs) = S x :: incAll xs --- %tcinline -- uncomment this, your compiler will hang forever --- still hang after setting fuel +%tcinline incAll' : Stream Nat -> Stream Nat incAll' = \(x::xs) => S x :: incAll' xs --- %tcinline -- uncomment this, your compiler will hang forever --- still hang after setting fuel +%tcinline incAll'' : Stream Nat -> Stream Nat incAll'' = \ys => case ys of (x :: xs) => S x :: incAll'' xs From 16357bfba5eab9d982f346f5d921bb3fc06b0811 Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Thu, 2 May 2024 17:37:55 +0300 Subject: [PATCH 6/9] add tests TcInlineFuel --- tests/idris2/total/total027/TcInlineFuel.idr | 18 ++++++++++++++++++ tests/idris2/total/total027/expected | 11 +++++++++++ tests/idris2/total/total027/run | 3 +++ 3 files changed, 32 insertions(+) create mode 100644 tests/idris2/total/total027/TcInlineFuel.idr create mode 100644 tests/idris2/total/total027/expected create mode 100755 tests/idris2/total/total027/run diff --git a/tests/idris2/total/total027/TcInlineFuel.idr b/tests/idris2/total/total027/TcInlineFuel.idr new file mode 100644 index 0000000000..1b152050bf --- /dev/null +++ b/tests/idris2/total/total027/TcInlineFuel.idr @@ -0,0 +1,18 @@ +%default total + +%tcinline_fuel 42 + +%tcinline +f : Nat -> a -> a +f Z x = x +f (S k) x = f k x + +-- this will typecheck +g1 : Nat -> Nat +g1 Z = Z +g1 (S k) = g1 (f 41 k) + +-- but this will not +g2 : Nat -> Nat +g2 Z = Z +g2 (S k) = g2 (f 42 k) \ No newline at end of file diff --git a/tests/idris2/total/total027/expected b/tests/idris2/total/total027/expected new file mode 100644 index 0000000000..e729b411a1 --- /dev/null +++ b/tests/idris2/total/total027/expected @@ -0,0 +1,11 @@ +1/1: Building TcInlineFuel (TcInlineFuel.idr) +Error: g2 is not total, possibly not terminating due to recursive path Main.g2 + +TcInlineFuel:16:1--16:16 + 12 | g1 Z = Z + 13 | g1 (S k) = g1 (f 41 k) + 14 | + 15 | -- but this will not + 16 | g2 : Nat -> Nat + ^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/total/total027/run b/tests/idris2/total/total027/run new file mode 100755 index 0000000000..1329f3b9d4 --- /dev/null +++ b/tests/idris2/total/total027/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check TcInlineFuel.idr From f421ffcf31b957b75cfc5674bb9ffc372232042a Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Thu, 2 May 2024 17:56:46 +0300 Subject: [PATCH 7/9] modify CHANGELOG_NEXT.md --- CHANGELOG_NEXT.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index ce5919b845..49d812f75d 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -52,6 +52,13 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun` and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`. +* Add new pragma `%tcinline_fuel` to avoid totality checker from infinitely + inlining recursive function with `%tcinline` and hang forever. The default + value of `%tcinline_fuel` is `1000`. + +* Fix a bug in `CallGraph.idr` that caused compiler to hang forever even when + `%tcinline_fuel` is set. + ### Backend changes #### RefC Backend From d9ece51f2bbe9c54a31950642a97d78b08d1c140 Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Thu, 2 May 2024 18:01:56 +0300 Subject: [PATCH 8/9] modify pragmas.rst --- docs/source/reference/pragmas.rst | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/docs/source/reference/pragmas.rst b/docs/source/reference/pragmas.rst index 0f300d2735..727f88dc66 100644 --- a/docs/source/reference/pragmas.rst +++ b/docs/source/reference/pragmas.rst @@ -151,6 +151,12 @@ the ``minimal`` directive priority over the ``compact`` directive if both are pr See the section for each codegen under :ref:`sect-execs` for available directives. +``%tcinline_fuel`` +-------------------- + +Set fuel to avoid totality checker from infinitely inlining recursive function with `%tcinline` and hang +forever. The default value is 1000. (See ``%tcinline`` pragma) + Pragmas on declarations ======================= From 68389d03be08b7bcf221897b5e0f73e97323e956 Mon Sep 17 00:00:00 2001 From: Anton Ping Date: Mon, 15 Apr 2024 15:29:08 +0300 Subject: [PATCH 9/9] modify CONTRIBUTOR.md --- CONTRIBUTORS | 1 + 1 file changed, 1 insertion(+) diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 677ff6c62c..bff49defe1 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -14,6 +14,7 @@ Andre Kuhlenschmidt André Videla Andy Lok Anthony Lodi +Anton Ping Arnaud Bailly Brian Wignall Bryn Keller