/******************************************************************************
 *
 *	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.
 *
 *	VDMCheck 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.
 *
 *	VDMCheck 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 VDMCheck. If not, see <http://www.gnu.org/licenses/>.
 *	SPDX-License-Identifier: GPL-3.0-or-later
 *
 ******************************************************************************/

import java.io.BufferedReader;
import java.io.ByteArrayInputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.io.PrintStream;
import java.io.StringReader;
import java.net.URISyntaxException;
import java.util.List;
import java.util.Random;
import java.util.Vector;
import java.util.zip.ZipEntry;
import java.util.zip.ZipException;
import java.util.zip.ZipFile;

import javax.xml.parsers.DocumentBuilder;
import javax.xml.parsers.DocumentBuilderFactory;

import org.xml.sax.InputSource;
import org.xml.sax.SAXException;

public class VDMCheck
{
	public static void main(String[] args)
	{
		String filename = null;
		String vdmOUT = null;
		String xmlIN = null;
		
		for (int a=0; a < args.length; a++)
		{
			switch (args[a])
			{
				default:
					filename = args[a];
					break;
					
				case "-v":
					vdmOUT = args[++a];
					break;
				
				case "-x":
					xmlIN = args[++a];
					break;
			}
		}
		
		if (filename == null && xmlIN == null)
		{
			System.err.println("Usage: java -jar vdmcheck2.jar [-v <VDM outfile>] -x <XML> | <file>.fmu | <file>.xml");
			System.exit(1);
		}
		else
		{
			if (vdmOUT != null)
			{
				new File(vdmOUT).delete();
			}
			
			List<XMLFile> checkList = getCheckList(filename, xmlIN);
			boolean failed = (checkList == null);
			
			if (!failed)
			{
				for (XMLFile tempXML: checkList)
				{
					boolean ok = run(filename, tempXML, vdmOUT);
					failed = failed || !ok;
				}
			}
			
			System.exit(failed ? 1 : 0);
		}
	}
	
	private static class XMLFile
	{
		public final String name;	// Sensible name
		public final File file;		// temp file path
		
		public XMLFile(String name, File file)
		{
			this.name = name;
			this.file = file;
		}
	}
	
	private static List<XMLFile> getCheckList(String filename, String xmlIN)
	{
		List<XMLFile> results = new Vector<XMLFile>();
		
		try
		{
			File fmuFile = filename == null ? null : new File(filename);

			if (fmuFile != null && !fmuFile.exists())
			{
				System.err.printf("File %s not found\n", filename);
				return null;
			}
			
			if (xmlIN != null)
			{
				try
				{
					DocumentBuilderFactory dbFactory = DocumentBuilderFactory.newInstance();
					DocumentBuilder dBuilder = dbFactory.newDocumentBuilder();
					dBuilder.parse(new InputSource(new StringReader(xmlIN)));
				}
				catch (SAXException e)
				{
					System.err.println("XML errors found");
					return null;
				}
				
				// Write XML into tempXML
				File tempXML = File.createTempFile("XML", "tmp");
				tempXML.deleteOnExit();
				copy(new ByteArrayInputStream(xmlIN.getBytes()), tempXML);
				results.add(new XMLFile("XML", tempXML));
			}
			else
			{
				ZipFile zip = null;
				try
				{
					zip = new ZipFile(fmuFile);
					ZipEntry entry = zip.getEntry("modelDescription.xml");
					
					if (entry == null)
					{
						System.err.printf("Cannot locate modelDescription.xml in %s\n", filename);
						return null;
					}
					
					File tempXML = File.createTempFile("modelDescription", "tmp");
					tempXML.deleteOnExit();
					copy(zip.getInputStream(entry), tempXML);
					results.add(new XMLFile("modelDescription.xml", tempXML));
					
					entry = zip.getEntry("icon/terminalsAndIcons.xml");
					
					if (entry != null)
					{
						File tempXML2 = File.createTempFile("terminalsAndIcons", "tmp");
						tempXML2.deleteOnExit();
						copy(zip.getInputStream(entry), tempXML2);
						results.add(new XMLFile("icon/terminalsAndIcons.xml", tempXML2));
					}
					else
					{
						System.out.println("FMU has no icon/terminalsAndIcons.xml");
					}
					
					entry = zip.getEntry("source/buildDescription.xml");
					
					if (entry != null)
					{
						File tempXML3 = File.createTempFile("buildDescription", "tmp");
						tempXML3.deleteOnExit();
						copy(zip.getInputStream(entry), tempXML3);
						results.add(new XMLFile("source/buildDescription.xml", tempXML3));
					}
					else
					{
						System.out.println("FMU has no source/buildDescription.xml");
					}
				}
				catch (ZipException e)	// Not a zip file, assume raw XML
				{
					try
					{
						DocumentBuilderFactory dbFactory = DocumentBuilderFactory.newInstance();
						DocumentBuilder dBuilder = dbFactory.newDocumentBuilder();
						dBuilder.parse(fmuFile);
					}
					catch (SAXException e1)
					{
						System.err.printf("Exception: %s\n", e1.getMessage());
						System.err.printf("Input %s is neither a ZIP nor an XML file?\n", filename);
						return null;
					}
					catch (Exception e1)
					{
						System.err.printf("Input %s is neither a ZIP nor an XML file?\n", filename);
						return null;
					}

					File tempXML = File.createTempFile("XML", "tmp");
					tempXML.deleteOnExit();
					copy(new FileInputStream(fmuFile), tempXML);
					results.add(new XMLFile("XML", tempXML));
				}
				finally
				{
					if (zip != null) zip.close();
				}
			}
		}
		catch (Exception e)
		{
			System.err.printf("Error: %s\n", e.getMessage());
			results.clear();
		}
		
		return results;
	}

	private static boolean run(String filename, XMLFile tempXML, String vdmOUT)
	{
		try
		{
			// Execute VDMJ to first convert tempXML to VDM-SL, then validate the VDM.
			System.out.println("Checking " + tempXML.name);
			File jarLocation = getJarLocation();
			
			String varName = "model" + (new Random().nextInt(9999));
		
			File tempVDM = File.createTempFile("vdm", "tmp");
			tempVDM.deleteOnExit();
			
			File tempOUT = File.createTempFile("out", "tmp");
			tempOUT.deleteOnExit();
			
			File schema = new File(jarLocation.getAbsolutePath() + File.separator + "schema/fmi2.xsd");
			
			int exit = runCommand(jarLocation, tempOUT,
					"java", "-jar", "xsd2vdm.jar", 
					"-xsd", schema.getCanonicalPath(),
					"-xml", tempXML.file.getCanonicalPath(),
					"-vdm", tempVDM.getCanonicalPath(),
					"-name", varName,
					"-nowarn");
			
			String[] dependencies = {"vdmj.jar", "annotations.jar"};
	
			runCommand(jarLocation, tempOUT,
					"java", "-Xmx1g", "-cp", String.join(File.pathSeparator, dependencies), 
					"com.fujitsu.vdmj.VDMJ", "-vdmsl", "-q", "-annotations",
					"-e", "isValidFMIConfiguration(" + varName + ")", "model", tempVDM.getCanonicalPath());
	
			sed(tempOUT, System.out,
					"^true$", "No errors found.",
					"^false$", "Errors found.");
			
			exit = grep("^true$", tempOUT) ? 0 : 1;

			if (vdmOUT != null)
			{
				if (filename == null) filename = "XML";
				
				sed(tempVDM, new PrintStream(new FileOutputStream(vdmOUT, true)),
					"generated from " + tempXML.file, "generated from " + tempXML.name);
				
				System.out.println("VDM source written to " + vdmOUT);
			}
			
			return exit == 0;
		}
		catch (Exception e)
		{
			System.err.printf("Error: %s\n", e.getMessage());
			return false;
		}
	}
	
	private static void copy(InputStream in, File outfile) throws IOException
	{
		OutputStream out = new FileOutputStream(outfile);
		
		for (int b = in.read(); b != -1; b = in.read())
		{
			out.write(b);
		}
		
		in.close();
		out.close();
	}
	
	private static File getJarLocation()
	{
		try
		{
			File location = new File(VDMCheck.class.getProtectionDomain()
					.getCodeSource().getLocation().toURI());
			
			return location.getParentFile();
		}
		catch (URISyntaxException e)
		{
			// can't happen?
			return null;
		}
	}
	
	private static int runCommand(File dir, File output, String... cmd) throws IOException
	{
		Process p = null;
		
		try
		{
			ProcessBuilder pb = new ProcessBuilder(cmd);
			pb.directory(dir);
			pb.inheritIO();
			if (output != null) pb.redirectOutput(output);
			p = pb.start();
			p.waitFor();
		}
		catch (InterruptedException e)
		{
			// Never happens?
		}
		
		return p.exitValue();
	}
	
	private static void sed(File input, PrintStream output, String... subs) throws IOException
	{
		if (subs.length % 2 != 0)
		{
			throw new IOException("Substitutions must be pairs");
		}
		
		BufferedReader br = new BufferedReader(new FileReader(input));
		String line = br.readLine();
		
		while (line != null)
		{
			for (int s=0; s < subs.length; s+=2)
			{
				line = line.replaceAll(subs[s], subs[s+1]);
			}
			
			output.println(line);
			line = br.readLine();
		}
		
		br.close();
	}

	private static boolean grep(String pattern, File input) throws IOException
	{
		BufferedReader br = new BufferedReader(new FileReader(input));
		String line = br.readLine();
		boolean result = false;
		
		while (line != null)
		{
			result = result || line.matches(pattern);
			line = br.readLine();
		}
		
		br.close();
		return result;
	}
}
