Commit graph

231 commits

Author SHA1 Message Date
Hesham Almatary
ff8c48d651 Benchmark: ARM - Fix typos in syscalls.h 2017-01-11 12:30:39 +11:00
Stephen Sherratt
c05210f508 manual: Remove empty cap description attribute 2016-12-16 15:57:57 +11:00
Stephen Sherratt
1f1a5ad4dc manual: Removed default cap description 2016-12-16 15:57:57 +11:00
Adrian Danis
55d7a38641 libsel4: seL4_VMEnter syscall for x86-64 2016-12-16 10:39:40 +11:00
Adrian Danis
017d786317 x64: VT-x related cap and object definitions
* Adds object and cap definitions for VT-x structures (VCPU and EPT).
* Extends the asid_map implementation to support ASIDs in the EPT
* Adds size definitions for VCPU and EPT objects
2016-12-16 10:39:40 +11:00
Kent McLeod
e537ee1d67 libsel4: add void to function prototypes 2016-12-15 15:04:44 +11:00
Jeff Waugh
803dd5c2ae libsel4: Optional public symbols for external interfaces
CONFIG_LIB_SEL4_PUBLIC_SYMBOLS=y will disable inlining for external
interfaces (except deprecated functions), thereby providing public
symbols for easy linkage with other languages.
2016-12-06 18:08:39 +11:00
Adrian Danis
80ae3286dc ia32: Support larger XSAVE region sizes 2016-11-30 17:44:24 +11:00
Stephen Sherratt
b6cd9f1227 libsel4: Updated api xml dtd file with doc tags 2016-11-30 16:09:06 +11:00
Adrian Danis
f9f360a747 Merge pull request #552 in SEL4/sel4 from ~ADANIS/sel4:fault to master
* commit '0435985eca5117a9df272e991fd0f8c421515831':
  arm: Use new cap rights structures in iospace
  libsel4: Correct VGIC and VCPU fault types
  libsel4: Correct deprecated macro for in unknown syscall
2016-11-30 14:43:37 +11:00
Stephen Sherratt
a09089292d Merge pull request #551 in SEL4/sel4 from ~SSHERRATT/sel4:caprights to master
* commit '2e30ac481f212b3490fde8dbd13f496a50d70f49':
  libsel4: Add remaining combinations of cap rights
  libsel4: Removed stray semicolon from shared_types
2016-11-30 14:16:22 +11:00
Adrian Danis
78009dd245 SELFOUR-675: x64: Increase message registers from 2 to 4 2016-11-30 12:04:54 +11:00
Adrian Danis
8b0e63f09d libsel4: Correct VGIC and VCPU fault types 2016-11-30 11:59:48 +11:00
Adrian Danis
fe0f417789 libsel4: Correct deprecated macro for in unknown syscall 2016-11-30 11:57:47 +11:00
Stephen Sherratt
2e30ac481f libsel4: Add remaining combinations of cap rights 2016-11-30 10:36:31 +11:00
Stephen Sherratt
3fce021c8b libsel4: Removed stray semicolon from shared_types 2016-11-30 10:35:47 +11:00
Stephen Sherratt
cd8b5de27e manual: Add docs to arch-independent inv xml file
This also moves the description of TCBSetEPTRoot from the general object
invocation xml file to the x86-specific one to prevent the need for
documentation-generating scripts to distinguish between VTX (ie. x86)
invocations, and truly architecture independent invocations.

JIRA: SELFOUR-606
2016-11-29 14:30:41 +11:00
Stephen Sherratt
08bca15c5f manual: Obj inv stub gen generates doxy comments
This modifies the object invocations stub generator to generate doxygen
comments based on documentation in the xml files it parses.

JIRA: SELFOUR-606
2016-11-29 14:30:36 +11:00
Stephen Sherratt
818a8330b3 manual: Added libsel4 tools library to manual dir
JIRA: SELFOUR-606
2016-11-29 14:30:02 +11:00
Stephen Sherratt
891a5eb587 libsel4: Trivial whitespace 2016-11-29 14:06:30 +11:00
Stephen Sherratt
0197d63b6a Replace bools with ints in shared_types header
The motivation for this change is the fact that the types of `true` and
`false` are different between userland and the kernel. This was forcing
code including shared_types.h to first include the appropriate header
defining `true` and `false`. This change prevents this need.
2016-11-28 14:05:23 +11:00
Adrian Danis
db174884e9 libsel4: Add missing seL4_AllRights macro
Left out of commit 2fea9a0fe2
2016-11-25 15:23:45 +11:00
Anna Lyons
ed95f84a43 SELFOUR-413: changes for verification
Avoid using ptrs to arrays at all

Another macrofull change brought to your by verification. This should
avoid nasty proofs about const pointers.
2016-11-25 12:30:29 +11:00
Anna Lyons
2fea9a0fe2 SELFOUR-567: use seL4_CapRights_t from libsel4
This change

* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
  now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4

Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.
2016-11-25 12:29:07 +11:00
Anna Lyons
b827ad37ba SELFOUR-413: refactor libsel4 fault API
This is a *breaking API change*

This commit:

* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
  the user calling seL4_SetTag() first (seL4_MessageInfo is passed
  in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes
2016-11-25 12:29:07 +11:00
Anna Lyons
33a771d3cb Split fault types into arch/generic
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
2016-11-25 12:29:07 +11:00
Adrian Danis
e78cdf9b64 SELFOUR-553: Support alternate IPC buffer locations without globals frame
This commit adds support for using the ThreadID registers of the ARM MPCore
platforms for storing the address of the IPC buffer instead of the globals
frame. The choice of using the user readable/writeable ThreadID register
is chosen, even though it means the user cannot use it for its own
purposes, as it leaves room in the future for doing TLS support in the
user read only register, where compilers expect it.
2016-11-22 11:49:52 +11:00
Adrian Danis
31628d9a58 Remove recycle
Removes the recycle operation and adds an operation
to cancel any badged sends on and endpoint. Calling
Revoke + CancelBadgedSend is equivalent to Recycle
on a badged endpoint
2016-11-18 14:10:01 +11:00
Adrian Danis
05bf1ca44d libsel4: Reorder bootinfo struct
This reorders the bootinfo struct to place the untyped array as the
last element. Having the array at the end makes the layout of the
information in this struct easier to represent in other languages.
2016-11-14 08:58:18 +11:00
Anna Lyons
c86669df43 x86: export tsc freq in bootinfo
We read the frequency from the platform info MSR and export it to the
user for accurate timing (for platforms that support platform into)
2016-11-08 14:46:18 +11:00
Adrian Danis
8d0ed7029d Use correct seL4_MaxUntypedBits
This change uses the seL4_MaxUntypedBits constant in decodeUntypedInvocation
when checking the size of the requested allocation. This constant
is also changed to be the correct value. The verification team suspects
this check is probably unnecessary, but have also resolved not to waste more
time investigating.
2016-11-01 16:17:11 +11:00
Kent Mcleod
436b214ec6 Merge pull request #444 in SEL4/sel4 from ~KMCLEOD/sel4:pr to master
* commit '66dfc2e786614a34c18ad2d7c20c04c69e589a97':
  Change ia32 to use fs register for IPC buffer
2016-10-30 23:00:44 +00:00
Kent McLeod
66dfc2e786 Change ia32 to use fs register for IPC buffer
gs register is used by gcc for TLS and the IPC buffer gets in the way
2016-10-28 16:40:38 +11:00
Adrian Danis
8a49b94893 Merge pull request #446 in SEL4/sel4 from ~ADANIS/sel4:withmrs to master
* commit 'be68b0c0bde5bfa439376fac4c8be255dacaa958':
  libsel4: Allow invocations to not use IPC buffer
  Retain in-register error descriptions when not using IPC buffer
2016-10-28 04:35:09 +00:00
Adrian Danis
be68b0c0bd libsel4: Allow invocations to not use IPC buffer
Reintroduces Kconfig option removed in 5271925ba5
that allows invocations to use the WithMRs variants of syscalls instead of
using the IPC buffer
2016-10-28 15:25:27 +11:00
Anna Lyons
f0cb354755 Merge pull request #410 in SEL4/sel4 from ~ALYONS/sel4:cache to master
* commit '44ed6adb616590a0f6ae8b0ad8c442afed625457':
  add seL4_BenchmarkFlushCaches() for arm and ia32
2016-10-28 04:21:25 +00:00
Anna Lyons
44ed6adb61 add seL4_BenchmarkFlushCaches() for arm and ia32
Available when CONFIG_ENABLE_BENCHMARKS is set, flushes caches for
running cold-cache benchmarks
2016-10-28 15:09:03 +11:00
Jeff Waugh
dc3d53417e Retain in-register error descriptions when not using IPC buffer
- Fixes "lost" error descriptions when using *WithMRs system call
  variants [1].
- Only stores real registers to IPC buffer if there's an error.
- If there's an error in a struct-returning function, return
  early without setting any struct members.
- Passes the sabre/qemu test suite... with and without --buffer!

[1] https://sel4.systems/pipermail/devel/2016-October/001079.html
2016-10-28 14:57:39 +11:00
Adrian Danis
e77d4d48cc Merge pull request #443 in SEL4/sel4 from ~ADANIS/sel4:recvwithmrs to master
* commit '339096d39eee5f85362ff5bbd1fcce7b81bacd71':
  Also let aarch32 seL4_RecvWithMRs/ReplyRecvWithMRs
2016-10-28 03:33:30 +00:00
Adrian Danis
151e95d908 libsel4: Update VTX invocations to use condition= instead of config= 2016-10-28 14:09:28 +11:00
Adrian Danis
654e366f5e libsel4: Update condition for SetEPTRoot
Using `config=` for guarding invocations was changed to be
`condition=`, but `SetEPTRoot` was not updated
2016-10-28 13:58:51 +11:00
Adrian Danis
48f99701c3 libsel4: Move vt-x definitions into common x86 2016-10-28 12:16:41 +11:00
Jeff Waugh
339096d39e Also let aarch32 seL4_RecvWithMRs/ReplyRecvWithMRs 2016-10-28 12:04:15 +11:00
Adrian Danis
7fbde1bbcb SELFOUR-287: 32-bit vt-x implementation
This is an implementation of vt-x for x86 kernels running in
ia32 mode.
2016-10-27 16:20:30 +11:00
Adrian Danis
cb79c0dd97 Merge pull request #437 in SEL4/sel4 from ~ADANIS/sel4:stubgen to master
* commit '59d48b778b6daf50cc612f7bd4f64c9d1bdf2e21':
  Let x86_64 CallWithMRs
2016-10-27 02:54:57 +00:00
Jeff Waugh
59d48b778b Let x86_64 CallWithMRs
* `syscall_stub_gen.py` now works on x86_64 without passing `--buffer`
2016-10-27 12:09:00 +11:00
Jeff Waugh
df1f021cc6 Let aarch32 CallWithMRs
* Initialise the message variables (as per ia32 and x86_64)
* `libsel4` now builds when `syscall_stub_gen.py` is run without `--buffer`
* While simple things appear to work, `sel4test` with aarch32 in qemu is *not* happy:

```
Bootstrapping kernel

Warning: using printf before serial is set up. This only works as your
printf is backed by seL4_Debug_PutChar()
sel4utils_create_object_at_level@mapping.h:22 Should not be called
Ignoring call to sys_rt_sigprocmask
Ignoring call to sys_gettid
sys_tkill assuming self kill
```
2016-10-27 04:39:27 +11:00
Adrian Danis
b90238d089 Replace #pragma once with include guards 2016-10-21 12:05:02 +11:00
Anna Lyons
49f26d5c84 Fix benchmark_debug_syscall_start
The lowest syscall number is -8, which doesnt' fit in 3 bits -> change
to 4.
Also, we were storing the -ve number, which also doesn't fit into 3
bits -> invert it when we store it.
2016-10-20 15:07:49 +11:00
Hesham Almatary
3c01da7018 Trivial: correct x86_64 seL4_BenchmarkReset() return value 2016-10-20 12:14:35 +11:00