// This file is part of CPAchecker,
// a tool for configurable software verification:
// https://cpachecker.sosy-lab.org
//
// SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

package org.sosy_lab.cpachecker.cpa.bdd;

import static com.google.common.truth.Truth.assertThat;
import static com.google.common.truth.Truth.assertWithMessage;
import static com.google.common.truth.TruthJUnit.assume;

import com.google.common.collect.ImmutableList;
import java.math.BigInteger;
import java.util.Collection;
import org.junit.Before;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameters;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.cpachecker.util.predicates.bdd.BDDManagerFactory;
import org.sosy_lab.cpachecker.util.predicates.regions.Region;
import org.sosy_lab.cpachecker.util.predicates.regions.RegionManager;

@RunWith(Parameterized.class)
public class BitvectorManagerTest {

  private LogManager logger;

  private RegionManager rmgr;
  private BitvectorManager bvmgr;
  private Region[] zero;
  private Region[] one;
  private Region[] two;
  private Region[] n5;
  private Region[] n7;
  private Region[] n15;
  private Region[] n16;
  private Region[] neg1;
  private Region[] neg3;
  private Region[] neg5;
  private Region[] neg25;
  private Region[] neg35;

  private ImmutableList<Region[]> numbers;
  private ImmutableList<Region[]> numbersNotZero;

  private int bitsize;

  @Parameters
  public static Collection<Integer> bitsize() {
    return ImmutableList.of(4, 5, 6, 8, 10, 12, 16, 32);
  }

  public BitvectorManagerTest(int pBitsize) {
    bitsize = pBitsize;
  }

  @Before
  public void init() throws InvalidConfigurationException {
    Configuration config = Configuration.defaultConfiguration();
    logger = LogManager.createTestLogManager();

    rmgr = new BDDManagerFactory(config, logger).createRegionManager();
    bvmgr = new BitvectorManager(rmgr);

    zero = bvmgr.makeNumber(BigInteger.ZERO, bitsize);
    one = bvmgr.makeNumber(BigInteger.ONE, bitsize);
    two = bvmgr.makeNumber(BigInteger.valueOf(2), bitsize);
    n5 = bvmgr.makeNumber(BigInteger.valueOf(5), bitsize);
    n7 = bvmgr.makeNumber(BigInteger.valueOf(7), bitsize);
    n15 = bvmgr.makeNumber(BigInteger.valueOf(15), bitsize);
    n16 = bvmgr.makeNumber(BigInteger.valueOf(16), bitsize);
    neg1 = bvmgr.makeNumber(BigInteger.valueOf(-1), bitsize);
    neg3 = bvmgr.makeNumber(BigInteger.valueOf(-3), bitsize);
    neg5 = bvmgr.makeNumber(BigInteger.valueOf(-5), bitsize);
    neg25 = bvmgr.makeNumber(BigInteger.valueOf(-25), bitsize);
    neg35 = bvmgr.makeNumber(BigInteger.valueOf(-35), bitsize);

    numbers = ImmutableList.of(zero, one, two, n5, n7, n15, n16, neg1, neg3, neg5, neg25, neg35);
    numbersNotZero = ImmutableList.of(one, two, n5, n7, n15, neg1, neg3, neg5);
  }

  private void assertIsTrue(Region r) {
    assertThat(r.isTrue()).isTrue();
  }

  private void assertIsFalse(Region r) {
    assertThat(r.isFalse()).isTrue();
  }

  private void assertEqual(Region[] r1, Region[] r2) {
    assertThat(r1).hasLength(r2.length);
    assertWithMessage(toString(r1) + " != " + toString(r2)).that(r2).isEqualTo(r1);
  }

  private void assertDistinct(Region[] r1, Region[] r2) {
    assertThat(r1).hasLength(r2.length);
    assertThat(r1).isNotEqualTo(r2);
  }

  @Test
  public void selfTest() {
    assertDistinct(zero, one);
    assertDistinct(neg1, one);

    for (int i = 0; i < bitsize; i++) {
      assertIsFalse(zero[i]);
    }
    assertIsTrue(one[0]);
    for (int i = 1; i < bitsize; i++) {
      assertIsFalse(one[i]);
    }
  }

  @Test(expected = AssertionError.class)
  public void differentLen() {
    bvmgr.makeAdd(bvmgr.makeNumber(BigInteger.ONE, 3), bvmgr.makeNumber(BigInteger.ONE, 4));
  }

  @Test
  public void addsub() {
    assertEqual(one, bvmgr.makeAdd(zero, one));
    assertEqual(two, bvmgr.makeAdd(one, one));
    assertEqual(two, bvmgr.makeSub(neg3, neg5));
    assertEqual(neg5, bvmgr.makeSub(neg3, two));

    for (Region[] m : numbers) {
      assertEqual(m, bvmgr.makeAdd(m, zero));
      assertEqual(zero, bvmgr.makeSub(m, m));
      for (Region[] n : numbers) {
        assertEqual(m, bvmgr.makeSub(bvmgr.makeAdd(m, n), n));
        assertEqual(m, bvmgr.makeSub(bvmgr.makeAdd(n, m), n));
        assertEqual(m, bvmgr.makeAdd(bvmgr.makeSub(m, n), n));
        assertEqual(m, bvmgr.makeAdd(n, bvmgr.makeSub(m, n)));
      }
    }
  }

  @Test
  public void bool() {
    for (Region[] n : ImmutableList.of(one, two, n5, n7, n15, neg1, neg3, neg5)) {
      assertIsFalse(bvmgr.makeNot(n));
    }
    assertIsTrue(bvmgr.makeNot(zero));

    assertEqual(zero, bvmgr.makeBinaryAnd(one, two));
    assertEqual(zero, bvmgr.makeBinaryAnd(one, zero));
    assertEqual(one, bvmgr.makeBinaryAnd(one, one));
    assertEqual(one, bvmgr.makeBinaryAnd(one, bvmgr.makeAdd(one, two)));

    assertIsTrue(bvmgr.makeLogicalEqual(one, one));
    assertIsTrue(bvmgr.makeLogicalEqual(two, two));
    assertEqual(bvmgr.makeBinaryEqual(one, one), bvmgr.makeSub(zero, one));
    assertEqual(bvmgr.makeBinaryEqual(zero, zero), bvmgr.makeSub(one, two));
    assertEqual(bvmgr.makeXor(one, two), bvmgr.makeAdd(one, two));
    assertEqual(bvmgr.makeXor(one, zero), one);
  }

  /** compares operands modulo 16 */
  private void assertEqualwithLen4(Region[] a, Region[] b) {
    assertEqual(bvmgr.toBitsize(4, true, a), bvmgr.toBitsize(4, true, b));
  }

  @Test
  public void signedLen4() {
    assume().withMessage("test is designed for a minimal bitsize of 4").that(bitsize).isAtLeast(4);

    assertEqualwithLen4(zero, bvmgr.makeAdd(neg1, one));
    assertEqualwithLen4(one, bvmgr.makeAdd(neg1, two));

    assertEqualwithLen4(neg1, bvmgr.makeSub(zero, one));
    assertEqualwithLen4(neg1, bvmgr.makeSub(one, two));

    assertEqualwithLen4(neg1, n15);

    Region[] sum = one;
    for (int i = 0; i < 4; i++) {
      sum = bvmgr.makeAdd(sum, sum);
    }
    assertEqualwithLen4(zero, sum); // 0 == 16 == 1*2*2*2*2 modulo 16
  }

  @Test
  public void lessSigned() {
    for (Region[] n : numbers) {
      assertIsFalse(bvmgr.makeLess(n, n, true));
    }

    assertIsFalse(bvmgr.makeLess(one, zero, true));
    assertIsTrue(bvmgr.makeLess(zero, one, true));

    assertIsTrue(bvmgr.makeLess(neg1, zero, true));
    assertIsFalse(bvmgr.makeLess(zero, neg1, true));
  }

  @Test
  public void lessUnsigned() {
    for (Region[] n : numbers) {
      assertIsFalse(bvmgr.makeLess(n, n, false));
    }

    assertIsFalse(bvmgr.makeLess(one, zero, false));
    assertIsTrue(bvmgr.makeLess(zero, one, false));
    assertIsTrue(bvmgr.makeLess(zero, two, false));
    assertIsTrue(bvmgr.makeLess(zero, n5, false));
    assertIsTrue(bvmgr.makeLess(zero, n7, false));

    assertIsFalse(bvmgr.makeLess(neg1, zero, false));
    assertIsTrue(bvmgr.makeLess(zero, neg1, false));
  }

  @Test
  public void lessOrEqualSigned() {
    for (Region[] n : numbers) {
      assertIsTrue(bvmgr.makeLessOrEqual(n, n, true));
    }

    assertIsFalse(bvmgr.makeLessOrEqual(one, zero, true));
    assertIsTrue(bvmgr.makeLessOrEqual(zero, one, true));

    assertIsTrue(bvmgr.makeLessOrEqual(neg1, zero, true));
    assertIsFalse(bvmgr.makeLessOrEqual(zero, neg1, true));
  }

  @Test
  public void lessOrEqualUnsigned() {
    for (Region[] n : numbers) {
      assertIsTrue(bvmgr.makeLessOrEqual(n, n, false));
    }

    assertIsFalse(bvmgr.makeLessOrEqual(one, zero, false));
    assertIsTrue(bvmgr.makeLessOrEqual(zero, one, false));

    assertIsFalse(bvmgr.makeLessOrEqual(neg1, zero, false));
    assertIsTrue(bvmgr.makeLessOrEqual(zero, neg1, false));
  }

  @Test
  public void shiftLeft() {
    for (Region[] n : numbers) {
      assertEqual(n, bvmgr.makeShiftLeft(n, zero));
      assertEqual(zero, bvmgr.makeShiftLeft(zero, n));
      Region[] twice = bvmgr.makeAdd(n, n);
      assertEqual(twice, bvmgr.makeShiftLeft(n, one));
      assertEqual(bvmgr.makeAdd(twice, twice), bvmgr.makeShiftLeft(n, two));
    }

    assertEqual(n16, bvmgr.makeShiftLeft(one, bvmgr.makeAdd(two, two)));
  }

  @Test
  public void shiftRightUnsigned() {
    for (Region[] n : numbers) {
      assertEqual(n, bvmgr.makeShiftRight(n, zero, false));
      assertEqual(zero, bvmgr.makeShiftRight(zero, n, false));
    }

    assertEqual(one, bvmgr.makeShiftRight(two, one, false));
    assertEqual(one, bvmgr.makeShiftRight(n5, two, false));
    assertEqual(one, bvmgr.makeShiftRight(n7, two, false));
  }

  @Test
  public void shiftRightSigned() {
    for (Region[] n : numbers) {
      assertEqual(n, bvmgr.makeShiftRight(n, zero, true));
      assertEqual(zero, bvmgr.makeShiftRight(zero, n, true));
      Region[] minus1 = bvmgr.makeSub(zero, one);
      assertEqual(minus1, bvmgr.makeShiftRight(minus1, n, true));
    }

    assertEqual(one, bvmgr.makeShiftRight(two, one, true));
    assertEqual(one, bvmgr.makeShiftRight(n5, two, true));
    assertEqual(one, bvmgr.makeShiftRight(n7, two, true));
  }

  @Test
  public void mult() {
    for (Region[] n : numbers) {
      assertEqual(zero, bvmgr.makeMult(n, zero));
      assertEqual(zero, bvmgr.makeMult(zero, n));
      assertEqual(n, bvmgr.makeMult(n, one));
      assertEqual(n, bvmgr.makeMult(one, n));
    }

    assertEqual(n16, bvmgr.makeMult(bvmgr.makeMult(two, two), bvmgr.makeMult(two, two)));

    assertEqual(n15, bvmgr.makeMult(neg3, neg5));
    assertEqual(n15, bvmgr.makeMult(neg5, neg3));

    assertEqual(bvmgr.makeMult(neg1, neg25), bvmgr.makeMult(neg5, neg5));

    assertEqual(neg35, bvmgr.makeMult(neg5, n7));
    assertEqual(neg35, bvmgr.makeMult(n7, neg5));
  }

  @Test
  public void divSigned() {
    for (Region[] n : numbersNotZero) {
      assertEqual(zero, bvmgr.makeDiv(zero, n, true));
      assertEqual(n, bvmgr.makeDiv(n, one, true));
      assertEqual(bvmgr.makeMult(neg1, n), bvmgr.makeDiv(n, neg1, true));
    }

    assertEqual(zero, bvmgr.makeDiv(two, neg3, true));
    assertEqual(neg1, bvmgr.makeDiv(bvmgr.makeAdd(two, two), neg3, true));
    assertEqual(zero, bvmgr.makeDiv(bvmgr.makeAdd(two, two), neg5, true));
    assertEqual(two, bvmgr.makeDiv(bvmgr.makeAdd(two, two), two, true));
    if (bitsize > 6) {
      assertEqual(neg3, bvmgr.makeDiv(n15, neg5, true));
      assertEqual(neg5, bvmgr.makeDiv(n15, neg3, true));
      assertEqual(neg5, bvmgr.makeDiv(neg25, n5, true));
      assertEqual(n5, bvmgr.makeDiv(neg25, neg5, true));
      assertEqual(n7, bvmgr.makeDiv(neg35, neg5, true));
    }
  }

  @Test
  public void divUnsigned() {
    for (Region[] n : numbersNotZero) {
      assertEqual(zero, bvmgr.makeDiv(zero, n, false));
      assertEqual(n, bvmgr.makeDiv(n, one, false));
    }

    assertEqual(zero, bvmgr.makeDiv(two, neg3, false));
    assertEqual(zero, bvmgr.makeDiv(bvmgr.makeAdd(two, two), neg5, false));
    assertEqual(two, bvmgr.makeDiv(bvmgr.makeAdd(two, two), two, false));
  }

  /** check some special values that are more or less undefined by the C99 standard. */
  @Test
  public void divModSpecial() {
    assertEqual(neg1, bvmgr.makeDiv(n5, zero, false));
    assertEqual(neg1, bvmgr.makeDiv(n5, zero, true));
    assertEqual(n5, bvmgr.makeMod(n5, zero, false));
    assertEqual(n5, bvmgr.makeMod(n5, zero, true));

    assertEqual(neg1, bvmgr.makeDiv(neg5, zero, false));
    assertEqual(one, bvmgr.makeDiv(neg5, zero, true));
    assertEqual(neg5, bvmgr.makeMod(neg5, zero, false));
    assertEqual(neg5, bvmgr.makeMod(neg5, zero, true));

    final Region[] big = bvmgr.makeNumber(1 << (bitsize - 1), bitsize);

    assertEqual(neg1, bvmgr.makeDiv(big, zero, false));
    assertEqual(one, bvmgr.makeDiv(big, zero, true));
    assertEqual(big, bvmgr.makeMod(big, zero, false));
    assertEqual(big, bvmgr.makeMod(big, zero, true));

    assertEqual(zero, bvmgr.makeDiv(big, neg1, false));
    assertEqual(big, bvmgr.makeDiv(big, neg1, true));
    assertEqual(big, bvmgr.makeMod(big, neg1, false));
    assertEqual(zero, bvmgr.makeMod(big, neg1, true));
  }

  @Test
  public void modSigned() {
    for (Region[] n : numbersNotZero) {
      assertEqual(zero, bvmgr.makeMod(n, n, true));
      assertEqual(zero, bvmgr.makeMod(zero, n, true));
      assertEqual(zero, bvmgr.makeMod(n, one, true));
    }
    if (bitsize > 6) {
      assertEqual(zero, bvmgr.makeMod(neg25, n5, true));
      assertEqual(zero, bvmgr.makeMod(neg35, n5, true));
      assertEqual(zero, bvmgr.makeMod(neg25, neg5, true));
      assertEqual(zero, bvmgr.makeMod(neg35, neg5, true));
    }
  }

  @Test
  public void modUnsigned() {
    for (Region[] n : numbersNotZero) {
      assertEqual(zero, bvmgr.makeMod(n, n, false));
      assertEqual(zero, bvmgr.makeMod(zero, n, false));
      assertEqual(zero, bvmgr.makeMod(n, one, false));
    }

    assertEqual(zero, bvmgr.makeMod(bvmgr.makeAdd(two, two), two, false));
  }

  private static String toString(Region[] r) {
    StringBuilder str = new StringBuilder("[ ");
    for (int i = r.length - 1; i >= 0; i--) {
      Region bit = r[i];
      str.append(bit.isFalse() ? "0" : (bit.isTrue() ? "1" : bit));
    }
    return str.append(" ]").toString();
  }
}
