#
# ChangeLog for src/compiler.ma
#
# Generated by Trac 1.2
# Jan 28, 2021, 9:26:09 AM

Sun, 24 Mar 2013 10:29:01 GMT tranquil [2946]
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToERTLptrAxiom.ma (added)
	* src/ERTL/ERTL_semantics.ma (modified)
	* src/ERTL/ERTLtoERTLptrUtils.ma (modified)
	* src/ERTLptr/ERTLptr.ma (modified)
	* src/ERTLptr/ERTLptrToLTLAxiom.ma (added)
	* src/ERTLptr/ERTLptr_semantics.ma (modified)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LIN/LINToASMAxiom.ma (added)
	* src/LIN/LIN_semantics.ma (modified)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLINAxiom.ma (moved)
	* src/LTL/LTL_semantics.ma (modified)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLToERTLAxiom.ma (moved)
	* src/RTL/RTL_overflow_to_unique.ma (added)
	* src/RTL/RTL_semantics.ma (modified)
	* src/RTL/RTL_separate_to_overflow.ma (added)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTLAxiom.ma (moved)
	* src/compiler.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/joint_fullexec.ma (modified)
	* src/joint/joint_semantics.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	main novelties:
	* there is an in-built stack_usage nat in joint ...


Thu, 21 Mar 2013 20:45:49 GMT campbell [2936]
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/RTLabs_syntax.ma (modified)
	* src/compiler.ma (modified)

	Disable initialisation code generation in Cminor, propogate init data ...


Tue, 19 Mar 2013 18:48:19 GMT sacerdot [2907]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/ASM/CostsProof.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/compiler.ma (modified)

	1. a few bugs fixed
	2. as_return implemented for ASM & OC


Mon, 18 Mar 2013 23:33:13 GMT sacerdot [2899]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/ASM/AbstractStatus.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplitSplit.ma (modified)
	* src/ASM/CostsProof.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/compiler.ma (modified)
	* src/semantics.ma (modified)

	1. some renaming ASM_xxx to OC_xxx
	2. ASM_pre_classified_system ...


Fri, 15 Mar 2013 00:32:50 GMT sacerdot [2875]
	* driver/backendPrinter.ml (modified)
	* driver/build (modified)
	* driver/cerco.ml (modified)
	* extracted/compiler.ml (modified)
	* extracted/compiler.mli (modified)
	* extracted/semantics.ml (modified)
	* extracted/semantics.mli (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)
	* src/semantics.ma (modified)

	Pretty printing of object code integrated too.
	A couple of axioms ...


Mon, 11 Mar 2013 11:40:46 GMT sacerdot [2841]
	* src/compiler.ma (modified)
	* src/semantics.ma (modified)

	The compiler now computes also the stack cost for every intermediate ...


Fri, 08 Mar 2013 22:54:35 GMT sacerdot [2835]
	* src/compiler.ma (modified)

	Included Uses.ma which is required by the untrusted code.
	The ...


Fri, 08 Mar 2013 22:17:44 GMT sacerdot [2828]
	* src/compiler.ma (modified)
	* src/semantics.ma (added)

	1. New semantics.ma file that puts together all semantics.
	   It ...


Thu, 07 Mar 2013 06:47:33 GMT mckinna [2794]
	* src/compiler.ma (modified)

	Minor tweaks/tidying up


Tue, 05 Mar 2013 17:15:06 GMT sacerdot [2774]
	* src/ERTLptr/ERTLptrToLTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)
	* src/joint/Joint.ma (modified)

	1. the compiler now outputs both the stack cost model and the max ...


Sun, 03 Mar 2013 13:03:58 GMT mckinna [2767]
	* src/ASM/ASM.ma (modified)
	* src/ASM/BitVectorTrie.ma (modified)
	* src/ASM/CodeMemory.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/common/LabelledObjects.ma (modified)
	* src/compiler.ma (modified)
	* src/utilities/extranat.ma (modified)
	* src/utilities/option.ma (modified)

	WARNING: BIG commit, which pushes code_size_opt check into ...


Sat, 02 Mar 2013 10:42:16 GMT sacerdot [2763]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Policy.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/compiler.ma (modified)

	All daemons in compiler.ma closed (i.e. proof obligations added
	to ...


Sat, 02 Mar 2013 01:37:43 GMT sacerdot [2762]
	* src/ASM/Policy.ma (modified)
	* src/compiler.ma (modified)

	All repaired up to compiler.ma.

	Note: one daemon is left for one ...


Fri, 01 Mar 2013 09:26:31 GMT sacerdot [2754]
	* src/ASM/ASM.ma (modified)
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/CodeMemory.ma (modified)
	* src/ASM/CostsProof.ma (modified)
	* src/ASM/Fetch.ma (modified)
	* src/ASM/Interpret2.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/BACKEND_BROKEN_FILES (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/compiler.ma (modified)

	1. WARNING: I commented out one of James's function used in ...


Thu, 28 Feb 2013 16:56:55 GMT mckinna [2753]
	* src/compiler.ma (modified)

	Further tidying up thanks to Claudio's strong_decidable intervention; ...


Thu, 28 Feb 2013 13:36:34 GMT mckinna [2752]
	* src/compiler.ma (modified)

	Fixed TODO regarding length of list_instr
	Added ASM/CodeMemory.ma to ...


Wed, 27 Feb 2013 21:46:05 GMT sacerdot [2745]
	* src/ASM/Policy.ma (modified)
	* src/compiler.ma (modified)

	1. Complexity of policy computation lowered from O(n^2) to O(n)
	2. ...


Sun, 24 Feb 2013 19:39:19 GMT campbell [2724]
	* src/RTLabs/CostCheck.ma (modified)
	* src/RTLabs/RTLabs_abstract.ma (modified)
	* src/RTLabs/RTLabs_traces.ma (modified)
	* src/common/ErrorMessages.ma (modified)
	* src/compiler.ma (modified)

	Add RTLabs cost labelling checks to compiler.ma.


Fri, 22 Feb 2013 18:17:44 GMT sacerdot [2709]
	* src/compiler.ma (modified)

	LINToAsm repaired


Fri, 22 Feb 2013 16:56:31 GMT sacerdot [2705]
	* src/ASM/ASM.ma (modified)
	* src/ASM/AbstractStatus.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/BACKEND_BROKEN_FILES (modified)
	* src/compiler.ma (modified)

	More progress in ASM towards implementing the new pseudoinstructions.


Fri, 22 Feb 2013 14:27:16 GMT sacerdot [2702]
	* src/ASM/UtilBranch.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/linearise.ma (modified)

	1. proof closed in ASM/UtilBranch
	2. more passes integrated in the ...


Fri, 22 Feb 2013 13:12:24 GMT sacerdot [2700]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/Policy.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ERTLptr/ERTLptrToLTL.ma (modified)
	* src/ERTLptr/Interference.ma (modified)
	* src/ERTLptr/liveness.ma (modified)
	* src/compiler.ma (modified)
	* src/utilities/fixpoints.ma (modified)

	1. exponential function dropped in favour of standard library
	2. ...


Fri, 22 Feb 2013 11:13:51 GMT sacerdot [2697]
	* src/ERTLptr/ERTLptrToLTL.ma (modified)
	* src/compiler.ma (modified)

	Compiler fixed to include the ERTLptrToLTL pass.


Fri, 22 Feb 2013 10:39:03 GMT sacerdot [2693]
	* src/BACKEND_BROKEN_FILES (modified)
	* src/ERTLptr/ERTLptrToLTL.ma (moved)
	* src/ERTLptr/Interference.ma (moved)
	* src/ERTLptr/liveness.ma (moved)
	* src/compiler.ma (modified)

	1. Stuff moved to correct places.
	2. ERTLptr pass added


Thu, 07 Feb 2013 20:22:22 GMT sacerdot [2645]
	* src/ASM/ASM.ma (modified)
	* src/ASM/BitVector.ma (modified)
	* src/ASM/Char.ma (deleted)
	* src/ASM/I8051.ma (modified)
	* src/BACKEND_BROKEN_FILES (added)
	* src/Clight/Cexec.ma (modified)
	* src/Clight/Csyntax.ma (modified)
	* src/Clight/TypeComparison.ma (modified)
	* src/Clight/test/addptrcharboth.test.ma (modified)
	* src/Clight/test/badconditional.test.ma (modified)
	* src/Clight/test/controlflow.test.ma (modified)
	* src/Clight/test/endptr.test.ma (modified)
	* src/Clight/test/endptr2.test.ma (modified)
	* src/Clight/test/forcont.test.ma (modified)
	* src/Clight/test/goto-if.test.ma (modified)
	* src/Clight/test/implicit.test.ma (modified)
	* src/Clight/test/implicitcond.test.ma (modified)
	* src/Clight/test/sum.test.ma (modified)
	* src/Clight/test/trivial.test.ma (modified)
	* src/Clight/toCminor.ma (modified)
	* src/Cminor/Cminor_semantics.ma (modified)
	* src/Cminor/Cminor_syntax.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTLptr/ERTLptr.ma (modified)
	* src/ERTLptr/ERTLtoERTLptrOK.ma (modified)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/RTL/RTL_semantics.ma (modified)
	* src/RTLabs/RTLabs_semantics.ma (modified)
	* src/RTLabs/import.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Animation.ma (modified)
	* src/common/BackEndOps.ma (modified)
	* src/common/ByteValues.ma (modified)
	* src/common/CostLabel.ma (modified)
	* src/common/ErrorMessages.ma (added)
	* src/common/Errors.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/common/Graphs.ma (modified)
	* src/common/IO.ma (modified)
	* src/common/Identifiers.ma (modified)
	* src/common/PreIdentifiers.ma (modified)
	* src/common/Registers.ma (modified)
	* src/common/Values.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/String.ma (moved)
	* src/joint/Traces.ma (modified)
	* src/joint/joint_semantics.ma (modified)
	* src/joint/semanticsUtils.ma (modified)

	1. some broken back-end files repaires, several still to go
	2. the ...


Tue, 15 Jan 2013 14:45:28 GMT mckinna [2581]
	* src/compiler.ma (modified)

	commented out back end entirely until knock-on effects of changes to ...


Sat, 01 Dec 2012 19:36:52 GMT mckinna [2512]
	* src/compiler.ma (modified)

	Simplified dependencies on ASM, to allow rollback to when ...


Thu, 29 Nov 2012 19:12:34 GMT mckinna [2508]
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/common/StructuredTraces.ma (modified)
	* src/compiler.ma (modified)

	more tweaks. compiler and correctness still build.


Thu, 29 Nov 2012 14:37:22 GMT mckinna [2505]
	* src/Clight/label.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/compiler.ma (modified)

	Cleaned up compiler.ma; some refactoring/additional code needed in ...


Tue, 27 Nov 2012 16:59:25 GMT mckinna [2497]
	* src/compiler.ma (modified)

	Simplified dependencies on ASM; knock-on from changes in ASM/*.ma


Mon, 26 Nov 2012 17:24:20 GMT mckinna [2494]
	* src/compiler.ma (modified)

	Removed BJC's axiomatisation of rtlabs_to_rtl, now that ...


Mon, 26 Nov 2012 10:52:51 GMT campbell [2492]
	* src/compiler.ma (modified)

	Reduce axiomatisation in compiler.ma.


Mon, 19 Nov 2012 16:13:21 GMT campbell [2475]
	* src/ASM/ASMCosts.ma (modified)
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/RTLabs/semantics.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Get compiler.ma and correctness.ma checking again.  Note that the ...


Wed, 17 Oct 2012 16:45:20 GMT campbell [2399]
	* src/Clight/label.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Fill in some details about the statement of correctness.


Mon, 03 Sep 2012 14:33:33 GMT campbell [2320]
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Update compiler and correctness with labelling changes.


Mon, 03 Sep 2012 11:16:29 GMT campbell [2319]
	* src/Clight/label.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/Clight/labelSpecification.ma (modified)
	* src/Cminor/initialisation.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/common/AST.ma (modified)
	* src/common/Globalenvs.ma (modified)
	* src/compiler.ma (modified)

	Generate per-program cost labels rather than per-function ones, and ...


Thu, 02 Aug 2012 15:04:38 GMT campbell [2291]
	* src/compiler.ma (modified)

	Disable switch removal in compiler.ma for now.


Thu, 02 Aug 2012 13:18:11 GMT tranquil [2286]
	* src/ASM/I8051.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/ERTL/ERTL.ma (modified)
	* src/ERTL/ERTLToLTL.ma (modified)
	* src/ERTL/ERTLToLTL_paolo.ma (deleted)
	* src/ERTL/ERTL_paolo.ma (deleted)
	* src/ERTL/Interference.ma (modified)
	* src/ERTL/Interference_paolo.ma (deleted)
	* src/ERTL/liveness.ma (modified)
	* src/ERTL/liveness_paolo.ma (deleted)
	* src/ERTL/semantics.ma (modified)
	* src/ERTL/semantics_paolo.ma (deleted)
	* src/LIN/LIN.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/LIN/LIN_paolo.ma (deleted)
	* src/LIN/joint_LTL_LIN.ma (modified)
	* src/LIN/joint_LTL_LIN_paolo.ma (deleted)
	* src/LIN/joint_LTL_LIN_semantics.ma (modified)
	* src/LIN/joint_LTL_LIN_semantics_paolo.ma (deleted)
	* src/LIN/semantics.ma (modified)
	* src/LIN/semantics_paolo.ma (deleted)
	* src/LTL/LTL.ma (modified)
	* src/LTL/LTLToLIN.ma (modified)
	* src/LTL/LTLToLIN_paolo.ma (deleted)
	* src/LTL/LTL_paolo.ma (deleted)
	* src/LTL/semantics.ma (modified)
	* src/LTL/semantics_paolo.ma (deleted)
	* src/RTL/RTL.ma (modified)
	* src/RTL/RTLTailcall.ma (modified)
	* src/RTL/RTLTailcall_paolo.ma (deleted)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTL/RTLToERTL_paolo.ma (deleted)
	* src/RTL/RTL_paolo.ma (deleted)
	* src/RTL/semantics.ma (modified)
	* src/RTL/semantics_paolo.ma (deleted)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/RTLabs/RTLabsToRTL_paolo.ma (deleted)
	* src/common/AST.ma (modified)
	* src/common/BackEndOps.ma (added)
	* src/common/ByteValues.ma (modified)
	* src/common/ByteValues_paolo.ma (deleted)
	* src/common/FrontEndVal.ma (modified)
	* src/common/Registers.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/BEMem.ma (modified)
	* src/joint/Joint.ma (modified)
	* src/joint/Joint_paolo.ma (deleted)
	* src/joint/SemanticUtils.ma (modified)
	* src/joint/Traces.ma (modified)
	* src/joint/TranslateUtils.ma (modified)
	* src/joint/TranslateUtils_paolo.ma (deleted)
	* src/joint/blocks.ma (modified)
	* src/joint/linearise.ma (modified)
	* src/joint/semantics.ma (modified)
	* src/joint/semanticsUtils_paolo.ma (deleted)
	* src/joint/semantics_paolo.ma (deleted)
	* src/utilities/extranat.ma (modified)

	Big update!

	* merge of all _paolo variants
	* reorganised some ...


Tue, 24 Jul 2012 17:40:22 GMT campbell [2253]
	* src/Clight/test/goto-if.test.ma (modified)
	* src/Clight/test/sum.test.ma (modified)
	* src/Cminor/toRTLabs.ma (modified)
	* src/compiler.ma (modified)

	Cminor to RTLabs is now a total function.


Wed, 18 Jul 2012 10:27:01 GMT campbell [2205]
	* src/LTL/LTLToLIN.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Get correctness.ma type checking again.


Wed, 27 Jun 2012 09:46:36 GMT sacerdot [2116]
	* src/compiler.ma (modified)

	load_code_memory will be moved into Fetch.ma in the next commit. ...


Wed, 06 Jun 2012 16:24:43 GMT campbell [2019]
	* src/Clight/Cexec.ma (modified)
	* src/Clight/CexecInd.ma (added)
	* src/Clight/CexecSound.ma (modified)
	* src/Clight/SimplifyCasts.ma (modified)
	* src/Clight/labelSimulation.ma (modified)
	* src/compiler.ma (modified)

	Split out special induction principle for Clight from soundness file. ...


Fri, 25 May 2012 11:47:32 GMT campbell [2001]
	* src/ASM/ASMCostsSplit.ma (modified)
	* src/ASM/CostsProof.ma (modified)
	* src/compiler.ma (modified)
	* src/correctness.ma (modified)

	Get the compiler to output more.


Thu, 24 May 2012 17:18:35 GMT campbell [1995]
	* src/ERTL/liveness.ma (modified)
	* src/LIN/LINToASM.ma (modified)
	* src/RTL/RTLToERTL.ma (modified)
	* src/RTLabs/RTLabsToRTL.ma (modified)
	* src/compiler.ma (modified)
	* src/joint/TranslateUtils.ma (modified)

	Overall compiler definition; bits and pieces to
	make everything ...


Thu, 24 May 2012 14:24:55 GMT campbell [1991]
	* src/Clight/test/search.c.ma (modified)
	* src/Clight/test/search.test.ma (added)
	* src/compiler.ma (added)

	Put the front end transformations together and make an example use
	it.