<commit_before>// Copyright (c) 2011, <NAME> (<EMAIL>)
// All rights reserved.
//
// This software may be modified and distributed under the terms
// of the BSD license.  See the LICENSE file for details.

package wyc.testing;

import static org.junit.Assert.fail;

import java.io.File;
import java.io.IOException;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.concurrent.TimeUnit;

import org.junit.*;
import org.junit.rules.Timeout;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameters;

import wyc.commands.Compile;
import wyc.util.TestUtils;
import wycc.util.Pair;

/**
 * Run through all valid test cases with verification enabled. Since every test
 * file is valid, a successful test occurs when the compiler succeeds and, when
 * executed, the compiled file produces the expected output. Note that an
 * internal failure does not count as a valid pass, and indicates the test
 * exposed some kind of compiler bug.
 *
 * @author <NAME>
 *
 */
@RunWith(Parameterized.class)
public class AllValidVerificationTest {
	@Rule
	public Timeout globalTimeout = new Timeout(5, TimeUnit.SECONDS);

	/**
	 * The directory containing the source files for each test case. Every test
	 * corresponds to a file in this directory.
	 */
	public final static String WHILEY_SRC_DIR = "tests/valid".replace('/', File.separatorChar);

	/**
	 * Ignored tests and a reason why we ignore them.
	 */
	public final static Map<String, String> IGNORED = new HashMap<>();

	static {
		// =================================================
		// Whiley Compiler Problems
		// =================================================
		// Bring over all the currently failing tests for the compiler. There's
		// absolutely no point trying to see whether these work or not, since we
		// already know they will not.
		IGNORED.putAll(AllValidTest.IGNORED);
		//
		IGNORED.put("ConstrainedList_Valid_28", "#666");
		//
		IGNORED.put("IfElse_Valid_4", "#712");
		IGNORED.put("Complex_Valid_4", "#712");
		IGNORED.put("ListAccess_Valid_6", "712");
		//
		IGNORED.put("Record_Valid_3", "#714");
		//
		//IGNORED.put("Ensures_Valid_3", "#730");
		//
		IGNORED.put("ConstrainedList_Valid_22", "#731");
		IGNORED.put("Assert_Valid_1", "#731");
		//
		IGNORED.put("Process_Valid_1", "#743");
		IGNORED.put("Process_Valid_9", "#743");
		IGNORED.put("Process_Valid_10", "#743");
		IGNORED.put("Process_Valid_11", "#743");
		IGNORED.put("Reference_Valid_2", "#743");
		IGNORED.put("Reference_Valid_3", "#743");
		IGNORED.put("Reference_Valid_6", "#743");
		//
		// ===============================================================
		// Whiley Theorem Prover faults
		// ===============================================================
		IGNORED.put("ConstrainedList_Valid_8", "too long for Travis");
		IGNORED.put("Complex_Valid_8", "too long for Travis");
		IGNORED.put("RecursiveType_Valid_2", "too long for Travis");
		// Issue 2 "Verification of Remainder Operator"
		IGNORED.put("ConstrainedInt_Valid_22", "WyTP#2");
		// Issue 12 "Support for Non-linear Arthmetic"
		IGNORED.put("IntMul_Valid_2", "WyTP#12");
		IGNORED.put("While_Valid_27", "WyTP#12");
		IGNORED.put("While_Valid_32", "WyTP#12");
		// Issue 29 "Triggerless Quantifier Instantiation"
		IGNORED.put("ConstrainedList_Valid_14", "WyTP#29");
		IGNORED.put("ConstrainedList_Valid_18", "WyTP#29");
		// Issue 36 "Support for Division Operator Feature"
		IGNORED.put("Cast_Valid_5", "WyTP#36");
		IGNORED.put("IntOp_Valid_1", "WyTP#36");
		IGNORED.put("IntDiv_Valid_3", "WyTP#36");
		IGNORED.put("Lambda_Valid_3", "WyTP#36");
		IGNORED.put("Lambda_Valid_4", "WyTP#36");
		// Issue 41 "Case Split within Quantifier"
		IGNORED.put("Property_Valid_4", "WyTP#41");
		IGNORED.put("Subtype_Valid_5", "WyTP#41");
		IGNORED.put("RecursiveType_Valid_19", "WyTP#41");
		// Issue 76 "Casting Record Types"
		IGNORED.put("Coercion_Valid_9", "WyTP#76");
		IGNORED.put("RecordCoercion_Valid_1", "WyTP#76");
		// Issue 80 "(Non-)Empty Type"
		IGNORED.put("OpenRecord_Valid_4", "WyTP#80");
		IGNORED.put("OpenRecord_Valid_9", "WyTP#80");
		// Issue 85 "NegativeArraySizeException in CoerciveSubtypeOperator"
		IGNORED.put("ConstrainedRecord_Valid_9", "WyTP#85");
		IGNORED.put("TypeEquals_Valid_54", "WyTP#85");
		// Issue 86 "Handle Coefficients for CongruenceClosure"
		IGNORED.put("While_Valid_25", "WyTP#86");
		IGNORED.put("While_Valid_30", "WyTP#86");
		// Issue 89 "Unknown Assertion Failure"
		IGNORED.put("While_Valid_37", "WyTP#89");
		// Issue 102 "Support Reference Lifetimes"
		IGNORED.put("Lifetime_Valid_8", "WyTP#102");
		// Issue 104 "Incompleteness in CoerciveSubtypeOperator"
		IGNORED.put("RecursiveType_Valid_7", "WyTP#104");
		IGNORED.put("While_Valid_15", "WyTP#104");
		IGNORED.put("While_Valid_20", "WyTP#104");
		// Issue 107 "Limitation with ReadableRecordExtractor"
		IGNORED.put("TypeEquals_Valid_30", "WyTP#107");
		IGNORED.put("TypeEquals_Valid_25", "WyTP#107");
		// Issue 111 "Infinite Recursive Expansion"
		IGNORED.put("RecursiveType_Valid_29", "WyTP#111");
		IGNORED.put("Function_Valid_18", "WyTP#111");
		IGNORED.put("While_Valid_22", "WyTP#111");
		// Issue 112 "More Performance Problems with Type Checking"
		IGNORED.put("Complex_Valid_2", "WyTP#112");
		IGNORED.put("BoolList_Valid_3", "WyTP#112");<commit_msg>Unignore test cases now passing<commit_after>// Copyright (c) 2011, <NAME> (<EMAIL>)
// All rights reserved.
//
// This software may be modified and distributed under the terms
// of the BSD license.  See the LICENSE file for details.

package wyc.testing;

import static org.junit.Assert.fail;

import java.io.File;
import java.io.IOException;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.concurrent.TimeUnit;

import org.junit.*;
import org.junit.rules.Timeout;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameters;

import wyc.commands.Compile;
import wyc.util.TestUtils;
import wycc.util.Pair;

/**
 * Run through all valid test cases with verification enabled. Since every test
 * file is valid, a successful test occurs when the compiler succeeds and, when
 * executed, the compiled file produces the expected output. Note that an
 * internal failure does not count as a valid pass, and indicates the test
 * exposed some kind of compiler bug.
 *
 * @author <NAME>
 *
 */
@RunWith(Parameterized.class)
public class AllValidVerificationTest {
	@Rule
	public Timeout globalTimeout = new Timeout(5, TimeUnit.SECONDS);

	/**
	 * The directory containing the source files for each test case. Every test
	 * corresponds to a file in this directory.
	 */
	public final static String WHILEY_SRC_DIR = "tests/valid".replace('/', File.separatorChar);

	/**
	 * Ignored tests and a reason why we ignore them.
	 */
	public final static Map<String, String> IGNORED = new HashMap<>();

	static {
		// =================================================
		// Whiley Compiler Problems
		// =================================================
		// Bring over all the currently failing tests for the compiler. There's
		// absolutely no point trying to see whether these work or not, since we
		// already know they will not.
		IGNORED.putAll(AllValidTest.IGNORED);
		//
		IGNORED.put("ConstrainedList_Valid_28", "#666");
		//
		IGNORED.put("IfElse_Valid_4", "#712");
		IGNORED.put("Complex_Valid_4", "#712");
		IGNORED.put("ListAccess_Valid_6", "712");
		//
		IGNORED.put("Record_Valid_3", "#714");
		//
		//IGNORED.put("Ensures_Valid_3", "#730");
		//
		IGNORED.put("ConstrainedList_Valid_22", "#731");
		IGNORED.put("Assert_Valid_1", "#731");
		//
		IGNORED.put("Process_Valid_1", "#743");
		IGNORED.put("Process_Valid_9", "#743");
		IGNORED.put("Process_Valid_10", "#743");
		IGNORED.put("Process_Valid_11", "#743");
		IGNORED.put("Reference_Valid_2", "#743");
		IGNORED.put("Reference_Valid_3", "#743");
		IGNORED.put("Reference_Valid_6", "#743");
		//
		// ===============================================================
		// Whiley Theorem Prover faults
		// ===============================================================
		IGNORED.put("ConstrainedList_Valid_8", "too long for Travis");
		IGNORED.put("Complex_Valid_8", "too long for Travis");
		IGNORED.put("RecursiveType_Valid_2", "too long for Travis");
		// Issue 2 "Verification of Remainder Operator"
		IGNORED.put("ConstrainedInt_Valid_22", "WyTP#2");
		// Issue 12 "Support for Non-linear Arthmetic"
		IGNORED.put("IntMul_Valid_2", "WyTP#12");
		IGNORED.put("While_Valid_27", "WyTP#12");
		IGNORED.put("While_Valid_32", "WyTP#12");
		// Issue 29 "Triggerless Quantifier Instantiation"
		IGNORED.put("ConstrainedList_Valid_14", "WyTP#29");
		IGNORED.put("ConstrainedList_Valid_18", "WyTP#29");
		// Issue 36 "Support for Division Operator Feature"
		IGNORED.put("Cast_Valid_5", "WyTP#36");
		IGNORED.put("IntOp_Valid_1", "WyTP#36");
		IGNORED.put("IntDiv_Valid_3", "WyTP#36");
		IGNORED.put("Lambda_Valid_3", "WyTP#36");
		IGNORED.put("Lambda_Valid_4", "WyTP#36");
		// Issue 41 "Case Split within Quantifier"
		IGNORED.put("Property_Valid_4", "WyTP#41");
		IGNORED.put("Subtype_Valid_5", "WyTP#41");
		IGNORED.put("RecursiveType_Valid_19", "WyTP#41");
		// Issue 76 "Casting Record Types"
		IGNORED.put("Coercion_Valid_9", "WyTP#76");
		IGNORED.put("RecordCoercion_Valid_1", "WyTP#76");
		// Issue 80 "(Non-)Empty Type"
		IGNORED.put("OpenRecord_Valid_4", "WyTP#80");
		IGNORED.put("OpenRecord_Valid_9", "WyTP#80");
		// Issue 85 "NegativeArraySizeException in CoerciveSubtypeOperator"
		IGNORED.put("ConstrainedRecord_Valid_9", "WyTP#85");
		IGNORED.put("TypeEquals_Valid_54", "WyTP#85");
		// Issue 86 "Handle Coefficients for CongruenceClosure"
		IGNORED.put("While_Valid_25", "WyTP#86");
		IGNORED.put("While_Valid_30", "WyTP#86");
		// Issue 89 "Unknown Assertion Failure"
		IGNORED.put("While_Valid_37", "WyTP#89");
		// Issue 102 "Support Reference Lifetimes"
		IGNORED.put("Lifetime_Valid_8", "WyTP#102");
		// Issue 104 "Incompleteness in CoerciveSubtypeOperator"
		IGNORED.put("RecursiveType_Valid_7", "WyTP#104");
		IGNORED.put("While_Valid_15", "WyTP#104");
		IGNORED.put("While_Valid_20", "WyTP#104");
		// Issue 107 "Limitation with ReadableRecordExtractor"
		IGNORED.put("TypeEquals_Valid_30", "WyTP#107");
		IGNORED.put("TypeEquals_Valid_25", "WyTP#107");
		// Issue 111 "Infinite Recursive Expansion"
		IGNORED.put("RecursiveType_Valid_29", "WyTP#111");
		// Issue 112 "More Performance Problems with Type Checking"
		IGNORED.put("Complex_Valid_2", "WyTP#112");
		IGNORED.put("BoolList_Valid_3", "WyTP#112");
{'fraction_non_alphanumeric': 0.18587639501078496, 'fraction_numerical': 0.04313982931632749, 'mean_word_length': 5.203606748109366, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4551687', 'n_tokens_mistral': 4176, 'n_tokens_neox': 3693, 'n_words': 813}