diff --git a/fmi2/static-model/pom.xml b/fmi2/static-model/pom.xml index 9cdd9e4f..bb456cde 100644 --- a/fmi2/static-model/pom.xml +++ b/fmi2/static-model/pom.xml @@ -9,6 +9,11 @@ org.into-cps.vdmcheck.fmi2 static-model + + + ${basedir} + + .generated diff --git a/fmi2/vdmcheck/src/main/java/annotations/ast/ASTOnFailAnnotation.java b/fmi2/vdmcheck/src/main/java/annotations/ast/ASTOnFailAnnotation.java deleted file mode 100644 index 377a08e8..00000000 --- a/fmi2/vdmcheck/src/main/java/annotations/ast/ASTOnFailAnnotation.java +++ /dev/null @@ -1,38 +0,0 @@ -/****************************************************************************** - * - * Copyright (c) 2017-2022, INTO-CPS Association, - * c/o Professor Peter Gorm Larsen, Department of Engineering - * Finlandsgade 22, 8200 Aarhus N. - * - * This file is part of the INTO-CPS toolchain. - * - * MaestroCheck is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * MaestroCheck is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with MaestroCheck. If not, see . - * SPDX-License-Identifier: GPL-3.0-or-later - * - ******************************************************************************/ - -package annotations.ast; - -import com.fujitsu.vdmj.ast.annotations.ASTAnnotation; -import com.fujitsu.vdmj.ast.lex.LexIdentifierToken; - -public class ASTOnFailAnnotation extends ASTAnnotation -{ - private static final long serialVersionUID = 1L; - - public ASTOnFailAnnotation(LexIdentifierToken name) - { - super(name); - } -} diff --git a/fmi2/vdmcheck/src/main/java/annotations/in/INOnFailAnnotation.java b/fmi2/vdmcheck/src/main/java/annotations/in/INOnFailAnnotation.java deleted file mode 100644 index 7a141e76..00000000 --- a/fmi2/vdmcheck/src/main/java/annotations/in/INOnFailAnnotation.java +++ /dev/null @@ -1,99 +0,0 @@ -/****************************************************************************** - * - * Copyright (c) 2017-2022, INTO-CPS Association, - * c/o Professor Peter Gorm Larsen, Department of Engineering - * Finlandsgade 22, 8200 Aarhus N. - * - * This file is part of the INTO-CPS toolchain. - * - * MaestroCheck is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * MaestroCheck is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with MaestroCheck. If not, see . - * SPDX-License-Identifier: GPL-3.0-or-later - * - ******************************************************************************/ - -package annotations.in; - -import java.util.List; -import java.util.Vector; - -import com.fujitsu.vdmj.in.annotations.INAnnotation; -import com.fujitsu.vdmj.in.expressions.INExpression; -import com.fujitsu.vdmj.in.expressions.INExpressionList; -import com.fujitsu.vdmj.in.expressions.INIntegerLiteralExpression; -import com.fujitsu.vdmj.in.expressions.INStringLiteralExpression; -import com.fujitsu.vdmj.runtime.Context; -import com.fujitsu.vdmj.runtime.ValueException; -import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; -import com.fujitsu.vdmj.values.Value; - -import maestro.OnFailError; - -public class INOnFailAnnotation extends INAnnotation -{ - private static final long serialVersionUID = 1L; - private static List errorList = new Vector<>(); - - public INOnFailAnnotation(TCIdentifierToken name, INExpressionList args) - { - super(name, args); - } - - @Override - public void inAfter(INExpression exp, Value rv, Context ctxt) - { - try - { - if (!rv.boolValue(ctxt)) // ONLY if we fail! - { - int errno = 0; - int offset = 1; // By default, args(1) is the 1st - - if (args.get(0) instanceof INIntegerLiteralExpression) - { - INIntegerLiteralExpression num = (INIntegerLiteralExpression)args.get(0); - errno = (int)num.value.value; - offset = 2; - } - - Object[] values = new Value[args.size() - offset]; - - for (int p = offset; p < args.size(); p++) - { - values[p - offset] = args.get(p).eval(ctxt); - } - - INStringLiteralExpression fmt = (INStringLiteralExpression)args.get(offset - 1); - String format = fmt.value.value; - String location = ""; - - if (format.endsWith("$")) // Add @OnFail location to output - { - location = name.getLocation().toString(); - format = format.substring(0, format.length() - 1); - } - - errorList.add(new OnFailError(errno, String.format(format + location, values))); - } - } - catch (ValueException e) - { - // Doesn't happen - } - } - - public static void setErrorList(List errors) - { - errorList = errors; - } -} diff --git a/fmi2/vdmcheck/src/main/java/annotations/tc/TCOnFailAnnotation.java b/fmi2/vdmcheck/src/main/java/annotations/tc/TCOnFailAnnotation.java deleted file mode 100644 index 31de482a..00000000 --- a/fmi2/vdmcheck/src/main/java/annotations/tc/TCOnFailAnnotation.java +++ /dev/null @@ -1,51 +0,0 @@ -/****************************************************************************** - * - * Copyright (c) 2017-2022, INTO-CPS Association, - * c/o Professor Peter Gorm Larsen, Department of Engineering - * Finlandsgade 22, 8200 Aarhus N. - * - * This file is part of the INTO-CPS toolchain. - * - * MaestroCheck is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * MaestroCheck is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with MaestroCheck. If not, see . - * SPDX-License-Identifier: GPL-3.0-or-later - * - ******************************************************************************/ - -package annotations.tc; - -import com.fujitsu.vdmj.tc.annotations.TCAnnotation; -import com.fujitsu.vdmj.tc.expressions.TCExpression; -import com.fujitsu.vdmj.tc.expressions.TCExpressionList; -import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; -import com.fujitsu.vdmj.typechecker.Environment; -import com.fujitsu.vdmj.typechecker.NameScope; - -public class TCOnFailAnnotation extends TCAnnotation -{ - private static final long serialVersionUID = 1L; - - public TCOnFailAnnotation(TCIdentifierToken name, TCExpressionList args) - { - super(name, args); - } - - @Override - public void tcBefore(TCExpression exp, Environment env, NameScope scope) - { - for (TCExpression arg: args) - { - arg.typeCheck(env, null, scope, null); // Just checks scope - } - } -} diff --git a/fmi2/vdmcheck/src/main/java/com/fujitsu/vdmj/mapper/ClassMapper.java b/fmi2/vdmcheck/src/main/java/com/fujitsu/vdmj/mapper/ClassMapper.java new file mode 100644 index 00000000..388e7935 --- /dev/null +++ b/fmi2/vdmcheck/src/main/java/com/fujitsu/vdmj/mapper/ClassMapper.java @@ -0,0 +1,653 @@ +/******************************************************************************* + * + * Copyright (c) 2016 Fujitsu Services Ltd. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package com.fujitsu.vdmj.mapper; +/* + * This is an older version of the ClassLoader in VDMJ which permits the override load behaviour + * We need this as we dont want the interpreter to print to the console but to a list + * */ + +import com.fujitsu.vdmj.config.Properties; + +import java.io.File; +import java.io.InputStream; +import java.lang.reflect.*; +import java.net.URL; +import java.util.*; + +/** + * A class to map classes and extend trees of objects. + */ +public class ClassMapper { + /** + * The mappers that have already been loaded, indexed by resource name + */ + private final static Map mappers = new HashMap(); + + /** + * These caches hold the object references converted so far, and keep a stack of the objects that are currently being processed. + */ + private final Stack inProgress = new Stack(); + + private final Map converted = new HashMap(); + + private long loadTimeMs; + + /** + * Get an instance of a mapper, defined by the mapspec file name (resource). + */ + public static ClassMapper getInstance(String config) { + ClassMapper mapper = mappers.get(config); + + if (mapper == null) { + mapper = new ClassMapper(config); + mappers.put(config, mapper); + } + + return mapper; + } + + /** + * Initialise the progress stack and converted objects map. + */ + public ClassMapper init() { + inProgress.clear(); + converted.clear(); + + for (Method m : initializers) { + try { + m.invoke(null, (Object[]) null); + } catch (Exception e) { + throw new RuntimeException("Error in mapping initialzer", e); + } + } + + return this; // Convenient for getInstance().init().convert(obj) + } + + /** + * Fields used during the processing of the configuration file + */ + private final String configFile; + private Field SELF; + private String srcPackage = ""; + private String destPackage = ""; + private int lineNo = 0; + private int errorCount = 0; + + /** + * The private constructor, passed the resource name of the mapping file. + */ + private ClassMapper(String config) { + configFile = config; + long before = System.currentTimeMillis(); + + try { + SELF = ClassMapper.class.getDeclaredField("SELF"); + readMappings(); + verifyConstructors(); + } catch (Exception e) { + error(e.getMessage()); + } + + loadTimeMs = System.currentTimeMillis() - before; + + if (errorCount > 0) { + System.err.println("Aborting with " + errorCount + " errors"); + // System.exit(1); + } + } + + /** + * The set of class mappings for one loaded file + */ + private final Map, MapParams> mappings = new HashMap, MapParams>(); + + /** + * A list of methods to call in the init() processing + */ + private final List initializers = new Vector(); + + /** + * A class to define how to construct one destPackage class, passing srcPackage object fields to the Constructor and setter methods. + */ + private static class MapParams { + public final int lineNo; + public final Class srcClass; + public final Class destClass; + public final List ctorFields; + public final List setterFields; + public final boolean unmapped; + + public Constructor constructor; + public Method[] setters; + + public MapParams(int lineNo, Class srcClass, Class destClass, List ctorFields, List setterFields, boolean unmapped) { + this.lineNo = lineNo; + this.srcClass = srcClass; + this.destClass = destClass; + this.ctorFields = ctorFields; + this.setterFields = setterFields; + this.unmapped = unmapped; + } + + @Override + public String toString() { + return "map " + srcClass.getSimpleName() + " to " + destClass.getSimpleName() + (setterFields.isEmpty() ? "" : " set " + setterFields); + } + } + + private void error(String message) { + System.err.println(configFile + " line " + lineNo + ": " + message); + errorCount++; + } + + /** + * Read mappings file(s) from the classpath and populate the mappings table. + */ + private void readMappings() throws Exception { + Enumeration urls = this.getClass().getClassLoader().getResources(configFile); + + while (urls.hasMoreElements()) { + URL url = urls.nextElement(); + readMapping(configFile, url.openStream()); + } + + /** + * You can add extra file locations by setting the vdmj.mappingpath property. + * This allows more than one mapping file of the same name to be included within + * one jar file. + */ + String mappingPath = Properties.mapping_search_path; + + if (mappingPath != null) { + for (String classpath : mappingPath.split(File.pathSeparator)) { + String filename = classpath + "/" + configFile; // NB. Use slash here! + InputStream is = getClass().getResourceAsStream(filename); + + if (is != null) { + readMapping(filename, is); + } + } + } + } + + private void readMapping(String filename, InputStream is) throws Exception { + MappingReader reader = new MappingReader(filename, is); + + try { + boolean eof = false; + + while (!eof) { + Mapping command = reader.readCommand(); + lineNo = command.lineNo; + + switch (command.type) { + case PACKAGE: + processPackage(command); + break; + + case MAP: + processMap(command); + break; + + case UNMAPPED: + processUnmapped(command); + break; + + case INIT: + processInit(command); + break; + + case EOF: + eof = true; + break; + + case ERROR: + // try next line + errorCount++; + break; + } + } + } finally { + reader.close(); + } + } + + private void processInit(Mapping command) { + String classname = null; + String methodname = null; + + try { + int end = command.source.lastIndexOf('.'); + + if (end > 0) { + classname = command.source.substring(0, end); + methodname = command.source.substring(end + 1); + Class initClass = Class.forName(classname); + Method initMethod = initClass.getMethod(methodname, (Class[]) null); + + if (!Modifier.isStatic(initMethod.getModifiers())) { + error("Init method is not static: " + classname + "." + methodname + "()"); + } else { + initializers.add(initMethod); + } + } else { + error("Init entry malformed: " + command.source); + } + } catch (ClassNotFoundException e) { + error("No such class: " + classname); + } catch (NoSuchMethodException e) { + error("Cannot find method: " + classname + "." + methodname + "()"); + } + } + + private void processUnmapped(Mapping command) { + try { + Class toIgnore = Class.forName(command.source); + mappings.put(toIgnore, new MapParams(lineNo, toIgnore, toIgnore, null, null, true)); + } catch (ClassNotFoundException e) { + error("No such class: " + command.source); + } + } + + private void processPackage(Mapping command) { + srcPackage = command.source; + destPackage = command.destination; + } + + private void processMap(Mapping command) throws Exception { + String srcClassname = command.source; + List srcParams = command.varnames; + String destClassname = command.destination; + List destParams = command.paramnames; + List destSetters = command.setnames; + + try { + Class srcClass = Class.forName(srcPackage + "." + srcClassname); + Class destClass = Class.forName(destPackage + "." + destClassname); + + Map srcFields = new HashMap(); + + for (String fieldname : srcParams) { + srcFields.put(fieldname, findField(srcClass, fieldname)); + } + + if (Modifier.isAbstract(srcClass.getModifiers())) { + if (!Modifier.isAbstract(destClass.getModifiers())) { + error("Source " + srcClassname + " is abstract, but mapping is not"); + } + + if (!destParams.isEmpty()) { + error("Abstract class cannot have ctor parameter substitutions"); + } + } else if (Modifier.isAbstract(destClass.getModifiers())) { + error("Mapped " + destClassname + " is abstract, but source is not"); + } + + List ctorFields = new Vector(); + List setterFields = new Vector(); + + for (String field : destParams) { + if (field.equals("this")) { + ctorFields.add(SELF); + } else if (srcFields.containsKey(field)) { + ctorFields.add(srcFields.get(field)); + } else { + error("Field not identified in " + srcClassname + ": " + field); + } + } + + for (String field : destSetters) { + if (srcFields.containsKey(field)) { + setterFields.add(srcFields.get(field)); + } else { + error("Field not identified in " + srcClassname + ": " + field); + } + } + + for (String field : srcParams) { + if (!destParams.contains(field) && !destSetters.contains(field)) { + error("Field not used in constructor or setters, " + destClassname + ": " + field); + } + } + + for (String field : destParams) { + if (destSetters.contains(field)) { + error("Field used in constructor and setter, " + destClassname + ": " + field); + } + } + + mappings.put(srcClass, new MapParams(lineNo, srcClass, destClass, ctorFields, setterFields, false)); + } catch (ClassNotFoundException e) { + error("No such class: " + e.getMessage()); + } catch (NoSuchFieldException e) { + error("No such field in " + srcClassname + ": " + e.getMessage()); + } + } + + private Field findField(Class src, String field) throws NoSuchFieldException, SecurityException { + try { + return src.getDeclaredField(field); + } catch (NoSuchFieldException e) { + return src.getField(field); + } + } + + /** + * We cannot verify the constructors exist until all the mappings have been read, because we map the parameter types from the source as well. This + * method checks that all of the mapped constructors exist in the destination classes. + */ + private void verifyConstructors() { + for (Class entry : mappings.keySet()) { + MapParams mp = mappings.get(entry); + + if (mp.unmapped) { + continue; // fine, it's not mapped + } else if (Modifier.isAbstract(entry.getModifiers())) { + continue; // fine, it will never be instantiated anyway + } else { + Class[] paramTypes = new Class[mp.ctorFields.size()]; + int a = 0; + + for (Field field : mp.ctorFields) { + Class fieldType = null; + MapParams mapping = null; + + if (field == SELF) // ie. "this" + { + fieldType = mp.srcClass; + mapping = null; + } else { + fieldType = field.getType(); + mapping = mappings.get(fieldType); + } + + if (mapping == null || mapping.unmapped) { + paramTypes[a++] = fieldType; // eg. java.lang.String + } else { + paramTypes[a++] = mapping.destClass; + } + } + + try { + lineNo = mp.lineNo; // For error reporting :) + mp.constructor = mp.destClass.getConstructor(paramTypes); + } catch (NoSuchMethodException e) { + error("No such constructor: " + mp.destClass.getSimpleName() + "(" + typeString(paramTypes) + ")"); + + System.err.println("Fields available from " + entry.getSimpleName() + ":"); + + for (Field f : getAllFields(entry)) { + System.err.println(" " + f.getType().getSimpleName() + " " + f.getName()); + } + + System.err.println("Constructors available for " + mp.destClass.getSimpleName() + ":"); + + for (Constructor ctor : mp.destClass.getConstructors()) { + System.err.println(" " + mp.destClass.getSimpleName() + "(" + typeString(ctor.getParameterTypes()) + ")"); + } + + System.err.println(); + } + + mp.setters = new Method[mp.setterFields.size()]; + a = 0; + + for (Field field : mp.setterFields) { + Class fieldType = field.getType(); + MapParams mapping = mappings.get(fieldType); + Class argType = null; + + if (mapping == null || mapping.unmapped) { + argType = fieldType; // eg. java.lang.String unmapped + } else { + argType = mapping.destClass; + } + + StringBuilder name = new StringBuilder(field.getName()); + name.setCharAt(0, Character.toUpperCase(name.charAt(0))); + + try { + lineNo = mp.lineNo; // For error reporting :) + mp.setters[a++] = mp.destClass.getMethod("set" + name, argType); + } catch (NoSuchMethodException e) { + error("No such setter: " + mp.destClass.getSimpleName() + ".set" + name + "(" + argType.getSimpleName() + ")"); + } + } + } + } + } + + private String typeString(Class[] paramTypes) { + StringBuffer sb = new StringBuffer(); + String prefix = ""; + + for (Class type : paramTypes) { + sb.append(prefix + type.getSimpleName()); + prefix = ", "; + } + + return sb.toString(); + } + + private Set getAllFields(Class clazz) { + Set allFields = new HashSet(); + + for (Field f : clazz.getFields()) { + allFields.add(f); // Including inherited fields + } + + for (Field f : clazz.getDeclaredFields()) { + allFields.add(f); // Including private local fields + } + + return allFields; + } + + /** + * Private class to identify one class in the process of being converted, and a place to record objects/fields that need to be set when the + * conversion is complete. + */ + private static class Progress { + public final Object source; + public final List updates; + + public Progress(Object source) { + this.source = source; + this.updates = new Vector(); + } + + @Override + public String toString() { + return source.getClass().getSimpleName(); + } + } + + /** + * Private class to hold an object/field pair to update (see Progress class). + */ + private static class Pair { + public final Object object; + public final String fieldname; + + public Pair(Object object, String fieldname) { + this.object = object; + this.fieldname = fieldname; + } + } + + /** + * Perform a recursive mapping for a source object/tree to a destination object/tree. + */ + @SuppressWarnings("unchecked") + public T convert(Object source) throws Exception { + if (source == null) { + return null; // Can't do much else, but the type may be wrong + } + + T result = null; + + // Check whether we have converted the object already. + // We use the MappedObject id because the equals methods are + // not cleanly implemented, and identity collisions can occur. + // MappedObject IDs are unique for different objects. + + if (source instanceof MappedObject) { + MappedObject mo = (MappedObject) source; + result = (T) converted.get(mo.getMappedId()); + + if (result != null) { + return result; // Here's the one we've already converted + } + } + + try { + inProgress.push(new Progress(source)); + + Class srcClass = source.getClass(); + MapParams mp = mappings.get(srcClass); + + if (mp == null) { + throw new Exception("No mapping for " + srcClass + " in " + configFile); + } else if (mp.unmapped) { + result = (T) source; + } else { + Object[] args = new Object[mp.ctorFields.size()]; + int a = 0; + + for (Field field : mp.ctorFields) { + if (field == SELF) // ie. "this" + { + args[a++] = source; + } else { + field.setAccessible(true); + Object fieldvalue = field.get(source); + + if (isInProgress(fieldvalue) == null) { + args[a++] = convert(fieldvalue); + } else { + args[a++] = null; + } + } + } + + result = (T) mp.constructor.newInstance(args); + int s = 0; + + for (Field setter : mp.setterFields) { + setter.setAccessible(true); + Object fieldvalue = setter.get(source); + Object arg = null; + + if (isInProgress(fieldvalue) == null) { + arg = convert(fieldvalue); + } else { + arg = null; + } + + mp.setters[s++].invoke(result, arg); + } + + for (Field field : mp.ctorFields) { + if (field != SELF) { + Progress progress = isInProgress(field.get(source)); + + if (progress != null) { + progress.updates.add(new Pair(result, field.getName())); + } + } + } + + for (Field field : mp.setterFields) { + Progress progress = isInProgress(field.get(source)); + + if (progress != null) { + progress.updates.add(new Pair(result, field.getName())); + } + } + } + } catch (InvocationTargetException e) { + if (e.getCause() instanceof Exception) { + throw (Exception) e.getCause(); + } else if (e.getTargetException() instanceof Exception) { + throw (Exception) e.getTargetException(); + } else if (e.getTargetException() instanceof ExceptionInInitializerError) { + ExceptionInInitializerError err = (ExceptionInInitializerError) e.getTargetException(); + + if (err.getException() instanceof Exception) { + throw (Exception) err.getException(); + } else { + throw new Exception(err.getException()); + } + } else { + throw new Exception(e.getTargetException()); + } + } finally { + Progress progress = inProgress.pop(); + + if (!progress.updates.isEmpty()) { + for (Pair pair : progress.updates) { + Field f = pair.object.getClass().getField(pair.fieldname); + f.setAccessible(true); + f.set(pair.object, result); + } + } + + if (source instanceof MappedObject) { + MappedObject mo = (MappedObject) source; + converted.put(mo.getMappedId(), result); + } + } + + return result; + } + + /** + * Check whether an object is already in the process of being converted. + */ + private Progress isInProgress(Object source) { + for (Progress update : inProgress) { + if (source == update.source) { + return update; + } + } + + return null; + } + + public int getNodeCount() { + return converted.size(); + } + + /** + * Return the load time of the mappings file. This is zeroed after the first request, because the mapping is not re-loaded after the first usage, + * and so the cost is zero. + */ + public long getLoadTime() { + long value = loadTimeMs; + loadTimeMs = 0; + return value; + } +} \ No newline at end of file diff --git a/fmi2/vdmcheck/src/main/java/maestro/MaestroCheck.java b/fmi2/vdmcheck/src/main/java/maestro/MaestroCheck.java index 09ad74c4..abadcc02 100644 --- a/fmi2/vdmcheck/src/main/java/maestro/MaestroCheck.java +++ b/fmi2/vdmcheck/src/main/java/maestro/MaestroCheck.java @@ -24,27 +24,6 @@ package maestro; -import java.io.BufferedOutputStream; -import java.io.File; -import java.io.FileInputStream; -import java.io.FileOutputStream; -import java.io.IOException; -import java.io.InputStream; -import java.nio.file.Files; -import java.nio.file.attribute.FileAttribute; -import java.util.List; -import java.util.Map; -import java.util.Vector; - -import javax.xml.XMLConstants; -import javax.xml.transform.Source; -import javax.xml.transform.stream.StreamSource; -import javax.xml.validation.Schema; -import javax.xml.validation.SchemaFactory; -import javax.xml.validation.Validator; - -import org.xml.sax.SAXException; - import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.modules.ASTModuleList; import com.fujitsu.vdmj.config.Properties; @@ -62,220 +41,197 @@ import com.fujitsu.vdmj.typechecker.ModuleTypeChecker; import com.fujitsu.vdmj.typechecker.TypeChecker; import com.fujitsu.vdmj.values.Value; - -import annotations.in.INOnFailAnnotation; +import org.xml.sax.SAXException; import types.Type; +import vdmcheck.annotations.in.INOnFailAnnotation; import xsd2vdm.Xsd2VDM; -public class MaestroCheck -{ - /** - * Main class for testing. Maestro will use the default constructor. - */ - public static void main(String[] args) throws Exception - { - MaestroCheck checker = new MaestroCheck(); - - for (OnFailError err: checker.check(new File(args[0]))) - { - System.out.println(err.errno + " => " + err.message); - } - } - - public List check(InputStream modelDescriptionStream) throws Exception - { - File xmlfile = Files.createTempFile("fmi", ".xml", new FileAttribute[0]).toFile(); - xmlfile.deleteOnExit(); - copyStream(modelDescriptionStream, xmlfile.getParentFile(), xmlfile.getName()); - return check(xmlfile); - } - - public List check(File modelDescriptionFile) throws Exception - { - List errors = new Vector<>(); - - File fmi2 = Files.createTempDirectory("fmi2", new FileAttribute[0]).toFile(); - fmi2.deleteOnExit(); - - File schema = new File(fmi2, "schema"); - schema.mkdir(); - schema.deleteOnExit(); - - copyResources(fmi2, - "/schema/fmi2Annotation.xsd", - "/schema/fmi2AttributeGroups.xsd", - "/schema/fmi2ModelDescription.xsd", - "/schema/fmi2ScalarVariable.xsd", - "/schema/fmi2Type.xsd", - "/schema/fmi2Unit.xsd", - "/schema/fmi2VariableDependency.xsd", - "/schema/fmi2.xsd", - "/schema/fmi3Annotation.xsd", - "/schema/fmi3BuildDescription.xsd", - "/schema/fmi3TerminalsAndIcons.xsd", - "/schema/fmi3Terminal.xsd", - "/schema/xsd2vdm.properties"); - - File xsdFile = new File(schema, "fmi2.xsd"); - OnFailError validation = validate(modelDescriptionFile, xsdFile); - - if (validation != null) - { - errors.add(validation); - } - else - { - File vdmsl = new File(fmi2, "vdmsl"); - vdmsl.mkdir(); - vdmsl.deleteOnExit(); - - File vdmFile = new File(vdmsl, "model.vdmsl"); - vdmFile.deleteOnExit(); - - Xsd2VDM converter = new Xsd2VDM(); - Xsd2VDM.loadProperties(xsdFile); - Map vdmSchema = converter.createVDMSchema(xsdFile, modelDescriptionFile, false, true); - converter.createVDMValue(vdmSchema, vdmFile, modelDescriptionFile, "model"); - - if (vdmFile.exists()) // Means successful? - { - copyResources(vdmsl, - "/CoSimulation_4.3.1.vdmsl", - "/DefaultExperiment_2.2.5.vdmsl", - "/FMI2Schema.vdmsl", - "/FMIModelDescription_2.2.1.vdmsl", - "/LogCategories_2.2.4.vdmsl", - "/Misc.vdmsl", - "/ModelExchange_3.3.1.vdmsl", - "/ModelStructure_2.2.8.vdmsl", - "/ModelVariables_2.2.7.vdmsl", - "/TypeDefinitions_2.2.3.vdmsl", - "/UnitDefinitions_2.2.2.vdmsl", - "/VariableNaming_2.2.9.vdmsl", - "/VendorAnnotations_2.2.6.vdmsl", - - "/BuildConfiguration_2.3.vdmsl", - "/GraphicalRepresentation_2.3.vdmsl", - "/Terminals_2.3.vdmsl", - "/VendorAnnotations_2.3.vdmsl", - "/Validation.vdmsl", - "/XSD.vdmsl" - ); - - Properties.init(); - Settings.annotations = true; - ASTModuleList ast = new ASTModuleList(); - - for (File sl: vdmsl.listFiles()) - { - LexTokenReader ltr = new LexTokenReader(sl, Dialect.VDM_SL); - ModuleReader mreader = new ModuleReader(ltr); - ast.addAll(mreader.readModules()); - - for (VDMError err: mreader.getErrors()) - { - errors.add(new OnFailError(err.number, err.message)); - } - } - - if (!errors.isEmpty()) - { - errors.add(new OnFailError(1, "Syntax errors in VDMSL?")); - } - else - { - TCModuleList tc = ClassMapper.getInstance(TCNode.MAPPINGS).init().convert(ast); - tc.combineDefaults(); - TypeChecker tchecker = new ModuleTypeChecker(tc); - tchecker.typeCheck(); - - if (TypeChecker.getErrorCount() > 0) - { - for (VDMError err: TypeChecker.getErrors()) - { - errors.add(new OnFailError(err.number, err.message)); - } - - errors.add(new OnFailError(2, "Type errors in VDMSL?")); - } - - INModuleList in = ClassMapper.getInstance(INNode.MAPPINGS).init().convert(tc); - Interpreter interpreter = new ModuleInterpreter(in, tc); - interpreter.init(); - INOnFailAnnotation.setErrorList(errors); - Value result = interpreter.execute("isValidFMIConfiguration(model)"); - - if (!result.boolValue(null)) - { - errors.add(new OnFailError(3, "Errors found")); - } - } - } - } - - return errors; - } - - private OnFailError validate(File xml, File xsd) - { - try - { - // Note that we pass a stream to allow the validator to determine the - // encoding, rather than passing a File, which seems to use default encoding. - Source xmlFile = new StreamSource(new FileInputStream(xml)); - xmlFile.setSystemId(xml.toURI().toASCIIString()); - Source xsdFile = new StreamSource(xsd); - xsdFile.setSystemId(xsd.toURI().toASCIIString()); - SchemaFactory schemaFactory = SchemaFactory.newInstance(XMLConstants.W3C_XML_SCHEMA_NS_URI); - - Schema schema = schemaFactory.newSchema(xsdFile); - Validator validator = schema.newValidator(); - validator.validate(xmlFile); - - return null; - } - catch (SAXException e) - { - return new OnFailError(0, "XML validation: " + e); // Raw exception gives file/line/col - } - catch (Exception e) - { - return new OnFailError(0, "XML validation: " + e.getMessage()); - } - } - - private void copyResources(File target, String... resources) throws Exception - { - if (!target.exists()) - { - throw new Exception("Target of copyResources does not exist: " + target); - } - - for (String resource: resources) - { - InputStream is = MaestroCheck.class.getResourceAsStream(resource); - - if (is == null) - { - throw new Exception("Cannot load resource " + resource); - } - - copyStream(is, target, resource); - is.close(); - } - } - - private void copyStream(InputStream data, File target, String file) throws IOException - { - File targetFile = new File(target, file); - BufferedOutputStream bos = new BufferedOutputStream(new FileOutputStream(targetFile)); - - while (data.available() > 0) - { - bos.write(data.read()); - } - - bos.close(); - targetFile.deleteOnExit(); // Note! All files temporary - } +import javax.xml.XMLConstants; +import javax.xml.transform.Source; +import javax.xml.transform.stream.StreamSource; +import javax.xml.validation.Schema; +import javax.xml.validation.SchemaFactory; +import javax.xml.validation.Validator; +import java.io.*; +import java.nio.file.Files; +import java.nio.file.attribute.FileAttribute; +import java.util.List; +import java.util.Map; +import java.util.Vector; + +public class MaestroCheck { + + /** + * Main class for testing. Maestro will use the default constructor. + */ + public static void main(String[] args) throws Exception { + MaestroCheck checker = new MaestroCheck(); + + for (OnFailError err : checker.check(new File(args[0]))) { + System.out.println(err.errno + " => " + err.message); + } + } + + static { + + final String key = "vdmj.mapping.search_path"; + String searchPath = System.getProperty(key); + if (searchPath == null) { + System.setProperty(key, "/annotations"); + } else { + System.setProperty(key, searchPath + File.pathSeparator + "/annotations"); + } + } + + + public List check(InputStream modelDescriptionStream) throws Exception { + File xmlfile = Files.createTempFile("fmi", ".xml", new FileAttribute[0]).toFile(); + xmlfile.deleteOnExit(); + copyStream(modelDescriptionStream, xmlfile.getParentFile(), xmlfile.getName()); + return check(xmlfile); + } + + public List check(File modelDescriptionFile) throws Exception { + List errors = new Vector<>(); + + File fmi2 = Files.createTempDirectory("fmi2", new FileAttribute[0]).toFile(); + fmi2.deleteOnExit(); + + File schema = new File(fmi2, "schema"); + schema.mkdir(); + schema.deleteOnExit(); + + copyResources(fmi2, "/schema/fmi2Annotation.xsd", "/schema/fmi2AttributeGroups.xsd", "/schema/fmi2ModelDescription.xsd", + "/schema/fmi2ScalarVariable.xsd", "/schema/fmi2Type.xsd", "/schema/fmi2Unit.xsd", "/schema/fmi2VariableDependency.xsd", + "/schema/fmi2.xsd", "/schema/fmi3Annotation.xsd", "/schema/fmi3BuildDescription.xsd", "/schema/fmi3TerminalsAndIcons.xsd", + "/schema/fmi3Terminal.xsd", "/schema/xsd2vdm.properties"); + + File xsdFile = new File(schema, "fmi2.xsd"); + OnFailError validation = validate(modelDescriptionFile, xsdFile); + + if (validation != null) { + errors.add(validation); + } else { + File vdmsl = new File(fmi2, "vdmsl"); + vdmsl.mkdir(); + vdmsl.deleteOnExit(); + + File vdmFile = new File(vdmsl, "model.vdmsl"); + vdmFile.deleteOnExit(); + + Xsd2VDM converter = new Xsd2VDM(); + Xsd2VDM.loadProperties(xsdFile); + Map vdmSchema = converter.createVDMSchema(xsdFile, modelDescriptionFile, false, true); + converter.createVDMValue(vdmSchema, vdmFile, modelDescriptionFile, "model"); + + if (vdmFile.exists()) // Means successful? + { + copyResources(vdmsl, "/CoSimulation_4.3.1.vdmsl", "/DefaultExperiment_2.2.5.vdmsl", "/FMI2Schema.vdmsl", + "/FMIModelDescription_2.2.1.vdmsl", "/LogCategories_2.2.4.vdmsl", "/Misc.vdmsl", "/ModelExchange_3.3.1.vdmsl", + "/ModelStructure_2.2.8.vdmsl", "/ModelVariables_2.2.7.vdmsl", "/TypeDefinitions_2.2.3.vdmsl", "/UnitDefinitions_2.2.2.vdmsl", + "/VariableNaming_2.2.9.vdmsl", "/VendorAnnotations_2.2.6.vdmsl", + + "/BuildConfiguration_2.3.vdmsl", "/GraphicalRepresentation_2.3.vdmsl", "/Terminals_2.3.vdmsl", "/VendorAnnotations_2.3.vdmsl", + "/Validation.vdmsl", "/XSD.vdmsl"); + + Properties.init(); + Settings.annotations = true; + ASTModuleList ast = new ASTModuleList(); + + for (File sl : vdmsl.listFiles()) { + LexTokenReader ltr = new LexTokenReader(sl, Dialect.VDM_SL); + ModuleReader mreader = new ModuleReader(ltr); + ast.addAll(mreader.readModules()); + + for (VDMError err : mreader.getErrors()) { + errors.add(new OnFailError(err.number, err.message)); + } + } + + if (!errors.isEmpty()) { + errors.add(new OnFailError(1, "Syntax errors in VDMSL?")); + } else { + ClassMapper instance = ClassMapper.getInstance(TCNode.MAPPINGS); + TCModuleList tc = instance.init().convert(ast); + tc.combineDefaults(); + TypeChecker tchecker = new ModuleTypeChecker(tc); + tchecker.typeCheck(); + + if (TypeChecker.getErrorCount() > 0) { + for (VDMError err : TypeChecker.getErrors()) { + errors.add(new OnFailError(err.number, err.message)); + } + + errors.add(new OnFailError(2, "Type errors in VDMSL?")); + } + + ClassMapper classMapper = ClassMapper.getInstance(INNode.MAPPINGS); + // patch(classMapper, CustomINOnFailAnnotation.class); + INModuleList in = classMapper.init().convert(tc); + Interpreter interpreter = new ModuleInterpreter(in, tc); + interpreter.init(); + INOnFailAnnotation.setErrorList(errors); + Value result = interpreter.execute("isValidFMIConfiguration(model)"); + + if (!result.boolValue(null)) { + errors.add(new OnFailError(3, "Errors found")); + } + } + } + } + + return errors; + } + + + private OnFailError validate(File xml, File xsd) { + try { + // Note that we pass a stream to allow the validator to determine the + // encoding, rather than passing a File, which seems to use default encoding. + Source xmlFile = new StreamSource(new FileInputStream(xml)); + xmlFile.setSystemId(xml.toURI().toASCIIString()); + Source xsdFile = new StreamSource(xsd); + xsdFile.setSystemId(xsd.toURI().toASCIIString()); + SchemaFactory schemaFactory = SchemaFactory.newInstance(XMLConstants.W3C_XML_SCHEMA_NS_URI); + + Schema schema = schemaFactory.newSchema(xsdFile); + Validator validator = schema.newValidator(); + validator.validate(xmlFile); + + return null; + } catch (SAXException e) { + return new OnFailError(0, "XML validation: " + e); // Raw exception gives file/line/col + } catch (Exception e) { + return new OnFailError(0, "XML validation: " + e.getMessage()); + } + } + + private void copyResources(File target, String... resources) throws Exception { + if (!target.exists()) { + throw new Exception("Target of copyResources does not exist: " + target); + } + + for (String resource : resources) { + InputStream is = MaestroCheck.class.getResourceAsStream(resource); + + if (is == null) { + throw new Exception("Cannot load resource " + resource); + } + + copyStream(is, target, resource); + is.close(); + } + } + + private void copyStream(InputStream data, File target, String file) throws IOException { + File targetFile = new File(target, file); + BufferedOutputStream bos = new BufferedOutputStream(new FileOutputStream(targetFile)); + + while (data.available() > 0) { + bos.write(data.read()); + } + + bos.close(); + targetFile.deleteOnExit(); // Note! All files temporary + } } diff --git a/fmi2/vdmcheck/src/main/java/vdmcheck/annotations/in/INOnFailAnnotation.java b/fmi2/vdmcheck/src/main/java/vdmcheck/annotations/in/INOnFailAnnotation.java new file mode 100644 index 00000000..69db8977 --- /dev/null +++ b/fmi2/vdmcheck/src/main/java/vdmcheck/annotations/in/INOnFailAnnotation.java @@ -0,0 +1,90 @@ +/****************************************************************************** + * + * Copyright (c) 2017-2022, INTO-CPS Association, + * c/o Professor Peter Gorm Larsen, Department of Engineering + * Finlandsgade 22, 8200 Aarhus N. + * + * This file is part of the INTO-CPS toolchain. + * + * MaestroCheck is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * MaestroCheck is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with MaestroCheck. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package vdmcheck.annotations.in; + +import com.fujitsu.vdmj.in.expressions.INExpression; +import com.fujitsu.vdmj.in.expressions.INExpressionList; +import com.fujitsu.vdmj.in.expressions.INIntegerLiteralExpression; +import com.fujitsu.vdmj.runtime.Context; +import com.fujitsu.vdmj.runtime.ValueException; +import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; +import com.fujitsu.vdmj.values.Value; +import maestro.OnFailError; + +import java.util.List; +import java.util.Vector; + +public class INOnFailAnnotation extends annotations.in.INOnFailAnnotation { + private static final long serialVersionUID = 1L; + private static List errorList = new Vector<>(); + + private final String format; + + public INOnFailAnnotation(TCIdentifierToken name, INExpressionList args, String format) { + super(name, args, format); + this.format = format; + } + + public INOnFailAnnotation(TCIdentifierToken name, INExpressionList args) { + this(name, args, ""); + } + + @Override + public void inAfter(INExpression exp, Value rv, Context ctxt) { + try { + if (!rv.boolValue(ctxt)) { + int errno = 0; + int offset = 1; + if (this.args.get(0) instanceof INIntegerLiteralExpression) { + INIntegerLiteralExpression num = (INIntegerLiteralExpression) this.args.get(0); + // errno = String.format("%04d: ", num.value.value); + errno = Long.valueOf(num.value.value).intValue(); + offset = 2; + } + + Object[] values = new Value[this.args.size() - offset]; + + for (int p = offset; p < this.args.size(); ++p) { + values[p - offset] = ((INExpression) this.args.get(p)).eval(ctxt); + } + + String location = ""; + String useformat = this.format; + if (this.format.endsWith("$")) { + location = this.name.getLocation().toString(); + useformat = this.format.substring(0, this.format.length() - 1); + } + errorList.add(new OnFailError(errno, String.format(useformat + location, values))); + // Console.out.printf(errno + useformat + location + "\n", values); + } + } catch (ValueException var9) { + } + + } + + public static void setErrorList(List errors) { + errorList = errors; + } +} diff --git a/fmi2/vdmcheck/src/main/resources/annotations/ast-tc.mappings b/fmi2/vdmcheck/src/main/resources/annotations/ast-tc.mappings deleted file mode 100644 index d62ecb36..00000000 --- a/fmi2/vdmcheck/src/main/resources/annotations/ast-tc.mappings +++ /dev/null @@ -1,7 +0,0 @@ -########################################################################################## -# The annotation class mapping definition for the VDMJ Type Checker. See ClassMapper. -########################################################################################## - -# annotations -package annotations.ast to annotations.tc; -map ASTOnFailAnnotation{name, args} to TCOnFailAnnotation(name, args); diff --git a/fmi2/vdmcheck/src/main/resources/annotations/tc-in.mappings b/fmi2/vdmcheck/src/main/resources/annotations/tc-in.mappings index 85864fa1..5dc3d916 100644 --- a/fmi2/vdmcheck/src/main/resources/annotations/tc-in.mappings +++ b/fmi2/vdmcheck/src/main/resources/annotations/tc-in.mappings @@ -3,5 +3,5 @@ ########################################################################################## # annotations -package annotations.tc to annotations.in; -map TCOnFailAnnotation{name, args} to INOnFailAnnotation(name, args); +package annotations.tc to vdmcheck.annotations.in; +map TCOnFailAnnotation{name, args,format} to INOnFailAnnotation(name, args,format); diff --git a/fmi2/vdmcheck/src/main/resources/annotations/tc-po.mappings b/fmi2/vdmcheck/src/main/resources/annotations/tc-po.mappings deleted file mode 100644 index 46459f5c..00000000 --- a/fmi2/vdmcheck/src/main/resources/annotations/tc-po.mappings +++ /dev/null @@ -1,8 +0,0 @@ -########################################################################################## -# The class mapping definition for the VDMJ Proof Obligation Generator. See ClassMapper. -########################################################################################## - -# annotations -package annotations.tc to annotations.po; -map TCOnFailAnnotation{name, args} to PONullAnnotation(name, args); - diff --git a/fmi2/vdmcheck/src/test/java/MaestroCheckTest.java b/fmi2/vdmcheck/src/test/java/MaestroCheckTest.java new file mode 100644 index 00000000..fa512983 --- /dev/null +++ b/fmi2/vdmcheck/src/test/java/MaestroCheckTest.java @@ -0,0 +1,19 @@ +import maestro.MaestroCheck; +import maestro.OnFailError; +import org.junit.Assert; +import org.junit.Test; + +import java.nio.file.Paths; +import java.util.List; + +public class MaestroCheckTest { + @Test + public void test() throws Exception { + + MaestroCheck checker = new MaestroCheck(); + + List errors = checker.check(Paths.get("src", "test", "resources", "modelDescription.xml").toFile()); + Assert.assertEquals(2, errors.size()); + Assert.assertEquals(1029, errors.get(0).errno); + } +}