Skip to content

Commit

Permalink
Add VDMJUnitLifecycle
Browse files Browse the repository at this point in the history
  • Loading branch information
nickbattle committed Oct 20, 2023
1 parent 23c97d9 commit 2b9c9b1
Show file tree
Hide file tree
Showing 3 changed files with 139 additions and 189 deletions.
18 changes: 1 addition & 17 deletions vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java
Original file line number Diff line number Diff line change
Expand Up @@ -471,22 +471,6 @@ protected boolean checkAndInitFiles()
return false;
}

/**
* These setters are used by DBGPReader, so that it can use the other
* lifecycle methods to parse/check the spec.
*/
public void setFiles(List<File> files)
{
this.files = files;
}

public void setArgs(String... args)
{
this.argv = new Vector<String>(Arrays.asList(args));
processArgs();
}


private int display(List<VDMMessage> messages, Class<? extends VDMMessage>type, boolean show)
{
int count = 0;
Expand All @@ -503,7 +487,7 @@ private int display(List<VDMMessage> messages, Class<? extends VDMMessage>type,
return count;
}

private boolean report(List<VDMMessage> messages, AbstractCheckFilesEvent event)
protected boolean report(List<VDMMessage> messages, AbstractCheckFilesEvent event)
{
int nerrs = display(messages, VDMError.class, true);
int nwarns = display(messages, VDMWarning.class, warnings);
Expand Down
181 changes: 9 additions & 172 deletions vdmjunit/src/main/java/com/fujitsu/vdmjunit/SpecificationReader.java
Original file line number Diff line number Diff line change
Expand Up @@ -24,19 +24,10 @@

package com.fujitsu.vdmjunit;

import static com.fujitsu.vdmj.plugins.PluginConsole.info;
import static com.fujitsu.vdmj.plugins.PluginConsole.infoln;
import static com.fujitsu.vdmj.plugins.PluginConsole.plural;
import static com.fujitsu.vdmj.plugins.PluginConsole.println;
import static com.fujitsu.vdmj.plugins.PluginConsole.verboseln;
import static org.junit.Assert.fail;

import java.io.File;
import java.io.FileNotFoundException;
import java.net.URL;
import java.nio.charset.Charset;
import java.util.List;
import java.util.Vector;

import com.fujitsu.vdmj.Settings;
import com.fujitsu.vdmj.config.Properties;
Expand All @@ -46,24 +37,14 @@
import com.fujitsu.vdmj.messages.VDMWarning;
import com.fujitsu.vdmj.plugins.EventHub;
import com.fujitsu.vdmj.plugins.PluginRegistry;
import com.fujitsu.vdmj.plugins.VDMJ;
import com.fujitsu.vdmj.plugins.analyses.ASTPlugin;
import com.fujitsu.vdmj.plugins.events.AbstractCheckFilesEvent;
import com.fujitsu.vdmj.plugins.events.CheckCompleteEvent;
import com.fujitsu.vdmj.plugins.events.CheckFailedEvent;
import com.fujitsu.vdmj.plugins.events.CheckPrepareEvent;
import com.fujitsu.vdmj.plugins.events.CheckSyntaxEvent;
import com.fujitsu.vdmj.plugins.events.CheckTypeEvent;
import com.fujitsu.vdmj.runtime.Interpreter;
import com.fujitsu.vdmj.util.GetResource;

/**
* The abstract parent class of all specification readers.
*/
abstract public class SpecificationReader
{
protected List<VDMError> errors = new Vector<VDMError>();
protected List<VDMWarning> warnings = new Vector<VDMWarning>();
private VDMJUnitLifecycle lifecycle = null;

/**
* Construct a SpecificationReader for a particular VDM dialect.
Expand All @@ -76,8 +57,10 @@ public SpecificationReader(Dialect dialect)
Settings.dialect = dialect;
PluginRegistry.reset();
EventHub.reset();
VDMJ.loadPlugins();
VDMJ.setArgs("-i"); // Because we want an interpreter

lifecycle = new VDMJUnitLifecycle("-i"); // Because we want an interpreter
lifecycle.loadPlugins();
lifecycle.processArgs();
}

/**
Expand Down Expand Up @@ -105,46 +88,9 @@ protected void printMessages(List<? extends VDMMessage> messages)
*/
public Interpreter readSpecification(Charset charset, String... filenames) throws Exception
{
Settings.filecharset = charset;
List<File> list = new Vector<File>(filenames.length);

for (String filename: filenames)
{
URL url = getClass().getResource("/" + filename);

if (url == null)
{
throw new FileNotFoundException(filename);
}

File file = null;

if (url.getProtocol().equals("jar"))
{
file = GetResource.load(new File("/" + filename));
}
else
{
file = new File(url.toURI());
}

if (file.isDirectory())
{
for (File subfile: file.listFiles(Settings.dialect.getFilter()))
{
if (subfile.isFile())
{
list.add(subfile);
}
}
}
else
{
list.add(file);
}
}
lifecycle.findFiles(charset, filenames);

if (!pluginLifecycle(list))
if (!lifecycle.checkAndInitFiles())
{
fail("Type errors (see stdout)");
}
Expand All @@ -158,7 +104,7 @@ public Interpreter readSpecification(Charset charset, String... filenames) throw
*/
public List<VDMError> getErrors()
{
return errors;
return lifecycle.errors;
}

/**
Expand All @@ -167,115 +113,6 @@ public List<VDMError> getErrors()
*/
public List<VDMWarning> getWarnings()
{
return warnings;
}

/**
* Methods to help with VDMJ plugin event processing.
*/
private boolean pluginLifecycle(List<File> files)
{
try
{
EventHub eventhub = EventHub.getInstance();
AbstractCheckFilesEvent event = new CheckPrepareEvent(files);
List<VDMMessage> messages = eventhub.publish(event);

if (report(messages, event))
{
event = new CheckSyntaxEvent();
messages = eventhub.publish(event);

if (report(messages, event))
{
event = new CheckTypeEvent();
messages = eventhub.publish(event);

if (report(messages, event))
{
event = new CheckCompleteEvent();
messages = eventhub.publish(event);

if (report(messages, event))
{
verboseln("Loaded files initialized successfully");
return true;
}
else
{
verboseln("Failed to initialize interpreter");
messages.addAll(eventhub.publish(new CheckFailedEvent(event)));
}
}
else
{
verboseln("Type checking errors found");
messages.addAll(eventhub.publish(new CheckFailedEvent(event)));
}
}
else
{
verboseln("Syntax errors found");
messages.addAll(eventhub.publish(new CheckFailedEvent(event)));
}
}
else
{
verboseln("Preparation errors found");
messages.addAll(eventhub.publish(new CheckFailedEvent(event)));
}
}
catch (Exception e)
{
println(e);
System.exit(1);
}

return false;
}

private boolean report(List<VDMMessage> messages, AbstractCheckFilesEvent event)
{
int nerrs = 0;
int nwarns = 0;

for (VDMMessage m: messages)
{
if (m instanceof VDMError && !errors.contains(m))
{
errors.add((VDMError)m);
println(m);
nerrs++;
}
else if (m instanceof VDMWarning && ! warnings.contains(m))
{
warnings.add((VDMWarning)m);
println(m);
nwarns++;
}
}

ASTPlugin ast = PluginRegistry.getInstance().getPlugin("AST");
int count = ast.getCount();

if (count > 0) // Just using -i gives count = 0
{
String objects = Settings.dialect == Dialect.VDM_SL ?
plural(count, "module", "s") :
plural(count, "class", "es");

double duration = (double)(EventHub.getInstance().getLastDuration())/1000;
String title = event.getProperty(AbstractCheckFilesEvent.TITLE);
String kind = event.getProperty(AbstractCheckFilesEvent.KIND);

if (nerrs > 0 || nwarns > 0)
{
info(title + " " + objects + " in " + duration + " secs. ");
info(nerrs == 0 ? "No " + kind + " errors" : "Found " + plural(nerrs, kind + " error", "s"));
infoln(nwarns == 0 ? "" : " and " + plural(nwarns, "warning", "s"));
}
}

return (nerrs == 0); // Return "OK" if we can continue (ie. no errors)
return lifecycle.warnings;
}
}
129 changes: 129 additions & 0 deletions vdmjunit/src/main/java/com/fujitsu/vdmjunit/VDMJUnitLifecycle.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,129 @@
/*******************************************************************************
*
* Copyright (c) 2023 Nick Battle.
*
* 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 <http://www.gnu.org/licenses/>.
* SPDX-License-Identifier: GPL-3.0-or-later
*
******************************************************************************/

package com.fujitsu.vdmjunit;

import java.io.File;
import java.io.FileNotFoundException;
import java.net.URL;
import java.nio.charset.Charset;
import java.util.List;
import java.util.Vector;

import com.fujitsu.vdmj.Settings;
import com.fujitsu.vdmj.messages.VDMError;
import com.fujitsu.vdmj.messages.VDMMessage;
import com.fujitsu.vdmj.messages.VDMWarning;
import com.fujitsu.vdmj.plugins.Lifecycle;
import com.fujitsu.vdmj.plugins.events.AbstractCheckFilesEvent;
import com.fujitsu.vdmj.util.GetResource;

public class VDMJUnitLifecycle extends Lifecycle
{
protected List<VDMError> errors = new Vector<VDMError>();
protected List<VDMWarning> warnings = new Vector<VDMWarning>();

public VDMJUnitLifecycle(String... args)
{
super(args);
}

@Override
protected void loadPlugins()
{
super.loadPlugins();
}

@Override
protected void processArgs()
{
super.processArgs();
}

protected void findFiles(Charset charset, String... filenames) throws Exception
{
Settings.filecharset = charset;
files = new Vector<File>(filenames.length);

for (String filename: filenames)
{
URL url = getClass().getResource("/" + filename);

if (url == null)
{
throw new FileNotFoundException(filename);
}

File file = null;

if (url.getProtocol().equals("jar"))
{
file = GetResource.load(new File("/" + filename));
}
else
{
file = new File(url.toURI());
}

if (file.isDirectory())
{
for (File subfile: file.listFiles(Settings.dialect.getFilter()))
{
if (subfile.isFile())
{
files.add(subfile);
}
}
}
else
{
files.add(file);
}
}
}

@Override
protected boolean checkAndInitFiles()
{
return super.checkAndInitFiles();
}

@Override
protected boolean report(List<VDMMessage> messages, AbstractCheckFilesEvent event)
{
for (VDMMessage m: messages)
{
if (m instanceof VDMError && !errors.contains(m))
{
errors.add((VDMError)m);
}
else if (m instanceof VDMWarning && ! warnings.contains(m))
{
warnings.add((VDMWarning)m);
}
}

return super.report(messages, event);
}
}

0 comments on commit 2b9c9b1

Please sign in to comment.