aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun
Commit message (Collapse)AuthorAge
* Adapt the VM GC hook to handle the no-naked-pointers option flag.Gravatar Pierre-Marie Pédrot2018-04-30
| | | | | | | The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers to C-allocated strings standing for VM bytecode. If the the no-naked-pointers option is set, we perform the check that a stack value lives on the OCaml heap ourselves.
* Make the VM accumulator look like an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
| | | | | | We allocate an additional header so that the accumulator is not a naked pointer. Indeed, it is contained in accumulator blocks which are scanned by the GC as their tags is 0.
* Wrap VM bytecode used on the OCaml side in an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
| | | | | | | | | | This prevents the existence of a few naked pointers to C heap from the OCaml heap. VM bytecode is represented as any block of size at least 1 whose first field points to a C-allocated string. This representation is compatible with the Coq VM representation of (potentially recursive) closures, which are already specifically tailored in the OCaml GC to be able to contain out-of-heap data.
* Moving the VM global atom table to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
|
* Moving the VM global data to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
|
* Handle application of a primitive projection to a not yet evaluated ↵Gravatar Guillaume Melquiond2016-12-23
| | | | cofixpoint (bug #5286).
* Fix #5248 - test-suite fails in 8.6beta1Gravatar Maxime Dénès2016-12-06
| | | | | | | | | | | | | This was yet another bug in the VM long multiplication, that I unfortunately introduced in ebc509ed2. It was impacting only 32-bit architectures. In the future, I'll try to make sure that 1) we provide unit tests for integer arithmetic (my int63 branch ships with such tests) 2) our continuous testing infrastructure runs the test suite on a 32-bit architecture. I tried to set up such an instance, but failed. Waiting for support reply.
* Fix incorrect long multiplication in the VM.Gravatar Guillaume Melquiond2016-11-24
| | | | | | | | | If the result had its 30th bit set, then all the high part of the result on a 64-bit architecture would end up being set, thus breaking subsequent computations. This patch also fixes the incorrectly parenthesized definition of uint32_of_value, which by luck was never misused.
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
|\
| * Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | The bytecode interpreter ensures that the stack space available at some points is above a static threshold. However, arbitrary large stack space can be needed between two check points, leading to segmentation faults in some cases. We track the use of stack space at compilation time and add an instruction to ensure greater stack capacity when required. This is inspired from OCaml's PR#339 and PR#7168. Patch written with Benjamin Grégoire.
* | More comments in VM.Gravatar Maxime Dénès2016-10-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\|
| * Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
| | | | | | | | | | | | | | | | If the second allocation causes a collection of the minor heap, the first allocation will be freed, thus causing a memory corruption. Note: it only happens when computing the native projection of an opaque value while the minor heap is almost full.
* | Remove int64 emulation in bytecode interpreter.Gravatar Maxime Dénès2016-03-25
|/ | | | | | | | We now assume an int64 type is provided by the C compiler. The emulation file was already not compiling, so it is probably not used even on exotic architectures. These files come from OCaml, where they are no longer used either.
* Adds support for the virtual machine to perform reduction of universe ↵Gravatar Gregory Malecha2015-10-28
| | | | | | | | polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions.
* Make interpreter of PROJ simpler by not using the stack.Gravatar Guillaume Melquiond2015-10-14
|
* Remove some unused variables.Gravatar Guillaume Melquiond2015-10-14
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
|
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
| | | | | Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values.
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
| | | | | | | | | On 64 bits architectures, integers could have some of their 32 msb set to 1 internally in the VM. When read back to a Coq term, this was not observable. But an equality test would fail. From the user point of view, the symptom was that vm_compute; reflexivity would succeed but the subsequent Qed would fail. Bug reported by Tahina Ramananandro.
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
| | | | ADDMULDIVINT31 was missing pops in some cases
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
| | | | | I'm pushing this patch now because the previous treatment of such projections in the VM was already unsound. It should however be carefully reviewed.
* Making Coq compile with ocp-memprof.Gravatar Pierre-Marie Pédrot2015-06-01
| | | | Patch provided by Çagdas Bozman.
* Fix some ill-typed debugging code in the VM.Gravatar Guillaume Melquiond2015-04-27
|
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
|
* allows the vm to deal with inductive type with 8388607 constant constructors ↵Gravatar Benjamin Gregoire2015-03-26
| | | | and 8388851 non-constant constructor.
* Fix compilation with forthcoming Ocaml version 4.03.Gravatar Arnaud Spiwack2015-03-13
| | | | | | | Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving: * OCaml runtime header files used to declare the int32, uint32, int64 and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Remove some dead code in the vmGravatar letouzey2012-10-02
| | | | | | | | | | | | | Apparently Cysmtable.set_global_boxed is unused, and removing it allows to get rid of a bunch of C code concerning "boxed" things (including ACCUMULATECOND instruction). Still TODO: Csymtable.set_transparent_const and Csymtable.set_opaque_const appear to be no-ops. Should we remove them ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15845 85f007b7-540e-0410-9357-904b9bb8a0f7
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix thumb2-related build errorGravatar glondu2011-04-19
| | | | | | | | Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882 Signed-off-by: Konstantinos Margaritis <markos@genesi-usa.com> Signed-off-by: Stephane Glondu <steph@glondu.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14027 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
| | | | | | | | | | | | | | | | | | We simply reuse the ocaml flag caml_signals_are_pending and the function caml_process_pending_signals, and place a test at some place of the interpreter loop (at a similar location as in ocaml byterun/interp.c). The symbols caml_* we use are not officially made public in *.h installed alongside ocaml, but they seem pretty stable (there since at least ocaml 3.10, independent of arch and of byte/asm), so we access them via "extern". For once, thanks dirty C... In addition to that, when catching a Ctrl-C, we reset the vm via "coq_sp = coq_stack_high" as suggested by Benjamin G. This patch should be quite portable, it might even work in win32. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
| | | | | | Ocaml 3.10.0 is already three year old... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild improvements + minor makefile fixGravatar letouzey2009-03-24
| | | | | | | | | | | * a small shell script ./build to drive ocamlbuild * rules for all the binaries (apart from coqide and coqchk) * use of ocamlbuild's Echo instead of using shell + sed + awk for generated files * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the list of things to "clean" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
| | | | | | | | | | | ...with proper options for dynamic loading of C stubs. I believe this is the preferred way of compiling C stubs. It also adds by itself -fno-defer-pop, -Wall, -I `ocamlc -where`, so CFLAGS could also be simplified. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
| | | | | | | | | | | | | | | | | | | | - Suite à une modification faite maladroitement, on ne se contentait pas de comparer le nom de la supposition quand on l'insérait dans l'ensemble des suppositions utilisées, mais aussi son type, ce qui était inutilement long (mais pas le facteur principal) - L'environnement était parcouru deux fois pour chaque variable de section. Ce n'était pas très grave vu qu'en général on a assez peu de variables de sections sous la main. Mais ça restait inutile. - Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui gagne dans le cas les pires (comme les théorèmes sur les réels typiquement) une exponentiel dans le temps de recherche (si on visualise l'espace de recherche comme un DAG, l'ancienne procédure le parcourais comme si il était un arbre, ce qui a une complexité exponentielle en la taille du DAG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
| | | | | | | | pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
* patch for C code of addmuldiv31Gravatar thery2008-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
| | | | | | | | | | | | | | the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
* corrections bug dans l'implem de int31Gravatar bgregoir2007-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Appel à caml_modify pour Ocaml 3.07Gravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans les scripts de configuration (coqtop et coqide affichent ↵Gravatar notin2006-07-28
| | | | | | maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 01:48:39 +0000