muen/tau0.git
21 months agoAdd explicit proof target master
Adrian-Ken Rueegsegger [Fri, 5 Jul 2019 15:22:28 +0000 (17:22 +0200)]
Add explicit proof target

This can be used to perform Tau0 proofs. They are not performed by
default since it may take a while.

21 months agoAdd Arcanist project file
Adrian-Ken Rueegsegger [Fri, 5 Jul 2019 13:46:55 +0000 (15:46 +0200)]
Add Arcanist project file

21 months agoMove test files to data directory
Adrian-Ken Rueegsegger [Fri, 5 Jul 2019 13:30:46 +0000 (15:30 +0200)]
Move test files to data directory

21 months agoImplement README comments
Johannes Osterholzer [Fri, 5 Jul 2019 12:36:57 +0000 (14:36 +0200)]
Implement README comments

21 months agoREADME: Assorted minor changes
Johannes Osterholzer [Tue, 2 Jul 2019 12:53:15 +0000 (14:53 +0200)]
README: Assorted minor changes

21 months agoREADME: Make subsection 'Invariant Preservation' clearer
Johannes Osterholzer [Tue, 2 Jul 2019 12:54:08 +0000 (14:54 +0200)]
README: Make subsection 'Invariant Preservation' clearer

21 months agoREADME: Update section 'Compilation'
Johannes Osterholzer [Tue, 2 Jul 2019 12:52:31 +0000 (14:52 +0200)]
README: Update section 'Compilation'

21 months agoREADME: Explain why memory region tables are not unmapped
Johannes Osterholzer [Tue, 2 Jul 2019 12:51:26 +0000 (14:51 +0200)]
README: Explain why memory region tables are not unmapped

21 months agoDebug: Add explicit elaboration pragma
Johannes Osterholzer [Tue, 2 Jul 2019 11:45:33 +0000 (13:45 +0200)]
Debug: Add explicit elaboration pragma

This fixes a compile error with GNAT Pro 19.0 (20181010-73), which
inserts an implicit "pragma Elaborate_All", leading to an elaboration
circle.

21 months agoFurther streamline naming of device domain XML commands
Johannes Osterholzer [Tue, 2 Jul 2019 09:36:17 +0000 (11:36 +0200)]
Further streamline naming of device domain XML commands

21 months agoPartially include test.xml in README
Reto Buerki [Tue, 2 Jul 2019 08:40:15 +0000 (10:40 +0200)]
Partially include test.xml in README

To illustrate how a command stream looks like.

21 months agoMinor cleanup in test.xml
Reto Buerki [Tue, 2 Jul 2019 08:38:55 +0000 (10:38 +0200)]
Minor cleanup in test.xml

21 months agoEnable exception backtraces
Reto Buerki [Wed, 26 Jun 2019 09:46:47 +0000 (11:46 +0200)]
Enable exception backtraces

21 months agoIncrease config constants
Reto Buerki [Mon, 24 Jun 2019 13:48:54 +0000 (15:48 +0200)]
Increase config constants

Required to build muen-ts system.

21 months agoDebug: Init log-level from Command_Line getter
Reto Buerki [Thu, 13 Jun 2019 10:17:31 +0000 (12:17 +0200)]
Debug: Init log-level from Command_Line getter

21 months agoImplement log-level command line handling
Reto Buerki [Thu, 13 Jun 2019 10:08:55 +0000 (12:08 +0200)]
Implement log-level command line handling

21 months agoAdd log message before command processing
Reto Buerki [Thu, 13 Jun 2019 09:53:30 +0000 (11:53 +0200)]
Add log message before command processing

Indicate to the user that this could take a while.

21 months agoSet default log-level to Notice
Reto Buerki [Thu, 13 Jun 2019 09:51:51 +0000 (11:51 +0200)]
Set default log-level to Notice

21 months agoSet some log messages to Notice log-level
Reto Buerki [Thu, 13 Jun 2019 09:49:34 +0000 (11:49 +0200)]
Set some log messages to Notice log-level

21 months agoOutput error log messages on command failure
Reto Buerki [Thu, 13 Jun 2019 09:35:50 +0000 (11:35 +0200)]
Output error log messages on command failure

Use log-level Error for this.

21 months agoMove Current_Level variable to Debug spec
Reto Buerki [Thu, 13 Jun 2019 09:34:37 +0000 (11:34 +0200)]
Move Current_Level variable to Debug spec

Allows to query the current level.

21 months agoAdd new Notice loglevel
Reto Buerki [Thu, 13 Jun 2019 09:33:22 +0000 (11:33 +0200)]
Add new Notice loglevel

21 months agoSet Exec_Dir to bin
Reto Buerki [Tue, 11 Jun 2019 13:52:05 +0000 (15:52 +0200)]
Set Exec_Dir to bin

21 months agoUse obj as Object_Dir
Reto Buerki [Tue, 11 Jun 2019 13:50:45 +0000 (15:50 +0200)]
Use obj as Object_Dir

21 months agoWrap calls with $(E) wrapper
Reto Buerki [Tue, 11 Jun 2019 13:43:18 +0000 (15:43 +0200)]
Wrap calls with $(E) wrapper

21 months agoRemove generated directory in clean target
Reto Buerki [Tue, 11 Jun 2019 13:37:23 +0000 (15:37 +0200)]
Remove generated directory in clean target

21 months agoDrop obsolete resolve.xsl file
Reto Buerki [Tue, 11 Jun 2019 13:24:57 +0000 (15:24 +0200)]
Drop obsolete resolve.xsl file

21 months agoUse RESOLVE_XSL variable from Muen Makeconf
Reto Buerki [Tue, 11 Jun 2019 13:24:45 +0000 (15:24 +0200)]
Use RESOLVE_XSL variable from Muen Makeconf

21 months agoDrop obsolete xml2ada script
Reto Buerki [Tue, 11 Jun 2019 13:11:30 +0000 (15:11 +0200)]
Drop obsolete xml2ada script

21 months agoUse XML2ADA variable from Muen Makeconf
Reto Buerki [Tue, 11 Jun 2019 13:11:07 +0000 (15:11 +0200)]
Use XML2ADA variable from Muen Makeconf

21 months agoUse BUILD_OPTS variable in BUILD target
Reto Buerki [Tue, 11 Jun 2019 13:06:37 +0000 (15:06 +0200)]
Use BUILD_OPTS variable in BUILD target

21 months agoInclude Muen Makeconf
Reto Buerki [Tue, 11 Jun 2019 13:05:12 +0000 (15:05 +0200)]
Include Muen Makeconf

Use SPARK_OPTS to define customized SPARK2014_OPTS.

21 months agoMove Active flag of EPT PTEs to bit 52
Adrian-Ken Rueegsegger [Wed, 12 Jun 2019 15:51:31 +0000 (17:51 +0200)]
Move Active flag of EPT PTEs to bit 52

Since EPT PTs are reused for Intel VT-d we cannot use bit 11 since that
is actually used by the IOMMU (Snoop control). Use a bit which is
ignored by EPT as well as Intel VT-d.

21 months agoMinor optimization to XML.Command_Size
Adrian-Ken Rueegsegger [Tue, 11 Jun 2019 13:56:15 +0000 (15:56 +0200)]
Minor optimization to XML.Command_Size

Only get count when actually used. This saves around half a second when
processing the Demo System VT-d/Lenovo T480s.

21 months agoIncrease Max_IRQs_Per_Subject from 8 to 48
Reto Buerki [Wed, 15 May 2019 09:06:09 +0000 (11:06 +0200)]
Increase Max_IRQs_Per_Subject from 8 to 48

21 months agoIncrease Max_Devices_Per_Subject from 8 to 16
Reto Buerki [Wed, 15 May 2019 07:34:58 +0000 (09:34 +0200)]
Increase Max_Devices_Per_Subject from 8 to 16

21 months agoIncrease Max_IRQs_Per_Device to 36
Reto Buerki [Mon, 13 May 2019 08:53:08 +0000 (10:53 +0200)]
Increase Max_IRQs_Per_Device to 36

E.g. the NVMe controller of the Lenovo T480s has 33 IRQs.

21 months agoData.Processors: Check that APIC IDs are pairwise distinct
Johannes Osterholzer [Tue, 25 Jun 2019 13:38:00 +0000 (15:38 +0200)]
Data.Processors: Check that APIC IDs are pairwise distinct

21 months agoCommand_Line: Remove parameter 'cpu-count'
Johannes Osterholzer [Tue, 25 Jun 2019 13:27:36 +0000 (15:27 +0200)]
Command_Line: Remove parameter 'cpu-count'

21 months agoAmend test.xml
Johannes Osterholzer [Tue, 25 Jun 2019 13:26:03 +0000 (15:26 +0200)]
Amend test.xml

21 months agoImplement command Add_Processor
Johannes Osterholzer [Tue, 25 Jun 2019 13:25:43 +0000 (15:25 +0200)]
Implement command Add_Processor

21 months agoUse Data.Processors
Johannes Osterholzer [Tue, 25 Jun 2019 13:23:50 +0000 (15:23 +0200)]
Use Data.Processors

21 months agoRemove outdated FIXME
Johannes Osterholzer [Tue, 25 Jun 2019 12:03:13 +0000 (14:03 +0200)]
Remove outdated FIXME

21 months agoAmend test.xml
Johannes Osterholzer [Tue, 18 Jun 2019 09:16:23 +0000 (11:16 +0200)]
Amend test.xml

21 months agoAdd parameter 'Level' to command 'Create_Device_Domain'
Johannes Osterholzer [Tue, 18 Jun 2019 09:15:47 +0000 (11:15 +0200)]
Add parameter 'Level' to command 'Create_Device_Domain'

21 months agoAmend test.xml
Johannes Osterholzer [Tue, 18 Jun 2019 08:53:21 +0000 (10:53 +0200)]
Amend test.xml

21 months agoAdd parameter 'ID' to command 'Create_Device_Domain'
Johannes Osterholzer [Tue, 18 Jun 2019 08:48:40 +0000 (10:48 +0200)]
Add parameter 'ID' to command 'Create_Device_Domain'

21 months agoCommands.Write_Image: Limit warnings pragma
Johannes Osterholzer [Wed, 12 Jun 2019 14:41:03 +0000 (16:41 +0200)]
Commands.Write_Image: Limit warnings pragma

21 months agoFix whitespace and alignment
Johannes Osterholzer [Wed, 12 Jun 2019 14:40:13 +0000 (16:40 +0200)]
Fix whitespace and alignment

21 months agoSet non-zero exit status on command failure
Reto Buerki [Wed, 12 Jun 2019 08:29:29 +0000 (10:29 +0200)]
Set non-zero exit status on command failure

21 months agoFix warnings reported by -gnatyt
Reto Buerki [Tue, 11 Jun 2019 13:47:31 +0000 (15:47 +0200)]
Fix warnings reported by -gnatyt

21 months agoEnable -gnatyt switch
Reto Buerki [Tue, 11 Jun 2019 13:49:17 +0000 (15:49 +0200)]
Enable -gnatyt switch

21 months agoFix alignment in tau0.gpr file
Reto Buerki [Tue, 11 Jun 2019 13:48:42 +0000 (15:48 +0200)]
Fix alignment in tau0.gpr file

21 months agoXML.*.Map_Pages: Honor value of parameter Base_Offset
Johannes Osterholzer [Wed, 12 Jun 2019 14:09:02 +0000 (16:09 +0200)]
XML.*.Map_Pages: Honor value of parameter Base_Offset

21 months agoAdd XML commands 'mapDevicePagesSubject' and 'mapDevicePagesKernel'
Johannes Osterholzer [Wed, 12 Jun 2019 13:59:03 +0000 (15:59 +0200)]
Add XML commands 'mapDevicePagesSubject' and 'mapDevicePagesKernel'

21 months agoUse buffering in Files.Read_Word64
Johannes Osterholzer [Mon, 27 May 2019 13:52:47 +0000 (15:52 +0200)]
Use buffering in Files.Read_Word64

21 months agoBounded_Table: Add postcondition for Model
Johannes Osterholzer [Mon, 27 May 2019 12:40:45 +0000 (14:40 +0200)]
Bounded_Table: Add postcondition for Model

21 months agoCommand_Stream.XML: Set explicit range for Index_Type
Johannes Osterholzer [Mon, 27 May 2019 12:09:29 +0000 (14:09 +0200)]
Command_Stream.XML: Set explicit range for Index_Type

21 months agoFile.Read_Word64: Pad with zeroes
Johannes Osterholzer [Mon, 27 May 2019 12:07:55 +0000 (14:07 +0200)]
File.Read_Word64: Pad with zeroes

21 months agoAdd XML commands 'mapPagesKernel' and 'mapPagesDeviceDomain'
Johannes Osterholzer [Mon, 27 May 2019 11:09:58 +0000 (13:09 +0200)]
Add XML commands 'mapPagesKernel' and 'mapPagesDeviceDomain'

21 months agoTypes.Page_Table.EPT: Set IPAT only for leaf page tables
Johannes Osterholzer [Mon, 27 May 2019 09:31:45 +0000 (11:31 +0200)]
Types.Page_Table.EPT: Set IPAT only for leaf page tables

21 months agoTypes.Page_Table: Set caching type only for leaf page tables
Johannes Osterholzer [Mon, 27 May 2019 09:28:06 +0000 (11:28 +0200)]
Types.Page_Table: Set caching type only for leaf page tables

21 months agoAdd_Mapping: Supply caching type of memory regions and devices
Johannes Osterholzer [Mon, 27 May 2019 08:48:26 +0000 (10:48 +0200)]
Add_Mapping: Supply caching type of memory regions and devices

21 months agoCommand_Stream: Use File.Read_Word64
Johannes Osterholzer [Mon, 27 May 2019 07:55:44 +0000 (09:55 +0200)]
Command_Stream: Use File.Read_Word64

21 months agoImplement Files.Read_Word64
Johannes Osterholzer [Mon, 27 May 2019 07:55:06 +0000 (09:55 +0200)]
Implement Files.Read_Word64

21 months agotest.xml: Fix tabs
Johannes Osterholzer [Fri, 24 May 2019 11:31:41 +0000 (13:31 +0200)]
test.xml: Fix tabs

21 months agotest.xml: Specify page access rights
Johannes Osterholzer [Fri, 24 May 2019 11:30:07 +0000 (13:30 +0200)]
test.xml: Specify page access rights

21 months agoSupply page access rights in commands 'mapDevicePage*'
Johannes Osterholzer [Fri, 24 May 2019 11:27:58 +0000 (13:27 +0200)]
Supply page access rights in commands 'mapDevicePage*'

21 months agoAdapt test.xml to changed command names
Johannes Osterholzer [Fri, 24 May 2019 11:10:14 +0000 (13:10 +0200)]
Adapt test.xml to changed command names

21 months agoStreamline naming of device domain XML commands
Adrian-Ken Rueegsegger [Thu, 23 May 2019 16:29:33 +0000 (18:29 +0200)]
Streamline naming of device domain XML commands

21 months agoAmend test.xml with examples for '*_Pages_*' commands
Johannes Osterholzer [Fri, 24 May 2019 11:03:49 +0000 (13:03 +0200)]
Amend test.xml with examples for '*_Pages_*' commands

21 months agoAdd and process XML command 'mapPagesSubject'
Johannes Osterholzer [Fri, 24 May 2019 11:03:06 +0000 (13:03 +0200)]
Add and process XML command 'mapPagesSubject'

21 months agoAdd and process XML command 'activatePagesMR'
Johannes Osterholzer [Fri, 24 May 2019 10:50:12 +0000 (12:50 +0200)]
Add and process XML command 'activatePagesMR'

21 months agoAdd and process XML commands 'appendPages*'
Johannes Osterholzer [Fri, 24 May 2019 09:41:56 +0000 (11:41 +0200)]
Add and process XML commands 'appendPages*'

21 months agoAdd and process XML command 'clearPages'
Johannes Osterholzer [Fri, 24 May 2019 08:46:07 +0000 (10:46 +0200)]
Add and process XML command 'clearPages'

21 months agoCommand_Stream: Generate commands from XML node lazily
Johannes Osterholzer [Fri, 24 May 2019 08:28:13 +0000 (10:28 +0200)]
Command_Stream: Generate commands from XML node lazily

Instead of returning a (fixed-size) buffer, the caller provides an
index.  This allows generating a dynamic number of commands from one
XML node.

21 months agoData.Devices.Writers: Rectify postcondition
Johannes Osterholzer [Fri, 24 May 2019 07:17:25 +0000 (09:17 +0200)]
Data.Devices.Writers: Rectify postcondition

21 months agoAdd ghost function 'Page.Within (Address, Base, Length)'
Johannes Osterholzer [Fri, 24 May 2019 07:16:46 +0000 (09:16 +0200)]
Add ghost function 'Page.Within (Address, Base, Length)'

21 months agoRemove unused Proof_In 'Typization_State'
Johannes Osterholzer [Fri, 24 May 2019 06:58:54 +0000 (08:58 +0200)]
Remove unused Proof_In 'Typization_State'

21 months agoData.Memory.Paging: Fix inferred global annotations
Johannes Osterholzer [Fri, 24 May 2019 06:37:25 +0000 (08:37 +0200)]
Data.Memory.Paging: Fix inferred global annotations

21 months agoRename package 'Verification' to 'Page', add function 'Within'
Johannes Osterholzer [Thu, 23 May 2019 14:27:22 +0000 (16:27 +0200)]
Rename package 'Verification' to 'Page', add function 'Within'

... for nicer contracts

21 months agoData.Memory.Paging: Prove preservation of Roots.Invariant
Johannes Osterholzer [Thu, 23 May 2019 11:36:24 +0000 (13:36 +0200)]
Data.Memory.Paging: Prove preservation of Roots.Invariant

21 months agoAdd axiom Full_Typization_Page
Johannes Osterholzer [Thu, 23 May 2019 11:36:03 +0000 (13:36 +0200)]
Add axiom Full_Typization_Page

21 months agoData.Memory.Paging: Add assertion to facilitate proof
Johannes Osterholzer [Thu, 23 May 2019 11:33:27 +0000 (13:33 +0200)]
Data.Memory.Paging: Add assertion to facilitate proof

21 months agoData.Roots: Add Lemma_Invariant
Johannes Osterholzer [Thu, 23 May 2019 11:32:17 +0000 (13:32 +0200)]
Data.Roots: Add Lemma_Invariant

21 months agoData.Memory.Add_*_Block: Add invariant to contract
Johannes Osterholzer [Thu, 23 May 2019 11:30:26 +0000 (13:30 +0200)]
Data.Memory.Add_*_Block: Add invariant to contract

21 months agoData.Memory.VTd_IOMMU: Fix incorrect contract
Johannes Osterholzer [Thu, 23 May 2019 11:29:49 +0000 (13:29 +0200)]
Data.Memory.VTd_IOMMU: Fix incorrect contract

21 months agoCommands.Setup: Add Roots.Invariant to contracts
Johannes Osterholzer [Thu, 23 May 2019 07:17:24 +0000 (09:17 +0200)]
Commands.Setup: Add Roots.Invariant to contracts

21 months agoData.Memory_Region_Table: Shorten postcondition
Johannes Osterholzer [Wed, 22 May 2019 14:25:12 +0000 (16:25 +0200)]
Data.Memory_Region_Table: Shorten postcondition

The deleted conjuncts are implied by the identity above.

21 months agoData.Roots.Writers: Strengthen some postconditions
Johannes Osterholzer [Wed, 22 May 2019 14:24:19 +0000 (16:24 +0200)]
Data.Roots.Writers: Strengthen some postconditions

21 months agoCommands.Devices: Add Data.Roots.Invariant to contracts
Johannes Osterholzer [Wed, 22 May 2019 14:01:31 +0000 (16:01 +0200)]
Commands.Devices: Add Data.Roots.Invariant to contracts

21 months agoData.Devices.Writers: Add Data.Roots.Invariant to contracts
Johannes Osterholzer [Wed, 22 May 2019 14:01:08 +0000 (16:01 +0200)]
Data.Devices.Writers: Add Data.Roots.Invariant to contracts

21 months agoData.Roots: Add Invariant_Tau0_State
Johannes Osterholzer [Wed, 22 May 2019 14:00:36 +0000 (16:00 +0200)]
Data.Roots: Add Invariant_Tau0_State

... which states that in the setup phase, no roots are created.

21 months agoCommands: Add Memory_Region_Table.Invariant to contracts
Johannes Osterholzer [Wed, 22 May 2019 12:09:22 +0000 (14:09 +0200)]
Commands: Add Memory_Region_Table.Invariant to contracts

21 months agoData.Roots.Writers: Apply Memory_Region_Table.Lemma_Invariant
Johannes Osterholzer [Wed, 22 May 2019 12:09:00 +0000 (14:09 +0200)]
Data.Roots.Writers: Apply Memory_Region_Table.Lemma_Invariant

21 months agoMemory.Paging: State Memory_Region_Table.Invariant
Johannes Osterholzer [Wed, 22 May 2019 12:08:32 +0000 (14:08 +0200)]
Memory.Paging: State Memory_Region_Table.Invariant

21 months agoMemory_Region_Table: Add 'Lemma_Invariant'
Johannes Osterholzer [Wed, 22 May 2019 12:07:30 +0000 (14:07 +0200)]
Memory_Region_Table: Add 'Lemma_Invariant'

Allows to prove that Memory_Region_Table.Invariant is preserved
although Data.Roots.State is modified.

21 months agoMemory.Paging: Honour out-parameter 'Success' in contracts
Johannes Osterholzer [Wed, 22 May 2019 08:46:55 +0000 (10:46 +0200)]
Memory.Paging: Honour out-parameter 'Success' in contracts

21 months agoMove VTd_Tables_Valid to Data.Roots
Johannes Osterholzer [Wed, 22 May 2019 08:23:33 +0000 (10:23 +0200)]
Move VTd_Tables_Valid to Data.Roots

21 months agoRoots.Writers.Assign_Device: Fix proof
Johannes Osterholzer [Wed, 22 May 2019 08:22:02 +0000 (10:22 +0200)]
Roots.Writers.Assign_Device: Fix proof