// 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 {}

///////////
// 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 from %0 : $Builtin.NativeObject, $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 from %0 : $Builtin.NativeObject, $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 from %0 : $Builtin.NativeObject, $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 from %0 : $Builtin.NativeObject, $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: BaseValue:    %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: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   switch_enum %0 : $Optional<Builtin.NativeObject>, case #Optional.some!enumelt.1: bb1, case #Optional.none!enumelt: bb2
// CHECK: Argument:   %2 = argument of bb1 : $Builtin.NativeObject
// CHECK: Expected convention: guaranteed.
// CHECK: Actual convention:   owned
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: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   switch_enum %0 : $Optional<Builtin.NativeObject>, case #Optional.some!enumelt.1: bb1, case #Optional.none!enumelt: bb2
// CHECK: Argument:   %2 = argument of bb1 : $Builtin.NativeObject
// CHECK: Expected convention: owned.
// CHECK: Actual convention: guaranteed
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_argument %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 from %0 : $Optional<Builtin.NativeObject>, $Optional<Builtin.NativeObject>
// CHECK: Non Consuming User:   end_borrow_argument %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 from %0 : $Optional<Builtin.NativeObject>, $Optional<Builtin.NativeObject>
  end_borrow_argument %2 : $Builtin.NativeObject
  br bb3

bb2:
  end_borrow %1 from %0 : $Optional<Builtin.NativeObject>, $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: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %2 = argument of bb1 : $SuperKlass
// CHECK: Expected convention: guaranteed.
// CHECK: Actual convention:   owned

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_guaranteed_to_owned_1'
// CHECK: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %5 = argument of bb2 : $Builtin.NativeObject
// CHECK: Expected convention: guaranteed.
// CHECK: Actual convention:   owned
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: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %5 = argument of bb2 : $Builtin.NativeObject
// CHECK: Expected convention: guaranteed.
// CHECK: Actual convention:   owned
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_argument %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: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %2 = argument of bb1 : $SuperKlass
// CHECK: Expected convention: guaranteed.
// CHECK: Actual convention:   owned
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_argument %2 : $Builtin.NativeObject
  br bb3

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

// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_owned_to_guaranteed_1'
// CHECK: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %2 = argument of bb1 : $SuperKlass
// CHECK: Expected convention: owned.
// CHECK: Actual convention:   guaranteed
// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_owned_to_guaranteed_1'
// CHECK: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %5 = argument of bb2 : $Builtin.NativeObject
// CHECK: Expected convention: owned.
// CHECK: Actual convention:   guaranteed
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_argument %1 : $SuperKlass
  br bb3

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

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


// CHECK-LABEL: Function: 'checked_cast_br_mismatching_argument_owned_to_guaranteed_2'
// CHECK: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %2 = argument of bb1 : $SuperKlass
// CHECK: Expected convention: owned.
// CHECK: Actual convention:   guaranteed
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_argument %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: Error! Argument ownership kind does not match terminator!
// CHECK: Terminator:   checked_cast_br %0 : $Builtin.NativeObject to $SuperKlass, bb1, bb2
// CHECK: Argument:   %5 = argument of bb2 : $Builtin.NativeObject
// CHECK: Expected convention: owned.
// CHECK: Actual convention:   guaranteed
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_argument %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 from %0 : $Builtin.NativeObject, $Builtin.NativeObject
// CHECK: Non Consuming User:   end_borrow_argument %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_argument %2 : $SuperKlass
  end_borrow %1 from %0 : $Builtin.NativeObject, $Builtin.NativeObject
  br bb3

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

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