aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
...
* | | start the new "BTL" IR.Sylvain Boulmé2021-04-281-0/+6
|/ /
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-072-0/+50
| |
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-177-10/+279
|\ \
| * \ Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0417-10/+1710
| |\ \ | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-10/+279
| |\ \ \ | | | |/ | | |/|
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
| | | | | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib.
| | * | Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | | | | | | | | | | | | | | | | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | | | | | | | | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
| | * | Add a canonical encoding of identifiers as numbers and use it in clightgen ↵Xavier Leroy2020-05-191-3/+76
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#353) Within CompCert, identifiers (names of C functions, variables, types, etc) are represented by unique positive numbers, sometimes called "atoms". In the original implementation, atoms 1, 2, ..., N are assigned to identifiers as they are encountered. The resulting number are small and are efficient when used as keys in data structures such as PTrees. However, the mapping from C source-level identifiers to atoms differs between compilation units. This is not a problem for CompCert but complicates CompCert-based verification tools that need to combine several compilation units. This commit introduces an alternate implementation of atoms, suggested by Andrew Appel. The choice between implementations is governed by the Boolean reference `Camlcoq.use_canonical_atoms`. In the alternate implementation, identifiers are converted to bit sequences via a Huffman encoding, then the bits are represented as positive numbers. The same identifier is always represented by the same number. However, the numbers are usually bigger than in the original implementation, making PTree operations slower: lookups and updates take time linear in the length of the identifier, instead of logarithmic time in the number of identifiers encountered. The CompCert compiler (the `ccomp` executable) still uses the original implementation, but the `clightgen` tool used in conjunction with the VST program logic can use either implementations: - The alternate "canonical atoms" implementation is used by default, and also if the `-canonical-idents` option is given. - The original implementation is used if the `-short-idents` option is given. Closes: #222 Closes: #311
| | * | Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
| | | | | | | | | | | | | | | | | | | | | | | | The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/
| | * | Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | | | | | | | | | | | | | | | | | | | So as not to depend on an implicit import from module Program. (See PR #352.)
| | * | Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | | | | | | | | | | | | | | | | | | | | | | | On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
| | * | Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
| | | | | | | | | | | | | | | | | | | | The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`.
* | | | Merge branch 'kvx-test-prepass' of ↵David Monniaux2020-11-2718-0/+1802
|\ \ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into aarch64-prepass+postpass
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-191-10/+53
| |\ \ \ | |/ / / |/| | |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+6
| |\| |
| * | | fix issue 210 in simu_checkSylvain Boulmé2020-09-211-4/+10
| | | |
| * | | starting to move common filesDavid Monniaux2020-09-1616-0/+1651
| | | |
* | | | Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
| |/ / |/| | | | | | | | helps to understand the difference between union and merge in the interface
* | | centralize if_sameDavid Monniaux2020-10-091-0/+6
|/ /
* | Adding copyrightsCyril SIX2020-05-044-0/+48
| |
* | moved to extraDavid Monniaux2020-04-161-0/+0
| |
* | gmap2_idemDavid Monniaux2020-04-161-65/+111
| |
* | gmap2_idemDavid Monniaux2020-04-161-0/+16
| |
* | gmap2_idem_EmptyDavid Monniaux2020-04-161-0/+54
| |
* | begin HashedMapsDavid Monniaux2020-04-161-0/+332
| |
* | forward_move_lDavid Monniaux2020-03-101-1/+13
| |
* | kill_reg_soundDavid Monniaux2020-03-091-1/+1
| |
* | CSE3 generate lists of killableDavid Monniaux2020-03-051-0/+4
| |
* | more about extraction and linkingDavid Monniaux2020-03-051-185/+180
| |
* | streamlined lattice codeDavid Monniaux2020-03-052-30/+15
| |
* | 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
| |
* | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-033-96/+317
|\ \ | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-4/+5
| |\| | | | | | | | | | mppa-work-upstream-merge
| * | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-1/+178
| |\ \
| | * | shrx'1_shr'David Monniaux2020-01-141-1/+127
| | | |
| | * | shrx1_shrDavid Monniaux2020-01-141-0/+51
| | | |
| * | | set_disjointDavid Monniaux2019-12-131-0/+49
| | | |
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-134-12/+15
| |\| | | | | | | | | | | | | | mppa-work-upstream-merge
| * | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-65/+517
| |\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * | | | IcondCyril SIX2019-10-071-0/+5
| | | | |
| * | | | Ibuiltin proofCyril SIX2019-10-042-12/+89
| | | | |
| * | | | Adding decidable equality for intCyril SIX2019-10-041-1/+12
| | | | |
| * | | | Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-051-1/+1
| | | | |
| * | | | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2David Monniaux2020-02-271-4/+5
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
| | |_|/ | |/| | | | | | | | | | Just moved a frequent failure case ahead of a costly "simpl".
* | | | progress on wellformed regDavid Monniaux2020-02-051-1/+120
| | | |
generated by cgit (git 2.34.1) at 2024-05-20 03:34:10 +0000