Skip to content

Commit

Permalink
* Shorten checksum (from md5 to CRC32)
Browse files Browse the repository at this point in the history 
* Put TLA+ and PlusCal checksums on the BEGIN TRANSLATION line to make
editing easier
* No longer transiently silence warnings but support disabling checksum
permanently (with syntax resembling TLA+)
* Raise dialog to migrate legacy specs to checksums
* Stuff too many changes into a single commit (screw you future Markus)

[Feature][TLC][Changlog]
  • Loading branch information
@lemmy
lemmy committed Aug 4, 2020
1 parent 7c61d1a commit f1cf514
Show file tree
Hide file tree
Showing 9 changed files with 363 additions and 285 deletions.
7 changes: 0 additions & 7 deletions tlatools/org.lamport.tlatools/src/pcal/PcalParams.java
View file
Expand Up @@ -191,17 +191,10 @@ public static TLAExpr DefaultVarInit()
***********************************************************************/
public static final String BeginXlation1 = "BEGIN" ;
public static final String BeginXlation2 = "TRANSLATION" ;
public static final String BeginXlation3 = "- the hash of the PCal code:" ;

public static final String EndXlation1 = "END" ;
public static final String EndXlation2 = "TRANSLATION" ;
public static final String EndXlation3 = "- the hash of the generated TLA code (remove "
+ "to silence divergence warnings):" ;

// Checksum marker keywords - introduced as part of https://github.com/tlaplus/tlaplus/issues/296
public static final String PCAL_CHECKSUM_KEYWORD = "PCal-";
public static final String TRANSLATED_PCAL_CHECKSUM_KEYWORD = "TLA-";

/*************************************************************************
* The string identifying the end of the automatically generated part of *
* the .cfg file and the beginning of the user-added part. *
Expand Down
11 changes: 11 additions & 0 deletions tlatools/org.lamport.tlatools/src/pcal/ValidationCallBack.java
View file
Expand Up @@ -27,12 +27,23 @@

public interface ValidationCallBack {

public enum Generate {
NOT_NOW, IGNORE, DO_IT;
}

public class Noop implements ValidationCallBack {
@Override
public boolean shouldCancel() {
return false;
}

@Override
public Generate shouldGenerate() {
return Generate.NOT_NOW;
}
}

boolean shouldCancel();

Generate shouldGenerate();
}
199 changes: 102 additions & 97 deletions tlatools/org.lamport.tlatools/src/pcal/Validator.java
View file
Expand Up @@ -5,14 +5,15 @@
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.nio.charset.StandardCharsets;
import java.security.MessageDigest;
import java.security.NoSuchAlgorithmException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import java.util.Vector;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
import java.util.zip.CRC32;

import pcal.exception.ParseAlgorithmException;
import tla2sany.modanalyzer.ParseUnit;
Expand All @@ -24,18 +25,19 @@
* blocks.
*/
public class Validator {

public enum ValidationResult {
/** No PlusCal algorithm exists in the specification */
NO_PLUSCAL_EXISTS,

/** No translation exists - BUT THERE IS PLUSCAL IN THE SPECIFICATION! */
NO_TRANSLATION_EXISTS,

/** PlusCal and a translation block exist, but there are no checksums calculated. */
NO_CHECKSUMS_EXIST,
NO_TLA_CHECKSUMS_EXIST,
NO_PCAL_CHECKSUMS_EXIST,

/** One or both Checksum in the spec do not match the checksums calculated for what was found in the spec. */
DIVERGENCE_EXISTS,
TLA_DIVERGENCE_EXISTS,
PCAL_DIVERGENCE_EXISTS,

/** A Java error was encountered while attempting to validate. */
ERROR_ENCOUNTERED,
Expand All @@ -44,23 +46,29 @@ public enum ValidationResult {
NO_DIVERGENCE;
}

static final String PCAL_CHECKSUM = "pcalchecksum";
static final String TLA_CHECKSUM = "tlachecksum";

static final String CHECKSUM_TEMPLATE_IGNORE = "(chksum(pcal) \\in STRING /\\ chksum(tla) \\in STRING)";
static final String CHECKSUM_TEMPLATE = "(chksum(pcal) = \"%s\" /\\ chksum(tla) = \"%s\")";

static final String MATCH_GROUP = "hash";
static final Pattern PCAL_CHECKSUM_PATTERN = Pattern.compile(PcalParams.PCAL_CHECKSUM_KEYWORD + "(?<" + MATCH_GROUP + ">[0-9a-f]+)");
static final Pattern TRANSLATED_PCAL_CHECKSUM_PATTERN
= Pattern.compile(PcalParams.TRANSLATED_PCAL_CHECKSUM_KEYWORD + "(?<" + MATCH_GROUP + ">[0-9a-f]+)");
static final Pattern CHECKSUM_PATTERN = Pattern
.compile("\\\\\\* BEGIN TRANSLATION\\s+\\(\\s*((?i)ch(ec)?ksum\\(p(lus)?cal\\)(?-i))\\s*(=\\s*\\\"(?<"
+ PCAL_CHECKSUM + ">[0-9A-Fa-f]*)\\\"|\\\\in\\s*"
+ "STRING)\\s*\\/\\\\\\s*((?i)ch(ec)?ksum\\(tla\\+?\\)(?-i))\\s*(=\\s*\\\"(?<" + TLA_CHECKSUM
+ ">[0-9A-Fa-f]*)\\\"|\\\\in\\s*STRING)\\s*\\)");

private static final Pattern MODULE_CLOSING_PATTERN = Pattern.compile(TLAConstants.MODULE_CLOSING_REGEX);

public static ValidationResult validate(ParseUnit parseUnit, InputStream inputStream)
public static Set<ValidationResult> validate(ParseUnit parseUnit, InputStream inputStream)
throws IOException {
final BufferedReader reader = new BufferedReader(
new InputStreamReader((inputStream instanceof BufferedInputStream) ? (BufferedInputStream) inputStream
: new BufferedInputStream(inputStream)));
return validate(parseUnit, reader);
}

public static ValidationResult validate(final ParseUnit parseUnit, final BufferedReader reader) throws IOException {
public static Set<ValidationResult> validate(final ParseUnit parseUnit, final BufferedReader reader) throws IOException {
// Instead of matching the module start and end markers, whe while loop use SANY's
// parse tree that has the location of the start and end markers.
final Location loc = parseUnit.getParseTree().getLocation();
Expand Down Expand Up @@ -98,7 +106,7 @@ public static ValidationResult validate(final ParseUnit parseUnit, final Buffere
// The appearance of "algorithm", however, might be a false
// positive of which validate will take care of (I don't have
// time to move the logic up here).
return ValidationResult.NO_PLUSCAL_EXISTS;
return setOf(ValidationResult.NO_PLUSCAL_EXISTS);
}
return validate(lines);
}
Expand All @@ -110,7 +118,7 @@ public static ValidationResult validate(final ParseUnit parseUnit, final Buffere
* @param specificationText the entire specification, line by line - for historical reasons.
* @return the result of the validation, as enumerated by the inner enum of this class.
*/
private static ValidationResult validate(final List<String> specificationText) {
private static Set<ValidationResult> validate(final List<String> specificationText) {
final Vector<String> deTabbedSpecification = trans.removeTabs(specificationText);

final IntPair searchLoc = new IntPair(0, 0);
Expand Down Expand Up @@ -181,104 +189,101 @@ private static ValidationResult validate(final List<String> specificationText) {
}
}
}
if (!foundBegin) {
return ValidationResult.NO_PLUSCAL_EXISTS;
}

final Set<ValidationResult> res = new HashSet<>();


// TLA+ translation
final int translationLine = trans.findTokenPair(deTabbedSpecification, 0,
PcalParams.BeginXlation1, PcalParams.BeginXlation2);
final String pcalMD5;
final String translatedMD5;
if (translationLine == -1) {
return ValidationResult.NO_TRANSLATION_EXISTS;
} else {
final int endTranslationLine = trans.findTokenPair(deTabbedSpecification, translationLine + 1,
PcalParams.EndXlation1, PcalParams.EndXlation2);
if (endTranslationLine == -1) {
return ValidationResult.NO_TRANSLATION_EXISTS;
}
res.add(ValidationResult.NO_TRANSLATION_EXISTS);
}

final int endTranslationLine = trans.findTokenPair(deTabbedSpecification, translationLine + 1,
PcalParams.EndXlation1, PcalParams.EndXlation2);
if (endTranslationLine == -1) {
res.add(ValidationResult.NO_TRANSLATION_EXISTS);
}
if (translationLine == -1 && endTranslationLine == -1) {
return res;
}

final String beginLine = deTabbedSpecification.get(translationLine);
Matcher m = Validator.PCAL_CHECKSUM_PATTERN.matcher(beginLine);
if (m.find()) {
pcalMD5 = m.group(MATCH_GROUP);
} else {
return ValidationResult.NO_CHECKSUMS_EXIST;
}
final String endLine = deTabbedSpecification.get(endTranslationLine);
m = Validator.TRANSLATED_PCAL_CHECKSUM_PATTERN.matcher(endLine);
if (m.find()) {
translatedMD5 = m.group(MATCH_GROUP);
// PlusCal algorithm
if (!foundBegin) {
res.add(ValidationResult.NO_PLUSCAL_EXISTS);
} else {

final Vector<String> translation = new Vector<>(specificationText.subList((translationLine + 1),
endTranslationLine));
final String calculatedMD5 = calculateMD5(translation);
if (!translatedMD5.equals(calculatedMD5)) {
return ValidationResult.DIVERGENCE_EXISTS;
}
} else {
translatedMD5 = null;
}
}

try {
ParseAlgorithm.uncomment(deTabbedSpecification, algLine, algCol);
} catch (ParseAlgorithmException e) {
PcalDebug.reportError(e);
return ValidationResult.ERROR_ENCOUNTERED;
}
// Get the PlusCal AST by parsing it.
try {
ParseAlgorithm.uncomment(deTabbedSpecification, algLine, algCol);
} catch (ParseAlgorithmException e) {
PcalDebug.reportError(e);
return setOf(ValidationResult.ERROR_ENCOUNTERED);
}

final TLAtoPCalMapping mapping = new TLAtoPCalMapping() ;
mapping.algColumn = algCol;
mapping.algLine = algLine;
PcalParams.tlaPcalMapping = mapping;

AST ast = new AST();
try {
final PcalCharReader reader = new PcalCharReader(deTabbedSpecification, algLine, algCol,
specificationText.size(), 0);
ast = ParseAlgorithm.getAlgorithm(reader, foundFairBegin);
} catch (ParseAlgorithmException e) {
PcalDebug.reportError(e);
// The PlusCal algorithm doesn't parse because of a syntax error. This indicates
// that the algorithm has been modified since it wouldn't have been possible to
// calculate a checksum earlier. ast will be empty string and, thus, not match below.
}

// Calculate the checksum value for the PlusCal's AST and compare unless no
// checksum to compare it with is given (or it has been disabled).
final Matcher m = Validator.CHECKSUM_PATTERN.matcher(deTabbedSpecification.get(translationLine));
if (m.find()) {
if (m.group(Validator.PCAL_CHECKSUM) != null) {

// This seems like crazy poor design - we're already passing around algLine and algCol, but if we don't make
// this arbitrary object, throw it into a global public static setting, and also assign values to it there,
// then the ParseAlgorithm won't pick up the values..
final TLAtoPCalMapping mapping = new TLAtoPCalMapping() ;
mapping.algColumn = algCol;
mapping.algLine = algLine;
PcalParams.tlaPcalMapping = mapping;

final PcalCharReader reader = new PcalCharReader(deTabbedSpecification, algLine, algCol,
specificationText.size(), 0);
final AST ast;
try {
ast = ParseAlgorithm.getAlgorithm(reader, foundFairBegin);
} catch (ParseAlgorithmException e) {
PcalDebug.reportError(e);
return ValidationResult.ERROR_ENCOUNTERED;
final String chksumPCalAST = Validator.checksum(ast.toString());
if (!m.group(Validator.PCAL_CHECKSUM).equals(chksumPCalAST)) {
// Mismatch between the PlusCal algorithm and its checksum.
res.add(ValidationResult.PCAL_DIVERGENCE_EXISTS);
}
}
if (m.group(Validator.TLA_CHECKSUM) != null) {
final Vector<String> translation = new Vector<>(
specificationText.subList((translationLine + 1), endTranslationLine));
final String chksumTLATranslation = Validator.checksum(translation);

if (!m.group(Validator.TLA_CHECKSUM).equals(chksumTLATranslation)) {
// Mismatch between the TLA+ translation and its checksum.
res.add(ValidationResult.TLA_DIVERGENCE_EXISTS);
}
}
} else {
res.add(ValidationResult.NO_PCAL_CHECKSUMS_EXIST);
}
}

final String calculatedMD5 = Validator.calculateMD5(ast.toString());
if (!pcalMD5.equals(calculatedMD5)) {
return ValidationResult.DIVERGENCE_EXISTS;
}

return ValidationResult.NO_DIVERGENCE;
return res.isEmpty() ? setOf(ValidationResult.NO_DIVERGENCE) : res;
}

public static String calculateMD5(final Vector<String> lines) {
public static String checksum(final Vector<String> lines) {
final StringBuilder sb = new StringBuilder();
for (final String str : lines) {
sb.append(str);
}

return calculateMD5(sb.toString());
return checksum(sb.toString());
}

static String calculateMD5(final String string) {
try {
final MessageDigest digest = MessageDigest.getInstance("MD5");
final byte[] hash = digest.digest(string.getBytes(StandardCharsets.UTF_8));
final StringBuffer hexString = new StringBuffer();
for (int i = 0; i < hash.length; i++) {
final String hex = Integer.toHexString(0xff & hash[i]);
if (hex.length() == 1) {
hexString.append('0');
}
hexString.append(hex);
}
return hexString.toString();
} catch (final NoSuchAlgorithmException e) {
PcalDebug.reportError("Unable to calculate MD5: " + e.getMessage());
return null;
}
static String checksum(final String string) {
final CRC32 crc32 = new CRC32();
crc32.update(string.getBytes());
return Long.toHexString(crc32.getValue());
}

private static Set<ValidationResult> setOf(ValidationResult... res) {
return new HashSet<>(Arrays.asList(res));
}
}

1 comment on commit f1cf514

@lemmy
Copy link
Member Author

@lemmy lemmy commented on f1cf514 Aug 5, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Peek 2020-08-04 17-03

Please sign in to comment.