aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Added builtin for dcbtlsBernhard Schommer2015-09-026-13/+63
| | | | | | THis commit adds a builtin function for the dcbtls instruction. Additionaly it changes the printing of the dcbt and dcbtst instruction to embedded mode and adds support for different address variants.
* Added the gcc builtin prefetch.Bernhard Schommer2015-09-016-0/+25
| | | | | | This commit implements the gcc __builtin_prefetch in a form with all arguments for the powerpc architecture. The resulting instructions are the dcbt and dcbtst instructions in Server Category.
* Merge branch 'new-builtins'Bernhard Schommer2015-09-0193-2597/+4014
|\
| * Upgrade the ARM port to the new builtins.Xavier Leroy2015-08-249-211/+260
| |
| * Improve error reporting in Asmexpand.Xavier Leroy2015-08-243-31/+74
| |
| * Some "feel good" proofs about avail sets.Xavier Leroy2015-08-231-0/+171
| |
| * Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-2312-45/+1030
| | | | | | | | | | | | | | | | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
| * Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-2227-125/+114
| | | | | | | | | | | | | | | | Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
| * Adapt the PowerPC port to the new builtin representation.Xavier Leroy2015-08-2111-260/+285
| | | | | | | | | | | | | | __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating.
| * Simplify the handling of extended inline asm, taking advantage of the new, ↵Xavier Leroy2015-08-213-14/+30
| | | | | | | | structured builtin arguments and results.
| * Merge branch 'master' into 'new-builtins'Xavier Leroy2015-08-2112-185/+206
| |\
| * | Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-2164-2044/+2181
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations.
* | | Improve printing of internal compiler errors.Xavier Leroy2015-08-251-2/+2
| | |
* | | Fixed the -T option.Bernhard Schommer2015-08-251-1/+1
| | | | | | | | | | | | The diab compiler expected -Wm<pathname> without whitespace.
* | | Fixed abbreviation of DW_TAG_formal_parameter.Bernhard Schommer2015-08-251-1/+1
| | | | | | | | | | | | | | | | | | Dwarf debuging entries for formal parameters were printed as variables. This could lead to confusion in function pointer types and later with local variables.
* | | Fixed error in handling of anonymous struct/union/enum types.Bernhard Schommer2015-08-241-8/+15
| | | | | | | | | | | | Composite types should be always handled by the composite_type_info table and not by the normal type table.
* | | Also change the order of high and low pc in the compilation unit tag.Bernhard Schommer2015-08-241-1/+1
| | |
* | | Count number of input files and do not use number of source files for ↵Bernhard Schommer2015-08-241-12/+14
| | | | | | | | | | | | warning about no input.
* | | Added error message when no input file is specified.Bernhard Schommer2015-08-231-0/+5
| | |
* | | Revert "Added support for the location of non static global variables."Bernhard Schommer2015-08-233-9/+2
| | | | | | | | | | | | This reverts commit b4846ffadfa3fbb73ffa7d9c43e5218adeece8da.
* | | Do not add subsize tag to array types without size such as flexible array ↵Bernhard Schommer2015-08-231-10/+14
| | | | | | | | | | | | members.
* | | Added the directory ../share/compcert to the search path for .ini files and ↵Bernhard Schommer2015-08-231-9/+12
| |/ |/| | | | | replaced the if else for the different possibilities by a List.find.
* | test/regression: test packedstruct1 only if unaligned accesses are supported.Xavier Leroy2015-08-215-6/+15
| | | | | | | | Also: exit on error when a test fails.
* | Erase incomplete file .depend.extr if "make depend" fails.Xavier Leroy2015-08-211-3/+2
| |
* | Don't use strdup(), it is not ISO C99.Xavier Leroy2015-08-211-1/+2
| |
* | Asmexpand for ARM: fixed bug in Pfreeframe.Xavier Leroy2015-08-212-5/+5
| | | | | | | | Plus: update comments and credit Bernhard Schommer.
* | Fix bugs in Asmexpand.ml for ARM.Xavier Leroy2015-08-211-8/+9
| |
* | Consistent naming of "P" instructions and consistent ordering of argumentsXavier Leroy2015-08-213-174/+171
| | | | | | | | according to Intel convention (instr destination, argument).
* | Fixed bugs in asm expansion causing the test suite to fail.Xavier Leroy2015-08-211-13/+20
| | | | | | | | More bugs remain.
* | Added command line option to specify a linker command file for the linker.Bernhard Schommer2015-08-201-0/+5
|/
* Added support for the location of non static global variables.Bernhard Schommer2015-08-183-2/+9
|
* Added builtin for the dcbf instructionBernhard Schommer2015-08-175-0/+9
|
* Merge pull request #46 from AbsInt/asmexpandXavier Leroy2015-08-178-615/+1031
|\ | | | | Merge branch 'asmexpand' of github.com:AbsInt/CompCert
| * Merge branch 'master' into asmexpandBernhard Schommer2015-07-141-1/+4
| |\
| * | Updated the branch and implemented the suggested changes.Bernhard Schommer2015-07-143-44/+78
| | |
| * | Merge branch 'master' into asmexpandBernhard Schommer2015-07-1451-241/+1046
| |\ \
| * | | Merge branch 'asmexpand' of github.com:AbsInt/CompCertBernhard Schommer2015-06-268-615/+997
| | | |
* | | | Added builtin for the dcbi instruction.Bernhard Schommer2015-08-175-4/+11
| | | |
* | | | Update clightgen w.r.t. teh calling_conventions record (new field cc_unproto).Xavier Leroy2015-08-171-1/+2
| | | |
* | | | Update clightgen w.r.t. EF_inline_asm (type of the clobber list).Xavier Leroy2015-08-171-1/+6
| | | |
* | | | Added builitin for the icbi instruction.Bernhard Schommer2015-08-145-1/+11
| | | |
* | | | Added builtin for the lwsync barrier.Bernhard Schommer2015-08-145-3/+12
| | | |
* | | | Also print the system in the output to differentiate between diab and gcc ↵Bernhard Schommer2015-08-051-2/+2
| | | | | | | | | | | | | | | | produced code in later checks.
* | | | Swapped high and low pc in the printing of the debug information for ↵Bernhard Schommer2015-07-241-2/+2
| | | | | | | | | | | | | | | | subroutines.
* | | | More tests for alias analysis.Xavier Leroy2015-07-202-6/+30
| | | |
* | | | ValueDomain: add some documentation comments.Xavier Leroy2015-07-191-20/+32
| | | |
* | | | Test to check that alias analysis is prudently conservative on ill-defined ↵Xavier Leroy2015-07-193-1/+153
| | | | | | | | | | | | | | | | pointer manipulations.
* | | | Value analysis: keep track of pointer values that leak through small ↵Xavier Leroy2015-07-199-232/+250
| | | | | | | | | | | | | | | | | | | | | | | | integers with Uns or Sgn abstract values. This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
* | | | Value analysis: keep track of pointer values that leak through arithmetic ↵Xavier Leroy2015-07-195-163/+171
| | | | | | | | | | | | | | | | | | | | | | | | operations with undefined behaviors. Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
* | | | ValueDomain.aptr_of_aval: be more conservative with pointers synthesized ↵Xavier Leroy2015-07-182-6/+14
| | | | | | | | | | | | | | | | | | | | | | | | from numbers. For example: *((int *) 0x10000) = 0. This write used to be treated as not interfering with any load. With this change, in relaxed value analysis mode, it is treated as interfering with any load except those from the current stack frame.
generated by cgit (git 2.34.1) at 2024-07-05 06:45:29 +0000