aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* CSE3 generate lists of killableDavid Monniaux2020-03-052-1/+5
|
* xget_killsDavid Monniaux2020-03-051-0/+74
|
* just the analysisDavid Monniaux2020-03-053-3/+6
|
* fix MakefileDavid Monniaux2020-03-051-0/+1
|
* more about extraction and linkingDavid Monniaux2020-03-054-185/+190
|
* streamlined lattice codeDavid Monniaux2020-03-054-144/+17
|
* begin CSE3David Monniaux2020-03-051-0/+76
|
* HashedSet with extractionDavid Monniaux2020-03-051-0/+6
|
* HashedSet with module typesDavid Monniaux2020-03-051-0/+115
|
* move lattice stuff where it belongsDavid Monniaux2020-03-054-0/+1446
|
* fix for ppcDavid Monniaux2020-03-031-14/+22
|
* try to get it to compileDavid Monniaux2020-03-031-0/+1
|
* forgot k1CDavid Monniaux2020-03-032-0/+147
|
* fixes for risc-VDavid Monniaux2020-03-031-1/+1
|
* fix for aarch64David Monniaux2020-03-031-11/+9
|
* ported to armDavid Monniaux2020-03-031-9/+6
|
* ported for ppcDavid Monniaux2020-03-031-22/+17
|
* fix for risc-VDavid Monniaux2020-03-031-9/+7
|
* adjust for x86David Monniaux2020-03-031-44/+35
|
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-0324-843/+1266
|\ | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| * CSE2 with alias analysisDavid Monniaux2020-03-031-0/+20
| |
| * CSE2 for powerpcDavid Monniaux2020-03-032-0/+152
| |
| * aarch64David Monniaux2020-03-032-0/+150
| |
| * CSE2 for ARMDavid Monniaux2020-03-031-0/+132
| |
| * better 32/64-bit handlingDavid Monniaux2020-03-032-26/+51
| |
| * CSE2 alias analysis for Risc-VDavid Monniaux2020-03-036-30/+158
| |
| * moved away x86-dependent partsDavid Monniaux2020-03-032-38/+46
| |
| * modularize proofDavid Monniaux2020-03-031-29/+10
| |
| * may_overlap_soundDavid Monniaux2020-03-031-0/+38
| |
| * starting to move x86 stuff to x86David Monniaux2020-03-032-201/+216
| |
| * offsets in globals for x86David Monniaux2020-03-032-2/+82
| |
| * globals alias analysis for x86David Monniaux2020-03-033-10/+67
| |
| * with indexed/indexed alias analysis for x86David Monniaux2020-03-033-4/+32
| |
| * kill_store_soundDavid Monniaux2020-03-021-10/+25
| |
| * kill_store1_soundDavid Monniaux2020-03-021-3/+41
| |
| * load_store_awayDavid Monniaux2020-03-021-1/+2
| |
| * swap predicateDavid Monniaux2020-03-022-13/+27
| |
| * works on x86 x86_64David Monniaux2020-03-021-29/+47
| |
| * playing with offsetsDavid Monniaux2020-03-021-1/+67
| |
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-0269-1230/+1104
| |\
| | * Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
| | | | | | | | | | | | | | | The proof script for Events.excall_free_ok was incomplete if Archi.ptr64 is unknown (as in the RISC-V case).
| | * Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-022-43/+74
| | | | | | | | | | | | | | | | | | | | | | | | According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334
| | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-022-18/+35
| | | | | | | | | | | | | | | | | | | | | | | | Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals.
| | * Documentation comment for single_passed_as_singleXavier Leroy2020-03-021-1/+2
| | |
| | * In strict PPC ABI mode, pass single FP on stack in double FP formatXavier Leroy2020-03-021-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The EABI and the SVR4 ABI state that single-precision FP arguments passed on stack are passed as a 64-bit word, extended to double-precision. This commit implements this behavior by using a stack slot of type Tany64. Not only this ensures that the slot is of size and alignment 8 bytes, but it also ensures that it is accessed by stfd and lfd instructions, using single-extended-to-double format.
| | * Define IRC.class_of_type for types Tany32, Tany64Xavier Leroy2020-03-021-1/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Until now the types Tany32 and Tany64 were not used prior to register allocation, so IRC.class_of_type did not need to be defined for those types. However, there are possible uses of stack slots of type Tany32 and Tany64 to specify calling conventions. For this purpose, we need to define class_of_type for Tany32 and Tany64. We follow the informal convention that Tany32 goes in integer registers and Tany64 goes into integer registers if 64-bit wide, or FP registers otherwise.
| | * Make single arg alignment depend on toolchain.Bernhard Schommer2020-03-023-3/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | GCC does passes single arguments as singles on the stack but diab and the eabi say single arguments should be passed as double on the stack. This commit changes the alignment of single arguments to 4 for gcc based backends.
| * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
| | |
* | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-032176-666/+596149
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * \ \ Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-1451-456/+2436
| |\ \ \
generated by cgit (git 2.34.1) at 2024-07-11 22:25:33 +0000