| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
| |
Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The commutation lemmas between program transformations and Genv operations now take separate compilation into account. For example:
Theorem find_funct_ptr_match:
forall b f,
find_funct_ptr (globalenv p) b = Some f ->
exists cunit tf,
find_funct_ptr (globalenv tp) b = Some tf
/\ match_fundef cunit f tf
/\ linkorder cunit ctx.
Note how "f" and "tf" are related wrt a compilation unit "cunit" which is not necessarily "ctx" (the context for the whole program), but can be a sub-unit of the this whole program.
The other changes in Globalenvs are a long-overdue refactoring and cleanup:
- Introduce Senv.equiv (extensional equivalence between two Senv.t) to collect (in one place) the invariance properties relevant to external functions (preservation of names, of public names, and of volatile blocks).
- Revise internal representation of Genv.t: one map ident -> globdef F V instead of two maps ident -> F and ident -> globvar V.
- More precise characterization of initial memory states: "Genv.init_mem_characterization" uniquely characterizes every byte (memval) of the representation of an initialized global variable.
- Necessary and sufficient conditions for the initial memory state to exist.
- Revised proofs about init_mem, especially init_mem_inject.
- Removed some Genv lemmas that were unused.
|
|
|
|
|
|
|
| |
- Add "prog_defmap" to compute the ptree name -> global definition corresponding to a program.
- Move "match_program" to Linking.
- Clean up and simplify a bit the transf_* functions for program transformations.
- Add a new kind of external functions, "EF_runtime". Unlike "EF_external", an "EF_runtime" external function cannot be implemented by an internal function definition in another compilation unit. (Linking returns an error in this case.) We will use "EF_runtime" for the "_i64_*" helper functions, which must not be defined by the program, and instead must remain external.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This framework follows "approach A" from the paper "Lightweight Verification of Separate Compilation" by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016.
Syntactic linking (of compilation units and their syntactic elements) is modeled by a type class with two components:
- a partial binary operation "link" that returns the syntactic element corresponding to the act of linking together its two arguments. It may fail if the two arguments cannot be linked, e.g. are incompatible definitions of the same name.
- a partial order "linkorder x y" that holds if "x" is a sub-unit of a whole program or bigger unit "y", or in other words, if "y" can be obtained by linking "x" with other units.
Instances of this type class are provided for the type AST.program and its syntactic elements (globvar, globdef, etc).
The "match_program" predicate that provides a relational characterization of compiler passes / program transformations is extended to account for context-dependent transformations and separate compilation: the transformation of a function definition can depend on the compilation unit it occurs in (this is the context), and this compilation unit "ctx" is characterized as any unit that is in the "linkorder ctx prog" relation with the whole source program "prog".
Under mild hypotheses, we show that "match_program" commutes with linking: if a1 matches b1, a2 matches b2, and a1 and a2 link together producing a, then b1 and b2 link together, producing a b that matches a.
Finally, we extend binary linking to linking of a nonempty list of compilation units; commutation with "match_program" still holds.
|
|
|
|
|
| |
- Make Mem.unchanged_on transitive.
- Add Mem.drop_perm_unchanged_on.
|
|
|
|
|
|
|
| |
- Coqlib: option_rel to lift a relation to option type.
- Coqlib: more lemmas about list_forall2.
- Coqlib: introduce type nlist (nonempty lists) and some operations.
- Maps: a variant of PTree.elements_extensional that uses option_rel.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Added the gcc options for the preprocessor:
-Xpreprocessor
-M
-MM
-MF
-MG
-MP
-MT
-MQ
-nostdinc
-imacros
-idirafter
-isystem
-iquote
-P
-C
-CC
Also warn for not supported GCC options in the diab case.
Bug 18066
|
|\ |
|
| |
| |
| |
| |
| |
| | |
Added additional configuration entries to seperate tools from options in the
.ini files. Internally they are just concatenated in Configuration.ml which
allows it to still use old .ini files.
|
| |
| |
| |
| |
| |
| |
| | |
The Xassembler option passes one option to the assembler and can
be used to pass options to the underlying assembler that the gcc
driver does not recognize.
Bug 18066
|
| | |
|
|/
|
|
|
|
|
|
|
|
|
| |
CompCert now recognizes the gcc linker options:
-nostartfiles
-nodefaultlibs
-nostdlib
-s
-Xlinker <opt>
-u <symb>
Bug 18066.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Two reasons:
- The movs is not supported if rd or rs is r13 (the stack ptr register).
Newer versions of GNU as reject it, older versions were probably
emulating it.
- The purpose of setting the "s" flag on some operations is to
enable 16-bit encoding in Thumb2 mode. However, for "mov"
it is the non-s form that has a 16-bit encoding; the s form
is never more compact.
|
|
|
|
|
| |
The new option -static passes the -static flag to the linker.
Bug 18066.
|
| |
|
|\
| |
| | |
Better treatment of names in the clightgen tool
|
| |
| |
| |
| | |
clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
|
|/
|
|
| |
This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
|
| |
|
| |
|
|
|
|
|
|
|
| |
The -include option is passed to the preprocessor and -include <file>
is equivalent to writting #include "<file>" as first line in the
primary source file.
Bug 18066.
|
|\
| |
| |
| | |
Flag -doptions to save machine configuration and command-line flags to a JSON file.
|
| | |
|
| |
| |
| |
| |
| |
| | |
The new options dumps the compiler options in a json file per.
This includes the clflags, compcert.ini and machine settings.
Bug 17988.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Since we cannot construct a default initializer for void types
we need to exit earlier.
Bug 18004.
|
| |
| |
| |
| |
| |
| | |
In parse_int it was not tested if the value of v is smaller than
zero. This allowed it that certain large integers were accepted
due to wrap around.
|
|/
|
|
|
| |
Implementing the same behavior as gcc anc clang.
Bug 18004
|
|
|
|
| |
The new option -dprepro allows it to keep the preprocessed source code files.
|
| |
|
|
|
|
|
|
| |
Gcc defines wint_t in the stddef header (even if it is not stanadard) and
additionally defines it if stddef is reincluded. The fix now defines it
before stddef is checked for reinclusion.
|
| |
|
|
|
|
|
|
| |
The typdef, enumerator and function_type types form the DebugTypes and
DwarfTypes shared a some fields. This commits renames them in order to
make them more unique and avoid potential name clashes.
|
|
|
|
|
|
|
| |
CompCert now prints if the assembler, linker or preprocessor
command failed and a hint for the user to get the full command
line.
Bug 17894
|
|
|
|
| |
The new configuration option -clightgen activates the build of clightgen.
|
|\
| |
| |
| | |
ssh://ssh.absint.com/common/repositories/git/tools/compcert
|
| |
| |
| |
| | |
17838
|
| |
| |
| |
| | |
Follow-up to commit f531d38
|
| |
| |
| |
| |
| |
| |
| | |
ARM: add __builtin_clzl, __builtin_clzll
IA32: add __builtin_clzl, __builtin_clzll,
__builtin_ctzl, __builtin_ctzll
Add corresponding tests in tests/regression/
|
|/ |
|
|
|
|
| |
compatibility, and not "unsigned int", as previously implemented.
|
|
|
|
| |
The original code produces wrong results if res and al are the same register.
|
| |
|
| |
|