test/lit/passes/constraint-analysis-propagation.wast

;; NOTE: Assertions have been generated by update_lit_checks.py and should not be edited.

;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s

(module
 ;; CHECK:      (func $no-immediate-propagation (type $0) (param $0 i32) (param $1 i32)
 ;; CHECK-NEXT:  (local $2 i32)
 ;; CHECK-NEXT:  (block $label
 ;; CHECK-NEXT:   (local.set $1
 ;; CHECK-NEXT:    (local.get $0)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (br_if $label
 ;; CHECK-NEXT:    (i32.eqz
 ;; CHECK-NEXT:     (local.get $1)
 ;; CHECK-NEXT:    )
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (br_if $label
 ;; CHECK-NEXT:    (local.get $0)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (local.set $2
 ;; CHECK-NEXT:    (local.get $1)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (block
 ;; CHECK-NEXT:    (local.set $0
 ;; CHECK-NEXT:     (local.get $2)
 ;; CHECK-NEXT:    )
 ;; CHECK-NEXT:    (unreachable)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:  )
 ;; CHECK-NEXT: )
 (func $no-immediate-propagation (param $0 i32) (param $1 i32)
  (local $2 i32)
  (local.set $1
   (local.get $0)
  )
  ;; Here we have $1 == $0

  (br_if 0
   (i32.eqz
    (local.get $1)
   )
  )
  ;; Here we also have $1 == 0

  (br_if 0
   (local.get $0)
  )
  ;; Here we also have $0 != 0, which leads to a contradiction with the
  ;; above ($0 and $1 are equal, and their value cannot be both == 0 and != 0).
  ;; However, we do not detect the contradiction, since we do not fully
  ;; process all existing constraints immediately, each time we add a new one.
  ;; TODO: should we, if it's fast enough?
  ;; As a result, we do not remove the following code as unreachable.

  (local.set $2
   (local.get $1)
  )
  ;; Now $2 == 1, and since $1 == 0, we apply $2 == 0, $2 == $1, $2 == $0.

  ;; Finally, we set $0 == $2. Applying the constraints here leads us to
  ;; actually notice the contradiction. We should not error, and the code
  ;; after us is unreachable, so we emit an unreachable right after.
  (local.set $0
   (local.get $2)
  )
 )

 ;; CHECK:      (func $$no-immediate-propagation-branch (type $1) (param $0 i32)
 ;; CHECK-NEXT:  (local $1 i32)
 ;; CHECK-NEXT:  (local $2 i32)
 ;; CHECK-NEXT:  (block $label
 ;; CHECK-NEXT:   (local.set $1
 ;; CHECK-NEXT:    (local.get $0)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (br_if $label
 ;; CHECK-NEXT:    (local.get $0)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (br_if $label
 ;; CHECK-NEXT:    (i32.eqz
 ;; CHECK-NEXT:     (local.get $1)
 ;; CHECK-NEXT:    )
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (local.set $2
 ;; CHECK-NEXT:    (local.get $1)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (br_if $label
 ;; CHECK-NEXT:    (local.get $0)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:   (block
 ;; CHECK-NEXT:    (local.set $0
 ;; CHECK-NEXT:     (local.get $2)
 ;; CHECK-NEXT:    )
 ;; CHECK-NEXT:    (unreachable)
 ;; CHECK-NEXT:   )
 ;; CHECK-NEXT:  )
 ;; CHECK-NEXT: )
 (func $$no-immediate-propagation-branch (param $0 i32) (local $1 i32) (local $2 i32)
  ;; Similar to above, but now the contradiction is noticed during a branch.

  (local.set $1 (local.get $0))        ;; $1 == $0

  (br_if 0 (local.get $0))             ;; after this, $0 != 0

  (br_if 0 (i32.eqz (local.get $1)))   ;; after this, $1 == 0, which is a
                                       ;; contradiction we don't notice yet, as
                                       ;; in the prior testcase

  (local.set $2 (local.get $1))        ;; $2 == $1

  (br_if 0 (local.get $0))             ;; this once again applies $0 != 0, and
                                       ;; now we notice the contradiction

  (local.set $0 (local.get $2))        ;; we add an unreachable after this
 )
)