Bug with ... in complicated pattern for modeless judgment

[laelath]

Demo file

I have a test case with a modeless judgement that is purely pattern matching based that is failing even though the case fits the pattern. The problem appears to be with ellipses, I tried to shrink it down to a minimal example, but I found that many attempts at simplifying the test case made the issue vanish.

[rfindler]

Maybe just a little more help: what output would you expect that you're not seeing?

[rfindler]

I tried to run it but got this:

$  git remote -v
origin  https://github.com/atgeller/Wasm-prechk.git (fetch)
origin  https://github.com/atgeller/Wasm-prechk.git (push)
$  git status
On branch bug-demo
Your branch is up to date with 'origin/bug-demo'.

nothing to commit, working tree clean
$  racket BugDemo.rkt 
open-input-file: cannot open module file
  module path: /Users/robby/git/atgeller/Wasm-prechk/WASM-Redex/Syntax.rkt
  path: /Users/robby/git/atgeller/Wasm-prechk/WASM-Redex/Syntax.rkt
  system error: no such file or directory; rkt_err=3
☕ [robby@renai] ~/git/atgeller/Wasm-prechk

[laelath]

The expected output would be that all the tests in that file pass, the error is because that repo depends on the WASM-Redex submodule.

[rfindler]

I'm sorry; after a few rounds of inlining code into a single file I've still got (at least) 5 requires to go and already 700 lines of complex code -- that depends on z3 no less. I want to try to help but someone that actually understands this code is going to have to put some more time into trying to simplify this before I can be useful. The way to approach these simplification tasks is by making a copy of the whole thing and the just slowly removing irrelevant things, focusing on one test case at a time. Remove clauses of judgment forms that aren't used in that example. That'll let you remove entire helper judgment forms which will in turn let you remove productions from the languages. When you've got something (a lot) smaller, I'd be more than happy to take a look.

[laelath]

No worries, I'll work on an example with fewer dependencies.

[laelath]

New and improved demo, this time with no external dependencies.

The tests on lines 154 and 164 for ⊢-module-func1 and ⊢-module-func2 respectively fail erroneously. ⊢-module-func{3, 4, 5} are slight mutations of the failing case that all pass, I included them hoping they're helpful in pinpointing where the bug is. ⊢-module-func4 in particular is what made me give up trying to find a minimal example of the bug.

#lang racket

(require redex/reduction-semantics)

(define-language L
  (n m t e tfi tg ti locals Γ φ ivar ::= any))

(define-judgment-form L
  #:contract (⊢ any any any)

  [---------------------
   (⊢ any_1 any_2 any_3)])

;; Base version, fails
(define-judgment-form L
  #:contract (⊢-module-func1 any any any)

  [(⊢ ((func tfi_f ...)
       (global tg ...)
       (table (n tfi_t ...) ...)
       (memory m ...)
       (local t_1 ... t ...)
       (label ((ti_2 ...) locals_1 Γ_6 φ_4))
       (return ((ti_2 ...) locals_1 Γ_6 φ_4)))
      (e ...)
      ((() ((t_1 ivar_1) ...) Γ_5 φ_5) -> ((ti_2 ...) locals_2 Γ_3 φ_3)))
   -------------------------------------------------------------------------------------------------
   (⊢-module-func1 ((func tfi_f ...) (global tg ...) (table (n tfi_t ...) ...) (memory m ...) _ _ _)
                   (() (func ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))
                             (local (t ...) (e ...))))
                   (() ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))))])

;; This one also fails
(define-judgment-form L
  #:contract (⊢-module-func2 any any any)

  [(⊢ ((func tfi_f ...)
       (global tg ...)
       (table (n tfi_t ...) ...)
       (memory m ...)
       (local t_1 ... t ...)
       (label ((ti_92 ...) locals_1 Γ_6 φ_4))
       (return ((ti_92 ...) locals_1 Γ_6 φ_4)))
      (e ...)
      ((() ((t_1 ivar_1) ...) Γ_5 φ_5) -> ((ti_2 ...) locals_2 Γ_3 φ_3)))
   -------------------------------------------------------------------------------------------------
   (⊢-module-func2 ((func tfi_f ...) (global tg ...) (table (n tfi_t ...) ...) (memory m ...) _ _ _)
                   (() (func ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))
                             (local (t ...) (e ...))))
                   (() ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))))])

;; This one passes
(define-judgment-form L
  #:contract (⊢-module-func3 any any any)

  [(⊢ ((func tfi_f ...)
       (global tg ...)
       (table (n tfi_t ...) ...)
       (memory m ...)
       (local t_1 ... t ...)
       (label ((ti_92 ..._1) locals_1 Γ_6 φ_4))
       (return ((ti_92 ..._1) locals_1 Γ_6 φ_4)))
      (e ...)
      ((() ((t_1 ivar_1) ...) Γ_5 φ_5) -> ((ti_2 ...) locals_2 Γ_3 φ_3)))
   -------------------------------------------------------------------------------------------------
   (⊢-module-func3 ((func tfi_f ...) (global tg ...) (table (n tfi_t ...) ...) (memory m ...) _ _ _)
                   (() (func ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))
                             (local (t ...) (e ...))))
                   (() ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))))])

;; This one very mysteriously passes, ((memory m ...) replaced with _)
(define-judgment-form L
  #:contract (⊢-module-func4 any any any)

  [(⊢ ((func tfi_f ...)
       (global tg ...)
       (table (n tfi_t ...) ...)
       (memory m ...)
       (local t_1 ... t ...)
       (label ((ti_2 ...) locals_1 Γ_6 φ_4))
       (return ((ti_2 ...) locals_1 Γ_6 φ_4)))
      (e ...)
      ((() ((t_1 ivar_1) ...) Γ_5 φ_5) -> ((ti_2 ...) locals_2 Γ_3 φ_3)))
   -------------------------------------------------------------------------------------------------
   (⊢-module-func4 ((func tfi_f ...) (global tg ...) (table (n tfi_t ...) ...) _ _ _ _)
                   (() (func ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))
                             (local (t ...) (e ...))))
                   (() ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ...) () Γ_4 φ_4))))])

;; This one passes, best workaround, replace all (ti_2 ...) with (ti_2 ..._1)
(define-judgment-form L
  #:contract (⊢-module-func5 any any any)

  [(⊢ ((func tfi_f ...)
       (global tg ...)
       (table (n tfi_t ...) ...)
       (memory m ...)
       (local t_1 ... t ...)
       (label ((ti_2 ..._1) locals_1 Γ_6 φ_4))
       (return ((ti_2 ..._1) locals_1 Γ_6 φ_4)))
      (e ...)
      ((() ((t_1 ivar_1) ...) Γ_5 φ_5) -> ((ti_2 ..._1) locals_2 Γ_3 φ_3)))
   -------------------------------------------------------------------------------------------------
   (⊢-module-func5 ((func tfi_f ...) (global tg ...) (table (n tfi_t ...) ...) (memory m ...) _ _ _)
                   (() (func ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ..._1) () Γ_4 φ_4))
                             (local (t ...) (e ...))))
                   (() ((((t_1 ivar_1) ...) () Γ_1 φ_1) -> ((ti_2 ..._1) () Γ_4 φ_4))))])

(define ticond0 `(((i32 a) (i32 b)) () ((empty (i32 a)) (i32 b)) empty))
(define ticond1 `(() ((i32 a) (i32 b)) ((empty (i32 a)) (i32 b)) empty))
(define ticond4 `(((i32 c)) ((i32 a) (i32 b)) (((((empty (i32 a)) (i32 b)) (i32 a_2)) (i32 b_2)) (i32 c)) (((empty (= a_2 a)) (= b_2 b)) (= c (add a_2 b_2)))))
(define ticond5 `(((i32 c)) () (((empty (i32 a)) (i32 b)) (i32 c)) (empty (= c (add a b)))))
(define ticond5_1 `(((i32 c)) ((i32 a) (i32 b)) (((empty (i32 a)) (i32 b)) (i32 c)) (empty (= c (add a b)))))

(define context1
  (term ((func (,ticond0 -> ,ticond5))
         (global)
         (table)
         (memory)
         (local)
         (label)
         (return))))

(define context1-inner
  (term ((func (,ticond0 -> ,ticond5))
         (global)
         (table)
         (memory)
         (local i32 i32)
         (label ,ticond5_1)
         (return ,ticond5_1))))

(define deriv3
  (derivation `(⊢ ,context1-inner
                  ((get-local 0) (get-local 1) (i32 add))
                  (,ticond1 -> ,ticond4))
              #f
              (list)))

(test-judgment-holds ⊢ deriv3)

(define deriv4
  (derivation `(⊢-module-func1 ,context1
                              (() (func (,ticond0 -> ,ticond5)
                                        (local () ((get-local 0) (get-local 1) (i32 add)))))
                              (() (,ticond0 -> ,ticond5)))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func1 deriv4)

(define deriv5
  (derivation `(⊢-module-func2 ,context1
                              (() (func (,ticond0 -> ,ticond5)
                                        (local () ((get-local 0) (get-local 1) (i32 add)))))
                              (() (,ticond0 -> ,ticond5)))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func2 deriv5)

(define deriv6
  (derivation `(⊢-module-func3 ,context1
                              (() (func (,ticond0 -> ,ticond5)
                                        (local () ((get-local 0) (get-local 1) (i32 add)))))
                              (() (,ticond0 -> ,ticond5)))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func3 deriv6)

(define deriv7
  (derivation `(⊢-module-func4 ,context1
                              (() (func (,ticond0 -> ,ticond5)
                                        (local () ((get-local 0) (get-local 1) (i32 add)))))
                              (() (,ticond0 -> ,ticond5)))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func4 deriv7)

(define deriv8
  (derivation `(⊢-module-func5 ,context1
                              (() (func (,ticond0 -> ,ticond5)
                                        (local () ((get-local 0) (get-local 1) (i32 add)))))
                              (() (,ticond0 -> ,ticond5)))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func5 deriv8)

[rfindler]

I started from that kept throwing thing out and whittled my way down to this. There's more to do here, but zoom awaits, so I'll just checkpoint my state here for now.

#lang racket
(require redex/reduction-semantics)

(define-language L
  (n m t e tfi tg ti locals Γ φ ivar ::= any))

(define-judgment-form L
  #:contract (⊢ any any any)

  [---------------------
   (⊢ any_1 any_2 any_3)])

;; Base version, fails
(define-judgment-form L
  #:contract (⊢-module-func1 any any any)

  [(⊢ ((func tfi_f)
       (global tg ...)
       (memory m ...)
       (local t_1 ... t ...)
       (label (n_2a ...))
       (return ((ti_2 ...))))
      (e_l1)
      (((t_1 ivar_1) ...)
       ->
       ((ti_2 ...))))
   -------------------------------------------------------------------------------------------------
   (⊢-module-func1 ((func tfi_q)
                    (global tg ...)
                    (table (n tfi_t ...) ...)
                    (memory m ...))
                   (() (func (((t_1 ivar_1) ...) -> ((ti_2b ...)))
                             (local (t ...) (e_l1))))
                   (()

                    ;; replace this:
                    ((t_1 ivar_1) ...)
                    ;; with this:
                    ;_
                    ;; to see the test case pass

                    ))])

(define deriv3
  (derivation `(⊢ ((func 1234)
                   (global)
                   (memory)
                   (local i32 i32)
                   (label (3456))
                   (return (((i32 c)))))
                  ((get-local 0))
                  (((i32 a) (i32 b))
                   ->
                   (((i32 c)))))
              #f
              (list)))

(define deriv4
  (derivation `(⊢-module-func1
                ((func 4646)
                 (global)
                 (table)
                 (memory))
                (() (func (((i32 a) (i32 b))
                           ->
                           (((i32 c))))
                          (local () ((get-local 0)))))
                (() ((i32 a) (i32 b))))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func1 deriv4)

[laelath]

One of the reasons I posted the full example was because simplifying the judgment form seems to be changing what part of the judgment is causing the issue. In the full example that I posted, the mutations seem to indicate that tying the ti_2 ...s in (label ((ti_2 ...) locals_1 Γ_6 φ_4)) and (return ((ti_2 ...) locals_1 Γ_6 φ_4)) together is what is causing the match to fail, but in your whittled down case the problem has moved to the (t_1 ivar_1) ... pattern.

[rfindler]

Sometimes one gets examples that have multiple bugs, indeed.

But the first two examples provided are quite difficult to look at from the perspective of the matcher. Far far too complex, at least for me (especially when I don't have to, as it appears I don't here! :)

Robby

On Thu, Apr 8, 2021 at 6:20 PM Justin Frank @.***> wrote:

One of the reasons I posted the full example was because simplifying the judgment form seems to be changing what part of the judgment is causing the issue. In the full example that I posted, the mutations seem to indicate that tying the ti_2 ...s in (label ((ti_2 ...) locals_1 Γ_6 φ_4)) and (return ((ti_2 ...) locals_1 Γ_6 φ_4)) together is what is causing the match to fail, but in your whittled down case the problem has moved to the (t_1 ivar_1) ... pattern.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/235#issuecomment-816296045, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADBNMA2I2CEZAMJWMTP32DTHY22RANCNFSM42R2HJ5Q .

[rfindler]

Can't seem to get something smaller than this one.

#lang racket
(require redex/reduction-semantics)
(define-language L)

(define-judgment-form L
  #:contract (⊢ any)

  [--------
   (⊢ any)])

(define-judgment-form L
  #:contract (⊢-module-func1 any)

  [(⊢ ((_ ...) (_ ...) (_ ...) (_ ...) (_ ...) (_ ...)
       (any_elephant ...)
       (any_elephant ...)))
   --------------------------------------------
   (⊢-module-func1 ((_ ...) (_ ...) (_ ...) (_ ...) (_ ...) (_ ...)
                    (any_ant ...)

                    ;; replace this:
                    (any_ant ...)
                    ;; with this:
                    ;_
                    ;; to see the test case pass

                    ))])

(define deriv3
  (derivation `(⊢ (() () () () () () () ()))
              #f
              (list)))

(define deriv4
  (derivation `(⊢-module-func1
                (() () () () () () (a) (a)))
              #f
              (list deriv3)))

(test-judgment-holds ⊢-module-func1 deriv4)

[rfindler]

Let me know if the larger example isn't cleared up.

[laelath]

That fixed it, thank you!