Commit graph

632 commits

Author SHA1 Message Date
Leonardo de Moura
cad562a448 Add support for metavariables in the normalizer.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-16 19:32:28 -07:00
Leonardo de Moura
1be2a30c8c Fix bug in normalizer. We must create a scope whenever we extend the value stack.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-16 19:32:28 -07:00
Soonho Kong
01339a93a3 Fix cpplint warning in util/safe_arith.cpp 2013-09-16 19:12:12 -07:00
Soonho Kong
13401d534c Add static assertion to util/safe_arith.cpp 2013-09-16 18:17:05 -07:00
Soonho Kong
6ee14bf17f Use unsigned short for the type of interval::bound_deps 2013-09-16 18:15:32 -07:00
Soonho Kong
ef18759e77 Update src/CmakeLists.txt - only check style over files starting with [A-z] 2013-09-16 16:23:20 -07:00
Leonardo de Moura
f79f046294 Add partial support for metavariables in the normalizer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 21:23:50 -07:00
Soonho Kong
58c8c1a5ec Add EXCLUDE_PATTERNS to src/Doxyfile
- */src/cmake/*
- GTAGS GPATH GRTAGS
- memcheck.supp
- *.cmake *.cmake.in
-  *.txt
2013-09-15 20:31:15 -07:00
Leonardo de Moura
2800292947 Add timestamp to metavar_env
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 19:50:48 -07:00
Leonardo de Moura
5a4bc331d2 Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 19:38:36 -07:00
Leonardo de Moura
63e102055e Move metavariables to the kernel. This is the first step for implementing the new elaborator.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-15 12:09:01 -07:00
Soonho Kong
e4b327bbaa Use C++11's <random> in pdeque/pvector tests (cygwin doesn't support rand_r) 2013-09-15 01:38:57 -07:00
Soonho Kong
dcc917a6b4 Use "sprintf" instead of "snprintf" because cygwin doesn't support "snprintf" 2013-09-15 01:38:21 -07:00
Soonho Kong
b553521578 Attempt to suppress valgrind warnings on Travis
- don't understand why cmake on travis doesn't pick up the memcheck.supp
file. It works on my local machine.
2013-09-15 01:17:05 -07:00
Soonho Kong
30f4b2de5f Update memcheck.supp
[skip ci]
2013-09-14 19:33:47 -07:00
Soonho Kong
ce05345129 Update CTestConfig.cmake to fix memcheck.supp 2013-09-14 20:22:05 -04:00
Soonho Kong
60903d3cea Fix cygwin build which was failed due to snprintf 2013-09-14 17:11:37 -07:00
Soonho Kong
c96a6982a0 Add <ctime> header for time() in pdeque/pvector tests 2013-09-13 20:42:49 -07:00
Soonho Kong
5266e22f05 Remove debug code from cpplint.py 2013-09-13 20:37:31 -07:00
Soonho Kong
eda25e77a4 Use time(0) as an initial seed for rand_r() in pvector/pdeque tests 2013-09-13 20:28:15 -07:00
Soonho Kong
f8c0c02cb0 Exclude 'style_check' from MemCheck list 2013-09-13 20:27:35 -07:00
Soonho Kong
0905529720 Add "style_check" test 2013-09-13 20:00:55 -07:00
Soonho Kong
0c450b5c23 Add StyleCheck.cmake 2013-09-13 19:21:02 -07:00
Soonho Kong
f620f54b32 Add target "style" to run cpplint.py
- try "ninja style"
2013-09-13 19:15:38 -07:00
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -07:00
Leonardo de Moura
99eaff0b4f Extract private and static, and add treeview to documentation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 17:55:37 -07:00
Leonardo de Moura
bcc3827a99 Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 13:46:22 -07:00
Leonardo de Moura
d54834279e Use consistent coding style for if-then-else
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 12:57:40 -07:00
Leonardo de Moura
8c735f1daa Use consistent coding style for spaces after ','
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 12:49:03 -07:00
Leonardo de Moura
2c68117adf Tag TODOs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 12:25:21 -07:00
Leonardo de Moura
18f9378f97 Rename numtype.h to num_type.h
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 09:07:44 -07:00
Leonardo de Moura
573ec5ccc2 Rename import_all. The idea is to use consistent name for library files.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 09:06:46 -07:00
Leonardo de Moura
0c09e4524a Use consistent names for import functions, and library files.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 08:58:34 -07:00
Leonardo de Moura
070c87bef0 Rename arith library files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-13 08:55:09 -07:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -07:00
Leonardo de Moura
4c19cc6957 Rename lean frontend files. The prefix lean_ is not necessary anymore.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 20:09:35 -07:00
Leonardo de Moura
26097475fd Use fullpath in #include directives.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 20:04:10 -07:00
Leonardo de Moura
c655e9fe7b Move sexpr_funcs to sexpr_fn. Using consistent file name conventions.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 18:27:46 -07:00
Leonardo de Moura
2e990ef7d3 Fix warnings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 14:02:40 -07:00
Leonardo de Moura
bc69e7803f Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 11:18:26 -07:00
Leonardo de Moura
74b8a4f0ac Add support for writing a[i] = v instead of a.set(i, v) in the pvector class.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 11:12:02 -07:00
Leonardo de Moura
f972cc9aae Fix bugs in pvector. Improve test driver
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 11:01:40 -07:00
Leonardo de Moura
55ff49d2d5 Replace queue.h with pdeque.h
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 10:09:54 -07:00
Leonardo de Moura
cd5e45bae2 Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-12 08:28:24 -07:00
Soonho Kong
5858c9d5e0 Update tests/util/list.cpp to suppress a g++ warning 2013-09-12 01:39:04 -07:00
Leonardo de Moura
f7196e05ff Add 'persistent' vectors. We should use the same approach for queues.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
ef0e0ad382 Add (optional) performance tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
572c7ced2a Add #include<atomic> to expr.h. We need it when #define LEAN_THREAD_UNSAFE_REF_COUNT is used
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
ed15a2df9b Use split_reverse_second instead of split and then reverse in queue
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:55 -07:00
Leonardo de Moura
37498f9fb8 Add persistent queues
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:54 -07:00
Leonardo de Moura
3657320edb Add basic list functions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-11 19:48:54 -07:00
Soonho Kong
7a6032dd86 Update memcheck.supp to ignore bash memroy leak on Fedora19 2013-09-10 22:44:24 -04:00
Soonho Kong
9e3583a04a Update memcheck.supp to match the thread bug patterns we get by using clang++-3.3 2013-09-10 17:37:22 -07:00
Soonho Kong
a993424165 Use "--gen-suppressions=all" in valgrind 2013-09-10 17:09:39 -07:00
Soonho Kong
6569406fb9 Update memcheck.supp
add reference for the suppression stuff
[skip ci]
2013-09-10 15:47:47 -07:00
Soonho Kong
3505ed8adb Use suppressions file to ignore certain valgrind warnings 2013-09-10 15:37:09 -07:00
Soonho Kong
9113f824bd Use '--track-origins=yes' option in valgrind 2013-09-10 14:31:30 -07:00
Leonardo de Moura
6fe86ffefd Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-10 13:51:02 -07:00
Soonho Kong
fae6c29237 Fix memory leaks in mpfp.h 2013-09-10 13:26:14 -07:00
Soonho Kong
8ce18a1508 Use "--leak-check=full" option in valgrind 2013-09-10 13:12:22 -07:00
Soonho Kong
f4edbba325 Turn off '--show-reachable=yes' valgrind option 2013-09-10 12:34:33 -07:00
Soonho Kong
b04bdae763 Use "--trace-children=yes" option for MemCheck(valgrind) to handle
leantests shell script
2013-09-10 10:47:04 -07:00
Leonardo de Moura
4c67721d32 Fix test error on Cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-09 18:35:11 -07:00
Leonardo de Moura
adfbba6447 Fix problem reported by Soonho
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 23:10:33 -07:00
Leonardo de Moura
2ca30571b4 Display the input term in the output of the Check command. It is useful to see the fully elaborated term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 22:55:21 -07:00
Leonardo de Moura
a8ba50531b Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 20:38:11 -07:00
Leonardo de Moura
59a589037e Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 11:23:46 -07:00
Leonardo de Moura
df116f88e0 Improve pretty printer for Pi's
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-08 11:04:07 -07:00
Leonardo de Moura
1cee392483 Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 22:33:18 -07:00
Leonardo de Moura
33c4b44b2b Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 11:15:11 -07:00
Leonardo de Moura
bab11b57ad Move Symm and Trans back to basic_thms.cpp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:49:35 -07:00
Leonardo de Moura
c674bb3790 Add castlib as an independent library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:40:47 -07:00
Leonardo de Moura
7a9d53d0d7 Refactor arith libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 23:19:47 -07:00
Leonardo de Moura
b92bbeb83b Add casting propagation and normalization
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 20:45:26 -07:00
Leonardo de Moura
7eab229114 Improve check_pi in lean elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:58:33 -07:00
Leonardo de Moura
c0c2f52087 Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:32:15 -07:00
Leonardo de Moura
b62816cc25 Fix problem with pretty printer. Add another test for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:01:11 -07:00
Leonardo de Moura
edafd519e1 Add missing case to elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 17:43:08 -07:00
Leonardo de Moura
26bf7bcaac Fix bug in the elaborator. Move character ' to class A
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 17:12:35 -07:00
Leonardo de Moura
8840b37258 Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 11:02:00 -07:00
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 10:06:26 -07:00
Leonardo de Moura
6da194334e Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
6f3b0c30fb Add 'Variables' command.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
3dc55c452c Parse decimal values
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 08:48:12 -07:00
Leonardo de Moura
b3a095b068 Fix pretty printer for evaluator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 18:57:29 -07:00
Leonardo de Moura
c22bd8b6ed Clean elaborator_exception pretty printing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 10:15:52 -07:00
Leonardo de Moura
eb96e6441f Moved kernel exception formatting to kernel_exception_formatter.cpp.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-05 10:15:43 -07:00
Soonho Kong
974b99b424 Update CTestCustom.cmake.in
Exclude "threads" test from valgrind targets
[skip ci]
2013-09-04 16:41:04 -07:00
Leonardo de Moura
87d3961158 Improve elaborator error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
613d83cdf4 Improve application type mismatch errors. We also show the implicit arguments (not just their types)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:58 -07:00
Leonardo de Moura
408005b730 Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 16:36:57 -07:00
Soonho Kong
30e5ac7004 Fix OSX linker warning issue 2013-09-04 15:35:07 -07:00
Leonardo de Moura
be7fa0932a Add unicode name for the types: Nat, Int and Real
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 09:03:41 -07:00
Leonardo de Moura
d41160f8a5 Modify environment. Now, when a builtin value is declared, if it has a unicode alternative representation, then we add it as a definition. Now, everything that occurs in the environment has been 'declared'.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 08:53:00 -07:00
Leonardo de Moura
e955c054ca Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 08:30:04 -07:00
Leonardo de Moura
9f34f96b08 Add another example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 05:40:28 -07:00
Soonho Kong
a8c16bc127 Fix test coverage problem by forcing to use gcov-4.8 2013-09-04 08:07:24 -04:00
Soonho Kong
5e603dbf9f Use cdash on cmacslab2 machine due to 10-build per day restriction 2013-09-04 04:46:37 -07:00
Leonardo de Moura
9f64e2b14b Fix another cdash warning
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 04:43:55 -07:00
Leonardo de Moura
00bee9c96e Fix warning produced by clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 04:40:43 -07:00