/* BSD 2-Clause License - see OPAL/LICENSE for details. */
package org.opalj
package ai
package domain
package l1

import scala.annotation.switch

import org.opalj.br.ClassType
import org.opalj.br.instructions.AALOAD
import org.opalj.br.instructions.AASTORE
import org.opalj.br.instructions.ARRAYLENGTH
import org.opalj.br.instructions.BALOAD
import org.opalj.br.instructions.BASTORE
import org.opalj.br.instructions.CALOAD
import org.opalj.br.instructions.CASTORE
import org.opalj.br.instructions.DALOAD
import org.opalj.br.instructions.DASTORE
import org.opalj.br.instructions.FALOAD
import org.opalj.br.instructions.FASTORE
import org.opalj.br.instructions.GETFIELD
import org.opalj.br.instructions.IALOAD
import org.opalj.br.instructions.IASTORE
import org.opalj.br.instructions.Instruction
import org.opalj.br.instructions.INVOKEINTERFACE
import org.opalj.br.instructions.INVOKEVIRTUAL
import org.opalj.br.instructions.LALOAD
import org.opalj.br.instructions.LASTORE
import org.opalj.br.instructions.MONITORENTER
import org.opalj.br.instructions.PUTFIELD
import org.opalj.br.instructions.SALOAD
import org.opalj.br.instructions.SASTORE
import org.opalj.br.instructions.VirtualMethodInvocationInstruction
import org.opalj.value.TypeOfReferenceValue

/**
 * Refines a reference's null property if the reference value may be null and
 * this has resulted in a corresponding exception.
 *
 * @author Michael Eichberg
 */
trait NullPropertyRefinement extends CoreDomainFunctionality {
    domain: ReferenceValuesDomain & Origin =>

    abstract override def afterEvaluation(
        pc:                       Int,
        instruction:              Instruction,
        oldOperands:              Operands,
        oldLocals:                Locals,
        targetPC:                 Int,
        isExceptionalControlFlow: Boolean,
        forceJoin:                Boolean,
        newOperands:              Operands,
        newLocals:                Locals
    ): (Operands, Locals) = {

        @inline def default() =
            super.afterEvaluation(
                pc,
                instruction,
                oldOperands,
                oldLocals,
                targetPC,
                isExceptionalControlFlow,
                forceJoin,
                newOperands,
                newLocals
            )

        def establishNullProperty(objectRef: DomainValue): (Operands, Locals) = {
            if (refIsNull(pc, objectRef).isUnknown) {
                if (isExceptionalControlFlow && {
                        // the NullPointerException was created by the JVM, because
                        // the objectRef is (assumed to be) null
                        val exception = newOperands.head
                        val TypeOfReferenceValue(utb) = exception: @unchecked
                        (utb.head eq ClassType.NullPointerException) && {
                            val origins = originsIterator(exception)
                            origins.nonEmpty && {
                                val origin = origins.next()
                                isImmediateVMException(origin) && pcOfImmediateVMException(origin) == pc &&
                                    !origins.hasNext
                            }
                        }
                    }
                ) {
                    val (operands2, locals2) =
                        refEstablishIsNull(targetPC, objectRef, newOperands, newLocals)
                    super.afterEvaluation(
                        pc,
                        instruction,
                        oldOperands,
                        oldLocals,
                        targetPC,
                        isExceptionalControlFlow,
                        forceJoin,
                        operands2,
                        locals2
                    )
                } else {
                    // ... the value is not null... even if an exception was thrown,
                    // because the exception is not a VM-level `NullPointerException`
                    val (operands2, locals2) =
                        refEstablishIsNonNull(targetPC, objectRef, newOperands, newLocals)
                    super.afterEvaluation(
                        pc,
                        instruction,
                        oldOperands,
                        oldLocals,
                        targetPC,
                        isExceptionalControlFlow,
                        forceJoin,
                        operands2,
                        locals2
                    )
                }
            } else {
                default()
            }
        }

        (instruction.opcode: @switch) match {
            case AALOAD.opcode
                | BALOAD.opcode
                | CALOAD.opcode
                | SALOAD.opcode
                | IALOAD.opcode
                | LALOAD.opcode
                | FALOAD.opcode
                | DALOAD.opcode =>
                val arrayRef = oldOperands(1)
                establishNullProperty(arrayRef)

            case AASTORE.opcode
                | BASTORE.opcode
                | CASTORE.opcode
                | SASTORE.opcode
                | IASTORE.opcode
                | LASTORE.opcode
                | FASTORE.opcode
                | DASTORE.opcode =>
                val arrayRef = oldOperands(2)
                establishNullProperty(arrayRef)

            case ARRAYLENGTH.opcode =>
                val arrayRef = oldOperands.head
                establishNullProperty(arrayRef)

            case MONITORENTER.opcode /* not necessary: | MONITOREXIT.opcode (every monitorexit is preceded by a monitorenter) */ =>
                val monitor = oldOperands.head
                establishNullProperty(monitor)

            case GETFIELD.opcode =>
                val objectRef = oldOperands.head
                establishNullProperty(objectRef)

            case PUTFIELD.opcode =>
                val objectRef = oldOperands.tail.head
                establishNullProperty(objectRef)

            // THE RECEIVER OF AN INVOKESPECIAL IS ALWAYS "THIS" AND, HENCE, IS IRRELEVANT!
            case INVOKEVIRTUAL.opcode | INVOKEINTERFACE.opcode =>
                val invoke = instruction.asInstanceOf[VirtualMethodInvocationInstruction]
                val receiver = oldOperands(invoke.methodDescriptor.parametersCount)
                establishNullProperty(receiver)

            case _ =>
                default()
        }
    }
}