Commit graph

840 commits

Author SHA1 Message Date
Adrian Danis
ea9ebc28cc SELFOUR-562: Update caps before calling perform
It is preferable for verification to update the information in a cap,
and pass the updated cap to the perform functions, than to pass all
the information and have the perform function update the cap
2016-07-26 15:38:59 +10:00
Adrian Danis
2399465494 SELFOUR-561: s/ARM_HYP/CONFIG_ARM_HYPERVISOR_SUPPORT/ 2016-07-26 15:31:34 +10:00
Adrian Danis
9d356b1ac7 Remove .arch directive from intermediate build file
Due to limitations in certain compilers in reported architecture
support the kernel needs to be compiled (to assembler) with one
architecture and assembled with another architecture.
Unfortunately when generating the kernel_final.s file the
architecture passed for compilation gets inserted as a '.arch'
directive. This directive overrides the architecture later
passed to the assembler.

This commit is an ugly work around that just strips out any
.arch directives from the assembler file
2016-07-26 10:39:23 +10:00
Hesham Almatary
c4de796da1 Merge pull request #292 in SEL4/sel4 from ~HALMATARY/sel4:fix/ARMHypTraps to master
* commit '3ffa58aa1fb75c65fac4d1351bc6e014bdda2b64':
  Verification: don't translate functions that are re-implemented from assembly to C
  ARM Hyp: Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C
  SELFOUR-526: ARM - Implement slowpath and restore_user_context in C
2016-07-23 04:06:01 +00:00
Hesham Almatary
3ffa58aa1f Verification: don't translate functions that are re-implemented from assembly to C 2016-07-22 17:07:26 +10:00
Adrian Danis
abaf3dfcfb Merge pull request #245 in SEL4/sel4 from ~CRICHARDSON/sel4:configurable-python to master
* commit '9f9bbc5b89fac99c0d5e132ad5ca3dcfa494e4dc':
  SELFOUR-418: Allow overriding python executable used with PYTHON env var
2016-07-22 04:35:24 +00:00
Adrian Danis
9c7f178f9f Merge pull request #274 in SEL4/sel4 from ~MFERNANDEZ/sel4:8dafd43a-daa8-4d38-ad7e-3ac425d50087 to master
* commit 'd36447b35f88705f796e17f47bf9033918fd2ed0':
  Mark strncmp as a pure function.
  Fix: Make VISIBLE expand to nothing for Clang.
2016-07-21 05:03:02 +00:00
Stephen Sherratt
85e70f02e0 Merge pull request #294 in SEL4/sel4 from ~SSHERRATT/sel4:6cff0b6e-92d8-4997-a625-e85f9bf709d9 to master
* commit '91718da4a286f625b4101945abe8f897bd2f9869':
  Fixed clobbered register in Signal syscall stub
2016-07-20 05:24:17 +00:00
Hesham Almatary
778043a73c ARM Hyp: Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C 2016-07-19 15:27:26 +10:00
Stephen Sherratt
91718da4a2 Fixed clobbered register in Signal syscall stub 2016-07-19 14:20:04 +10:00
Hesham Almatary
5bd5d9cfca SELFOUR-526: ARM - Implement slowpath and restore_user_context in C 2016-07-18 10:54:59 +10:00
Kofi Doku Atuah
56030fc3cc x86: Fix cpuid family/model composition
Fixes a bug where previously MODEL_ID() was defined as:
    `#define MODEL_ID(x) ( ((x & 0xf0000) >> 16) + (x & 0xf0) )`

This was incorrect because (1) it didn't take into account the conditional
nature of the extended_model_ID, and (2) it's actually shifting the
extended_model_ID into the low bits and keeping the model_ID in the high bits,
when it should be the other way around.

This patch also introduces a foundation for more sane testing of CPU vendor,
family, model and brand_ID.
2016-07-15 17:12:25 +10:00
Hesham Almatary
d97603bd84 SELFOUR-566: Decouble seL4_DebugNameThread from CONFIG_PRINTING 2016-07-15 12:30:17 +10:00
Partha Susarla
4f5ad9d8f3 Merge branch 'master' of ssh://bitbucket.keg.ertos.in.nicta.com.au:7999/sel4/seL4 2016-07-13 17:54:46 +10:00
Partha Susarla
8e02adc344 update VERSION file to 3.2.0-dev 2016-07-13 17:31:47 +10:00
Partha Susarla
e70cd7613b update VERSION file to 3.2.0 2016-07-13 17:31:47 +10:00
Anna Lyons
bb4bda4b7f Merge pull request #286 in SEL4/sel4 from ~ALYONS/sel4:29e0070 to master
* commit '69f140a2268532523b4f52f26d2692963e61b468':
  trivial: remove duplicated setMRs_syscall_error
2016-07-13 01:33:13 +00:00
Hesham Almatary
62b8cf1eea Merge pull request #287 in SEL4/sel4 from ~HALMATARY/sel4:astyle2.04 to master
* commit '2f163e27b7f7a95a63f0f1c9d1d64c069036243b':
  astyle: Make comments compatible with both 2.03 and 2.04 astyle versions
2016-07-12 05:32:20 +00:00
Hesham Almatary
2f163e27b7 astyle: Make comments compatible with both 2.03 and 2.04 astyle versions 2016-07-12 14:54:28 +10:00
Anna Lyons
69f140a226 trivial: remove duplicated setMRs_syscall_error 2016-07-12 14:44:14 +10:00
Hesham Almatary
11916d7601 Merge pull request #278 in SEL4/sel4 from ~HALMATARY/sel4:UnifiedCEntry to master
* commit 'cee1268e9bf9619b60bd85cfda0a5d5306e8cf8a':
  [VER-619] Pass verification related to newly added built-in unreachable
  SELFOUR-545: x86 - cleanup c_traps.c file and use new traps.h
  SELFOUR-526: ARM - dummy unreachable statements after fastpath calls
  SELFOUR-526: ARM - Unify C entry point for system calls
2016-07-12 04:37:44 +00:00
Alejandro Gomez-Londono
cee1268e9b [VER-619] Pass verification related to newly added built-in unreachable 2016-07-12 14:32:47 +10:00
Adrian Danis
2b3a305ef8 SELFOUR-560: Remove unused io_page_directory cap 2016-07-08 16:55:33 +10:00
Adrian Danis
c50926b505 SELFOUR-559: Cleanup ARMPageUnmap for IO mappings
This commit moves setThreadState outside the 'perform' stage of the
invocation, and renames decodeARMIOUnmapInvocation to
performPageInvocationUnmapIO as it is actually doing a perform
and not a decode
2016-07-08 16:50:08 +10:00
Adrian Danis
5ca374b34c SELFOUR-558: Consistently name Unmap instead of UnMap 2016-07-08 16:27:02 +10:00
Adrian Danis
75299d05a9 SELFOUR-557: s/isIOSpaceFrame/isIOSpaceFrameCap/ 2016-07-08 16:17:09 +10:00
Adrian Danis
a4ed36a404 SELFOUR-555: Rename ksCurCPU->armHSCurVCPU 2016-07-08 15:38:33 +10:00
Adrian Danis
382dc2d60e SELFOUR-554: Update archCapIsPhysical
VCPU and IO page table caps were not added to archCapisPhysical,
this commit fixes that and marks them as physical objects
2016-07-08 15:38:33 +10:00
Adrian Danis
9bedaaa873 SELFOUR-552: Translate IO-ASIDs->PDs by table
Previously looking up the page directory base for a SysteMMU was
done by writing the ASID into the hardware and reading out the
currently set page directory for that ASID. This is confusing for
verification so this commit introduces a global translation table
for converting an ASID to a page directory.
2016-07-08 15:38:33 +10:00
Hesham Almatary
f9ea6383f3 SELFOUR-545: x86 - cleanup c_traps.c file and use new traps.h
Closes SELFOUR-545
2016-07-08 10:39:17 +10:00
Adrian Danis
4d43172292 Makefile: Prevent macro redefinition warning
These defines were added to the Makefile so that standalone debug builds
would have printing/debug support. However, in the case of a non standalone
kernel build these are redefinitions, which is fine except for
CONFIG_USER_STACK_TRACE_LENGTH, which is possibly getting defined as
something different reuslting in a compilation warning.

This commit moves these definitions to open occur if a standalone
build is actually happening.
2016-07-07 16:27:58 +10:00
Adrian Danis
edefda5352 Merge pull request #280 in SEL4/sel4 from ~ADANIS/sel4:stubgen to master
* commit '9fc8194b1f89a0cb0f73cce32d413248a587e9d2':
  fix "syscall_stub_gen.py --word-size" invocation
2016-07-06 23:35:06 +00:00
Alexander Boettcher
9fc8194b1f fix "syscall_stub_gen.py --word-size" invocation
Fixes #29
2016-07-06 16:03:58 +02:00
Adrian Danis
3f099700c3 Merge pull request #225 in SEL4/sel4 from ~CRICHARDSON/sel4:SELFOUR-299 to master
* commit '319183597e862d8130428dbbf802da3ea448a576':
  SELFOUR-229: add error condition for root task overlapping kernel window on ARM
2016-07-06 07:38:31 +00:00
Adrian Danis
4deaadd27d Merge pull request #279 in SEL4/sel4 from ~ADANIS/sel4:bda to master
* commit 'f3ee45cc0aa36005bb2bcb3867c17587998743d9':
  x86: Add link explaining BDA
  x86: read default serial configuration from BDA
2016-07-06 06:27:52 +00:00
Adrian Danis
f3ee45cc0a x86: Add link explaining BDA 2016-07-06 14:34:28 +10:00
Hesham Almatary
7c7fd1bc65 SELFOUR-526: ARM - dummy unreachable statements after fastpath calls 2016-07-06 11:11:52 +10:00
Hesham Almatary
39c692cc35 SELFOUR-526: ARM - Unify C entry point for system calls 2016-07-06 10:32:26 +10:00
Alexander Boettcher
d95f10a416 x86: read default serial configuration from BDA
BDA - BiosDataArea

Fixes #28
2016-07-05 15:33:55 +02:00
Adrian Danis
082882449f Merge branch 'master' of https://github.com/zhicheng/seL4 into master 2016-07-05 09:28:06 +10:00
Anna Lyons
ffc15e95bb SELFOUR-436: libsel4 s/__SWINUM/__SEL4_SWINUM
Namespace the definition and do not #undef.
2016-07-01 12:16:02 +10:00
Matthew Fernandez
d36447b35f Mark strncmp as a pure function.
Simply a performance optimisation. This has no effect on functional behaviour.
2016-06-29 17:04:28 +10:00
Matthew Fernandez
fee3af3dd3 Fix: Make VISIBLE expand to nothing for Clang.
The `VISIBLE` macro is designed to selectively inhibit the effects of GCC's
whole program and link-time optimisations. This is necessary when a C function
is only referenced from a context outside the compiler's visibility, e.g. an
assembly file. As far as I can determine, Clang's link-time optimisations
already account for this possibility and do not need to have this information
manually indicated to them (see, for example, Linux's compiler support headers).

In any event, `__attribute__((visibility("default")))` is not equivalent to
`__attribute__((externally_visible))`, but is instead for controlling symbol
visibility in a library-like setting. This commit removes this incorrect
expansion.
2016-06-29 16:58:47 +10:00
Adrian Danis
7a2ede80f8 Merge pull request #272 in SEL4/sel4 from ~JALIM/sel4:master to master
* commit 'fa63ab738fe5cf00865807f0cb1dd1fc74b32863':
  Add -nostdinc to CPPFLAGS
2016-06-29 06:37:25 +00:00
Adrian Danis
dbc9ae3f4c README.md: Update README for serial output 2016-06-27 09:41:45 +10:00
Adrian Danis
8082f7cb37 README.md: Update README for verified platform 2016-06-27 09:41:45 +10:00
Adrian Danis
3afa45a83a Makefile: Remove linker.lds_pp on clean
When changing platforms if this file is not removed make is unable
to realize that it should be rebuilt.
2016-06-27 09:41:45 +10:00
Rafal Kolanski
234c9fefce Merge pull request #271 in SEL4/sel4 from ~ADANIS/sel4:stdbool to master
* commit 'e450377a6f26ba4a32dd0e6535c8b472bae9faff':
  Remove #include <stdbool.h>
2016-06-24 16:41:43 +00:00
Japheth Lim
fa63ab738f Add -nostdinc to CPPFLAGS
CFLAGS already contains -nostdinc but this was forgotten for CPPFLAGS.
2016-06-24 16:22:56 +10:00
Adrian Danis
e450377a6f Remove #include <stdbool.h>
seL4 has no stdbool.h and #including this is simply causing gcc to
pull in some 'random' stdbool outside of our control
2016-06-24 15:05:44 +10:00