8ee20e572a
ignore C parser test files in license check
2017-04-28 20:39:47 +10:00
4a5fa29b23
x64: add CI test setup
2017-04-28 20:17:36 +10:00
23057ee017
x64 refine: add a RefineOnly image which skips Orphanage
2017-04-24 23:58:05 +10:00
2c742ed2c6
x64 refine: fix proofs after rebase and spec updates
2017-04-24 23:58:05 +10:00
d4fc2de959
x64 design: run Haskell translator
2017-04-24 23:58:05 +10:00
3c84f2ade3
x64 haskell: check capVPIsDevice in checkValidIPCBuffer
2017-04-24 23:58:05 +10:00
ff5efcd2da
x64 abstract: make invalidate_asid_entry take a bare vspace pointer
2017-04-24 23:58:04 +10:00
110a2bf354
x64 haskell: make invalidateASID take a bare vspace pointer
...
Previously, this took a PAddr, but the C kernel and abstract specs
take kernel virtual addresses.
Similar for hwASIDInvalidate, flushAll, flushPD and flushPDPT.
2017-04-24 23:57:07 +10:00
1a3debd78e
x64: refine: clear sorries for setVMRoot
2017-04-24 15:44:36 +10:00
2652a7d773
x64: refine: proved perform_aci_invs
2017-04-24 14:46:12 +10:00
fe26c457d3
x64 refine: fix findVSpaceForASID_vs_at_wp
2017-04-24 14:36:56 +10:00
c01e9f68c6
x64: progress in VSpace_R
...
Corres lemmas are proven. Remaining:
- A handfull of Hoare triples.
- The Haskell spec for invalidateASID needs to be updated
to close a small hole in each of unmap_pd_corres and
unmap_pdpt_corres.
2017-04-24 13:58:37 +10:00
990b6a02df
x64: cleared sorries in Detype_R
2017-04-24 12:11:39 +10:00
96abdfbfe7
x64: haskell: use VMNoMap in createObject rather than VMVspaceMap
2017-04-24 12:11:09 +10:00
04d102608a
x64: ainvs: fix broken proofs from strengthening of wellformed_pde et al
2017-04-21 17:17:21 +10:00
3b8d91161b
x64: add RefineQD image with quick and dirty, without Orphanage
2017-04-21 14:33:21 +10:00
93f6029fbf
x64: refine: Refine.thy fixed again
2017-04-21 14:32:53 +10:00
3b2c465497
x64: refine: KernelInit_R done
2017-04-21 14:25:48 +10:00
1463da973f
x64: refine: EmptyFail_H done
2017-04-21 14:25:03 +10:00
84f827a042
x64: refine: Refine.thy done
2017-04-21 14:15:56 +10:00
9c10fde9f7
x64: refine: PageTableDuplicates done
2017-04-21 14:01:56 +10:00
8cd3ae5389
x64: refine: DomainTime_R done
2017-04-21 13:37:09 +10:00
c0296a7bf1
x64: refine: ADT_H done
2017-04-21 13:33:06 +10:00
4a09859592
x64: ainvs: strengthen wellformed_pde et al
2017-04-21 13:32:52 +10:00
35f147d3fa
x64: refine: Syscall_R done
2017-04-21 10:49:24 +10:00
0ce6a7da88
x64: refine: finished sorries in Arch_R
2017-04-20 16:56:51 +10:00
cfed54fcf2
x64: haskell translator
2017-04-20 16:56:17 +10:00
6cb31009f1
x64: readd checkPTAt et al to lookup functions
2017-04-20 16:56:04 +10:00
d725084ae6
x64: refine: Arch_R done with sorries
2017-04-20 14:38:45 +10:00
ae33842a66
x64: haskell translator
2017-04-20 14:38:10 +10:00
d59915630c
x64: add IOPort function bodies to skel files
2017-04-20 14:38:00 +10:00
993ab453ab
x64: more caseconvs
2017-04-20 14:37:19 +10:00
32d0014c2d
x64: haskell: fix up decode invocation functions
2017-04-20 14:37:07 +10:00
64fa273221
x64: ainvs: fix proofs after arch_decode_invocation refactor, add more to valid_cap for IOPorts
2017-04-20 14:36:28 +10:00
c67da43bd2
x64: refactor arch_decode_invocation, minor tweaks for refine
2017-04-20 14:35:53 +10:00
991fa244e4
x64: refine: Untyped_R done
2017-04-13 16:11:07 +10:00
774570483e
x64: refine: fix sameRegionAs_def2
2017-04-13 15:39:45 +10:00
98160a2085
x64: abstract: fix up arch_data_to_obj_type definition
2017-04-13 15:39:22 +10:00
1b46cb1379
x64: refine: Detype_R done with some sorries
2017-04-12 18:14:45 +10:00
1696932ad2
x64: refine: readd VSpace_R to Retype_R imports
2017-04-12 18:14:32 +10:00
73cf43d8c3
x64: make word lemmas arch agnostic-ish
2017-04-12 18:10:13 +10:00
c12e8f44a8
x64: haskell translator
2017-04-12 18:01:47 +10:00
98f81bfd8e
x64: haskell: update cteSizeBits et al - these should be arch split
2017-04-12 18:01:33 +10:00
2c9aa53c6b
x64: refine: Tcb_R done
2017-04-12 13:45:21 +10:00
1b695685b6
x64: haskell translator
2017-04-12 13:45:00 +10:00
7bad3f3ab1
x64: haskell: fix checkValidIPCBuffer
2017-04-12 13:44:51 +10:00
ae5d190220
x64: refine: CNodeInv_R done
2017-04-12 11:20:48 +10:00
ac7232326c
x64: refine: Interrupt_R done
2017-04-11 18:48:40 +10:00
a9e8518c1d
x64: abstract: minor tweak to throws in arch_decode_irq_control_invocation
2017-04-11 18:37:30 +10:00
3935de8050
x64: haskell translator
2017-04-11 18:36:46 +10:00
Gerwin Klein
Matthew Brecknell
Joel Beeren