// RUN: %target-sil-opt -enable-sil-ownership -sil-ownership-verifier-enable-testing -enable-sil-verify-all=0 -o /dev/null 2>&1  %s | %FileCheck %s
// REQUIRES: asserts

sil_stage canonical

import Builtin

//////////////////
// Declarations //
//////////////////

sil @guaranteed_user : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()

class RefWithInt {
  var value: Builtin.Int32

  init()
}

enum Optional<T> {
case some(T)
case none
}

class SuperKlass {
  func doSomething()
}

class Klass : SuperKlass {
}

///////////
// Tests //
///////////

// This checks if the dataflow verifier asserts when we have two consuming users
// in the same block.
// CHECK-LABEL: Function: 'double_consume_same_bb'
// CHECK: Found over consume?!
// CHECK: Value:   %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   destroy_value %0 : $Builtin.NativeObject
// CHECK: Block: bb0
sil @double_consume_same_bb : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  destroy_value %0 : $Builtin.NativeObject
  destroy_value %0 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}

// This test checks if the dataflow verifier asserts when there are two
// consuming users in chained blocks.
// CHECK-LABEL: Function: 'double_consume_jump_thread_blocks'
// CHECK: Found over consume?!
// CHECK: Value:   %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   destroy_value %0 : $Builtin.NativeObject
// CHECK: Block: bb0
sil @double_consume_jump_thread_blocks : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  destroy_value %0 : $Builtin.NativeObject
  br bb1

bb1:
  destroy_value %0 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}


// We have a double consume, since we need to copy %0 before we store it.
// CHECK-LABEL: Function: 'double_consume_loop_test'
// CHECK: Found over consume?!
// CHECK: Value:   %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: Block: bb0
sil @double_consume_loop_test : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  %1 = alloc_stack $Builtin.NativeObject
  store %0 to [init] %1 : $*Builtin.NativeObject
  destroy_addr %1 : $*Builtin.NativeObject
  dealloc_stack %1 : $*Builtin.NativeObject
  br bb1

bb1:
  cond_br undef, bb2, bb5

bb2:
  cond_br undef, bb3, bb4

bb3:
  br bb1

bb4:
  br bb1

bb5:
  destroy_value %0 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}

// We have a consume of a guaranteed argument
// CHECK-LABEL: Function: 'consumed_guaranteed_arg'
// CHECK: Have operand with incompatible ownership?!
// CHECK: Value:   %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   destroy_value %0 : $Builtin.NativeObject
// CHECK: Conv: guaranteed
sil @consumed_guaranteed_arg : $@convention(thin) (@guaranteed Builtin.NativeObject) -> () {
bb0(%0 : @guaranteed $Builtin.NativeObject):
  destroy_value %0 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}

// We have a use of a borrowed value after an end_borrow. This is effectively a
// use after consume.
//
// CHECK-LABEL: Function: 'use_after_end_borrow'
// CHECK: Found use after free?!
// CHECK: Value:   %1 = begin_borrow %0 : $Builtin.NativeObject
// CHECK: Consuming User:   end_borrow %1 : $Builtin.NativeObject
// CHECK: Non Consuming User:   %4 = apply %2(%1) : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()
// CHECK: Block: bb0
sil @use_after_end_borrow : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  %1 = begin_borrow %0 : $Builtin.NativeObject
  %2 = function_ref @guaranteed_user : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()
  end_borrow %1 : $Builtin.NativeObject
  apply %2(%1) : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()
  destroy_value %0 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}

// We have a destroy value of an owned value before a borrow of the owned value
// has finished.
//
// CHECK-LABEL: Function: 'destroy_before_end_borrow'
// CHECK: Found use after free?!
// CHECK: Value:   %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: Consuming User:   destroy_value %0 : $Builtin.NativeObject
// CHECK: Non Consuming User:   end_borrow %1 : $Builtin.NativeObject
// CHECK: Block: bb0
sil @destroy_before_end_borrow : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  %1 = begin_borrow %0 : $Builtin.NativeObject
  %2 = function_ref @guaranteed_user : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()
  destroy_value %0 : $Builtin.NativeObject
  end_borrow %1 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'ref_element_addr_requires_borrow'
// CHECK: Have operand with incompatible ownership?!
// CHECK: Value:   %0 = argument of bb0 : $RefWithInt
// CHECK: User:   %1 = ref_element_addr %0 : $RefWithInt, #RefWithInt.value
// CHECK: Conv: owned
sil @ref_element_addr_requires_borrow : $@convention(thin) (@owned RefWithInt) -> () {
bb0(%0 : @owned $RefWithInt):
  %1 = ref_element_addr %0 : $RefWithInt, #RefWithInt.value
  destroy_value %0 : $RefWithInt
  %9999 = tuple()
  return %9999 : $()
}

// Make sure that we catch that in the case where unchecked_enum_data is
// propagating forward @owned ownership, that we catch a double consumed.
//
// CHECK-LABEL: Function: 'unchecked_enum_data_propagates_ownership'
// CHECK: Found over consume?!
// CHECK: Value: %0 = argument of bb0 : $Optional<Builtin.NativeObject>
// CHECK: User: destroy_value %0 : $Optional<Builtin.NativeObject>
// CHECK: Block: bb0
sil @unchecked_enum_data_propagates_ownership : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {
bb0(%0 : @owned $Optional<Builtin.NativeObject>):
  %1 = unchecked_enum_data %0 : $Optional<Builtin.NativeObject>, #Optional.some!enumelt.1
  destroy_value %0 : $Optional<Builtin.NativeObject>
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'switch_enum_mismatching_argument_guaranteed_to_owned'
// CHECK: Have operand with incompatible ownership?!
// CHECK: Value: %0 = argument of bb0
// CHECK: User:   switch_enum %0
// CHECK: Conv: guaranteed
// CHECK: OwnershipMap:
// CHECK: -- OperandOwnershipKindMap --
// CHECK: trivial:  Yes. Liveness: MustBeLive
// CHECK: unowned:  No.
// CHECK: owned: Yes. Liveness: MustBeInvalidated
// CHECK: guaranteed:  No.
// CHECK: any: Yes. Liveness: MustBeLive
sil @switch_enum_mismatching_argument_guaranteed_to_owned : $@convention(thin) (@guaranteed Optional<Builtin.NativeObject>) -> () {
bb0(%0 : @guaranteed $Optional<Builtin.NativeObject>):
  switch_enum %0 : $Optional<Builtin.NativeObject>, case #Optional.some!enumelt.1: bb1, case #Optional.none!enumelt: bb2

bb1(%1 : @owned $Builtin.NativeObject):
  destroy_value %1 : $Builtin.NativeObject
  br bb3

bb2:
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'switch_enum_mismatching_argument_owned_to_guaranteed'
// CHECK: Have operand with incompatible ownership?!
// CHECK: Value: %0 = argument of bb0 : $Optional<Builtin.NativeObject>
// CHECK: User:   switch_enum %0 : $Optional<Builtin.NativeObject>
// CHECK: Conv: owned
// CHECK: OwnershipMap:
// CHECK: -- OperandOwnershipKindMap --
// CHECK: trivial:  Yes. Liveness: MustBeLive
// CHECK: unowned:  No.
// CHECK: owned:  No.
// CHECK: guaranteed: Yes. Liveness: MustBeLive
// CHECK: any: Yes. Liveness: MustBeLive
sil @switch_enum_mismatching_argument_owned_to_guaranteed : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {
bb0(%0 : @owned $Optional<Builtin.NativeObject>):
  switch_enum %0 : $Optional<Builtin.NativeObject>, case #Optional.some!enumelt.1: bb1, case #Optional.none!enumelt: bb2

bb1(%1 : @guaranteed $Builtin.NativeObject):
  end_borrow %1 : $Builtin.NativeObject
  br bb3

bb2:
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}


// CHECK-LABEL: Function: 'switch_enum_guaranteed_arg_outlives_original_value'
// CHECK: Found use after free?!
// CHECK: Value:   %1 = begin_borrow %0 : $Optional<Builtin.NativeObject>
// CHECK: Consuming User:   end_borrow %1 : $Optional<Builtin.NativeObject>
// CHECK: Non Consuming User:   end_borrow %3 : $Builtin.NativeObject
// CHECK: Block: bb1
sil @switch_enum_guaranteed_arg_outlives_original_value : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {
bb0(%0 : @owned $Optional<Builtin.NativeObject>):
  %1 = begin_borrow %0 : $Optional<Builtin.NativeObject>
  switch_enum %1 : $Optional<Builtin.NativeObject>, case #Optional.some!enumelt.1: bb1, case #Optional.none!enumelt: bb2

bb1(%2 : @guaranteed $Builtin.NativeObject):
  end_borrow %1 : $Optional<Builtin.NativeObject>
  end_borrow %2 : $Builtin.NativeObject
  br bb3

bb2:
  end_borrow %1 : $Optional<Builtin.NativeObject>
  br bb3

bb3:
  destroy_value %0 : $Optional<Builtin.NativeObject>
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_guaranteed_to_owned_1'
// CHECK: Have operand with incompatible ownership?!
// CHECK: Value: %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Conv: guaranteed
// CHECK: OwnershipMap:
// CHECK: -- OperandOwnershipKindMap --
// CHECK: trivial:  No.
// CHECK: unowned:  No.
// CHECK: owned: Yes. Liveness: MustBeInvalidated
// CHECK: guaranteed:  No.
// CHECK: any: Yes. Liveness: MustBeLive
sil @checked_cast_br_mismatching_argument_guaranteed_to_owned_1 : $@convention(thin) (@guaranteed Builtin.NativeObject) -> () {
bb0(%0 : @guaranteed $Builtin.NativeObject):
  checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%1 : @owned $SuperKlass):
  destroy_value %1 : $SuperKlass
  br bb3

bb2(%2 : @owned $Builtin.NativeObject):
  destroy_value %2 : $Builtin.NativeObject
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_guaranteed_to_owned_2'
// CHECK: Ill-formed SIL! Unable to compute ownership kind map for user?!
// CHECK: For terminator users, check that successors have compatible ownership kinds.
// CHECK: Value: %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Conv: guaranteed
sil @checked_cast_br_mismatching_argument_guaranteed_to_owned_2 : $@convention(thin) (@guaranteed Builtin.NativeObject) -> () {
bb0(%0 : @guaranteed $Builtin.NativeObject):
  checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%1 : @guaranteed $SuperKlass):
  end_borrow %1 : $SuperKlass
  br bb3

bb2(%2 : @owned $Builtin.NativeObject):
  destroy_value %2 : $Builtin.NativeObject
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_guaranteed_to_owned_3'
// CHECK: Ill-formed SIL! Unable to compute ownership kind map for user?!
// CHECK: For terminator users, check that successors have compatible ownership kinds.
// CHECK: Value: %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Conv: guaranteed
sil @checked_cast_br_mismatching_argument_guaranteed_to_owned_3 : $@convention(thin) (@guaranteed Builtin.NativeObject) -> () {
bb0(%0 : @guaranteed $Builtin.NativeObject):
  checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%1 : @owned $SuperKlass):
  destroy_value %1 : $SuperKlass
  br bb3

bb2(%2 : @guaranteed $Builtin.NativeObject):
  end_borrow %2 : $Builtin.NativeObject
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_owned_to_guaranteed_1'
// CHECK: Have operand with incompatible ownership?!
// CHECK: Value: %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Conv: owned
// CHECK: OwnershipMap:
// CHECK: -- OperandOwnershipKindMap --
// CHECK: trivial:  No.
// CHECK: unowned:  No.
// CHECK: owned:  No.
// CHECK: guaranteed: Yes. Liveness: MustBeLive
// CHECK: any: Yes. Liveness: MustBeLive
sil @checked_cast_br_mismatching_argument_owned_to_guaranteed_1 : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%1 : @guaranteed $SuperKlass):
  end_borrow %1 : $SuperKlass
  br bb3

bb2(%2 : @guaranteed $Builtin.NativeObject):
  end_borrow %2 : $Builtin.NativeObject
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}


// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_owned_to_guaranteed_2'
// CHECK: Ill-formed SIL! Unable to compute ownership kind map for user?!
// CHECK: For terminator users, check that successors have compatible ownership kinds.
// CHECK: Value: %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Conv: owned
sil @checked_cast_br_mismatching_argument_owned_to_guaranteed_2 : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%1 : @guaranteed $SuperKlass):
  end_borrow %1 : $SuperKlass
  br bb3

bb2(%2 : @owned $Builtin.NativeObject):
  destroy_value %2 : $Builtin.NativeObject
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_owned_to_guaranteed_3'
// CHECK: Ill-formed SIL! Unable to compute ownership kind map for user?!
// CHECK: For terminator users, check that successors have compatible ownership kinds.
// CHECK: Value: %0 = argument of bb0 : $Builtin.NativeObject
// CHECK: User:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Conv: owned
sil @checked_cast_br_mismatching_argument_owned_to_guaranteed_3 : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%1 : @owned $SuperKlass):
  destroy_value %1 : $SuperKlass
  br bb3

bb2(%2 : @guaranteed $Builtin.NativeObject):
  end_borrow %2 : $Builtin.NativeObject
  br bb3

bb3:
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'checked_cast_br_guaranteed_arg_outlives_original_value'
// CHECK: Found use after free?!
// CHECK: Value:   %1 = begin_borrow %0 : $Builtin.NativeObject
// CHECK: Consuming User:   end_borrow %1 : $Builtin.NativeObject
// CHECK: Non Consuming User:   end_borrow %7 : $Builtin.NativeObject
// CHECK: Block: bb2
sil @checked_cast_br_guaranteed_arg_outlives_original_value : $@convention(thin) (@owned Builtin.NativeObject) -> () {
bb0(%0 : @owned $Builtin.NativeObject):
  %1 = begin_borrow %0 : $Builtin.NativeObject
  checked_cast_br %1 : $Builtin.NativeObject to $SuperKlass, bb1, bb2

bb1(%2 : @guaranteed $SuperKlass):
  end_borrow %2 : $SuperKlass
  end_borrow %1 : $Builtin.NativeObject
  br bb3

bb2(%3 : @guaranteed $Builtin.NativeObject):
  end_borrow %1 : $Builtin.NativeObject
  end_borrow %3 : $Builtin.NativeObject
  br bb3

bb3:
  destroy_value %0 : $Builtin.NativeObject
  %9999 = tuple()
  return %9999 : $()
}

// CHECK-LABEL: Function: 'consume_with_classmethod'
// CHECK: Found use after free?!
// CHECK: Value:   %2 = upcast %0 : $Klass to $SuperKlass
// CHECK: Consuming User:   store %2 to [init] %1 : $*SuperKlass
// CHECK: Non Consuming User:   %4 = class_method %2 : $SuperKlass, #SuperKlass.doSomething!1 : (SuperKlass) -> () -> (), $@convention(method) (@guaranteed SuperKlass) -> ()
// CHECK: Block: bb0
sil @consume_with_classmethod : $@convention(thin) (@owned Klass) -> () {
bb0(%0 : @owned $Klass):
  %1 = alloc_stack $SuperKlass
  %2 = upcast %0 : $Klass to $SuperKlass
  store %2 to [init] %1 : $*SuperKlass
  %3 = class_method %2 : $SuperKlass, #SuperKlass.doSomething!1 : (SuperKlass) -> () -> (), $@convention(method) (@guaranteed SuperKlass) -> ()
  destroy_addr %1 : $*SuperKlass
  dealloc_stack %1 : $*SuperKlass
  %9999 = tuple()
  return %9999 : $()
}