portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
116 commits 1 branch 42 tags 18 MiB
Commit graph

49 commits

Author SHA1 Message Date
Adrian Danis
f2ac14f12f arm: Rename BI_CAP_IT_PD to BI_CAP_IT_VSPACE to match x86 and common boot code 2015-02-17 10:44:41 +11:00
Adrian Danis
a5e442a70e Merge branch master into pae 2015-02-17 10:37:33 +11:00
Adrian Danis
d8eadae289 Trivial: style 2015-02-17 10:20:18 +11:00
Adrian Danis
7acfbd7202 am335x: Remove dead code 2015-02-17 10:19:31 +11:00
Tim Newsham
80308386e7 - fix am335x interrupt handling and disable watchdog 2015-02-17 10:15:12 +11:00
Robbie VanVossen
f28eb2c586 Added support for the Allwinner A20 platform (specifically the CubieTruck board) 2015-02-13 10:24:42 -05:00
Adrian Danis
42c93cbe50 ia32: Correct pdpt modifications to reload cr3 as required by the intel manual 2015-02-11 15:05:08 +11:00
Adrian Danis
af0f3b361f ia32: Large commit that implements PAE paging for x86 
This commit involves the PAE paging itself, refactoring the
vspace code to extra what is common between PAE and 32bit paging,
as well as some renaming to not call the root paging structure
a PD
 2015-01-28 12:11:51 +11:00
Matthew Fernandez
3c13124c6a Fix more trivial comment typos. 2015-01-27 11:58:55 +11:00
Matthew Fernandez
84fbc34eb8 IA32: Fix trivial comment typo. 2015-01-27 11:42:32 +11:00
Adrian Danis
14bfc396b2 ia32: Move _boot_pd definition from linker script to C 2015-01-16 11:14:36 +11:00
akroh
d796aa0a22 zynq: Increase kernel window size (start at 0xe0000000) now that the elfloader does not attempt to access the serial port at 0xe0001000 after PD switch 2015-01-07 16:58:33 +11:00
akroh
986de67742 trivial: fix directory listings 2015-01-06 17:58:20 +11:00
akroh
bcdb09d93b Merge exynos debug serial drivers 2015-01-06 17:49:07 +11:00
akroh
98ac528fc7 Zynq7000: split coresite and trustzone device memory blocks 2014-12-18 13:59:23 +11:00
akroh
c685dded5b Trivial: simplify #ifdef logic in L2C310 code 2014-12-18 12:59:56 +11:00
akroh
d46a234a3f Add support for Zynq-7000 2014-12-18 12:29:25 +11:00
Gerwin Klein
f896ffa0cb XN: fix order of vm_attributes in init code and update apq8064 2014-11-27 20:09:52 +11:00
Gerwin Klein
49378220c5 trivial: once more with the style thing 2014-11-27 19:40:16 +11:00
Gerwin Klein
1357984e9f trivial: thank you, astyle. 2014-11-27 17:11:25 +11:00
Gerwin Klein
c9985de0f4 trivial: more style 2014-11-27 17:02:43 +11:00
Adrian Danis
47624ce008 trivial: style 2014-11-27 16:04:50 +11:00
Matthew Fernandez
644dff497b further support for XN bit on ARM 2014-11-26 12:44:06 +11:00
Matthew Fernandez
138e8304e2 trivial: Fix string typos. 2014-11-17 14:33:42 +11:00
Gerwin Klein
3179696494 Merge pull request #38 from mfernandez/trivial 
trivial: Print domain values as unsigned integers in user errors.
 2014-10-22 09:42:49 +11:00
Matthew Fernandez
6d31d46024 trivial: Standardise on 32-bit unsigned variables for domain values. 
Domains are unnecessarily treated explicitly as 8-bit values within boot info.
Though there are existing proof constraints that limit the maximum domain value
to 8 bits, most of the code would permit domain values up to 32 bits. The
maximum value is unnecessarily constrained in boot info, a restriction which
this commit removes.

Closes VER-341
 2014-10-21 13:32:42 +11:00
Matthew Fernandez
edf2d46bc5 trivial: Print domain values as unsigned integers in user errors. 
With the comparison preceding this being done on unsigned integers, this avoids
confusing error messages like '-2147482648 >= 1'.
 2014-10-21 13:00:47 +11:00
Matthew Fernandez
b8ad423d08 Remove some unused #defines. 
Does not affect verification.
 2014-10-20 14:20:16 +11:00
Adrian Danis
04106920c3 Derive a new IPC buffer cap when inserting into the initial threads TCB to remove mapping information 
For any other thread setting the IPC buffer via TCB_Configure will result
in a derived capability being installed that does not have mapping information.
This leads to a expected behaviour that setting a new IPC buffer (even if it is
the same as the current one), will not perform an unmapping.
 2014-10-17 16:01:39 +11:00
Peter Chubb
28eb695464 gic_pl390.c: whitespace changes 
Remove trailing whitespace, and align comments.
 2014-10-16 11:38:35 +11:00
Peter Chubb
735dead468 ARM: port to GIC400 
The gic400 used on the Exynos5 platforms is a little different from
the pl390, and needs a few small changes.
 2014-10-16 09:42:27 +11:00
Adrian Danis
ed39d55d14 trivial: style 2014-10-10 15:14:34 +11:00
Adrian Danis
1aa902e2fb ia32: Handle spurious IRQs correctly on the PIC 2014-10-09 10:22:31 +11:00
Thomas Sewell
97d6bc96d5 Clean up data-flow in resolveVAddr. 
Initialise the 'ret' struct from a constant zero struct to ensure that no
uninitialised data is returned. Returning uninitialized data creates headaches
for binary verification.

This function is inlined in builds I have looked at, and the 'ret' struct is
never built, so this change has zero impact on the binary.
 2014-09-03 15:16:52 +10:00
Joel Beeren
f2a3677d23 ioapic: trivial: style 2014-09-02 16:22:40 +10:00
Joel Beeren
ec5ff930a3 ioapic: reverted setIRQState change 2014-09-02 16:22:40 +10:00
Joel Beeren
3695d22b18 ioapic: refactored C code and first attempt at haskell spec 2014-09-02 16:22:40 +10:00
Adrian Danis
c0e9c63804 Support IOAPIC on ia32 and modify interrupt handling to support user level setting of modes 2014-09-02 16:22:40 +10:00
Thomas Sewell
5d439655bd DONT_TRANSLATE more inline asm functions. 
The c-parser can now parse these functions, but it does it by
discarding the inline ASM block, creating a misleading and likely
malformed function body. It is better to not translate these
with a DONT_TRANSLATE comment.

This change has been made for the current verification platform
only, and should probably be extended to any other verification
targets as necessary.
 2014-09-01 16:58:32 +10:00
Adrian Danis
3d100f43a3 trivial: style 2014-08-12 16:48:18 +10:00
Adrian Danis
7d877465de ia32: Move as much of the interrupt and syscall traps into C as possible 2014-08-12 14:00:28 +10:00
Peter Chubb
2261557ab3 Fix IFC6410 build 
The IFC6410 has too many devices to fit into the bootinfo page.
What is more, some are aligned on half-page boundaries.

Exclude devices on half-page boundaries from the bootinfo device list.
 2014-08-08 13:50:10 +10:00
Adrian Danis
0b64f564e5 arm: Perform additional cache clean to prevent TLB walker loading garbage entries for first user process 2014-08-08 09:30:30 +10:00
Adrian Danis
185f22bc3c Add license header 2014-07-21 09:38:36 +10:00
Gerwin Klein
e62d407c83 Merge branch 'getpaddr' 
Adds new system call page_getaddress.
 2014-07-18 17:37:52 +02:00
Adrian Danis
2732406e98 Recomment of branch getpaddr on release snapshot 2014-07-18 15:14:00 +10:00
Adrian Danis
43e1a215bb arm: Add work around for errata on some Cortex-A15 boards and move errata checking to C code 2014-07-18 11:37:11 +10:00
TrustworthySystems
784a367b37 Release cleanup 2014-07-18 05:10:23 +10:00
TrusthworthySystems
91b7da8625 Release snapshot 2014-07-18 05:03:59 +10:00