Developer's Guide - Revision history

Preiner at 17:10, 21 August 2017

2017-08-21T17:10:46Z

Ajreynol: /* Using ASAN */

2016-05-03T19:55:23Z

‎Using ASAN

Ajreynol: /* Using ASAN */

2016-05-03T19:34:45Z

‎Using ASAN

Guyk: /* Using ASAN */

2016-04-02T03:46:26Z

‎Using ASAN

Guyk: /* Using ASAN */

2016-04-02T03:45:41Z

‎Using ASAN

Guyk: /* Using ASAN */

2016-04-02T03:45:05Z

‎Using ASAN

Guyk: /* Using ASAN */

2016-04-02T03:44:17Z

‎Using ASAN

Guyk: /* Using ASAN */

2016-04-02T03:42:38Z

‎Using ASAN

Guyk: /* Using ASAN */

2016-04-02T03:38:16Z

‎Using ASAN

Guyk: /* Profiling the code */

2016-04-02T03:34:10Z

‎Profiling the code

← Older revision		Revision as of 17:10, 21 August 2017
Line 1:		Line 1:
−	In addition to this wiki, we also have a [http://cs.nyu.edu/mailman/listinfo/cvc4-devel developer mailing list] and [~~http~~://~~church~~.~~cims.nyu.edu~~/~~bugzilla3~~/ ~~Bugzilla database~~] for this version of CVC. CVC3 resources have been kept separate, at this time, because of the different needs of CVC4 during active development.	+	In addition to this wiki, we also have a [http://cs.nyu.edu/mailman/listinfo/cvc4-devel developer mailing list] and [https://github.com/CVC4/CVC4/issues Github issue tracker] for this version of CVC. CVC3 resources have been kept separate, at this time, because of the different needs of CVC4 during active development.

	=Source tree layout=		=Source tree layout=

@@ Line 617: / Line 617: @@
 B) To run CVC4 with one example:
-    ASAN_SYMBOLIZER_PATH=$PREFIX/bin/llvm-symbolizer ./builds/bin/cvc4 test/regress/regress0/ite5.smt2
+    ASAN_SYMBOLIZER_PATH=$BUILD_DIR/bin/llvm-symbolizer ./builds/bin/cvc4 test/regress/regress0/ite5.smt2
 C) To run CVC4 on make regress:
-    ASAN_SYMBOLIZER_PATH=$PREFIX/bin/llvm-symbolizer make regress
+    ASAN_SYMBOLIZER_PATH=$BUILD_DIR/bin/llvm-symbolizer make regress
 =Coding guidelines=

@@ Line 599: / Line 599: @@
 Step 2: Configuring CVC4
-A) This is mostly all done at configure time. The main goals are to disable proofs (for now), set binary locations, and add compilation and linking flags.
+A) This is mostly all done at configure time. The main goals are to disable proofs (for now), set binary locations, and add compilation and linking flags. Let $BUILD_DIR be the directory build/ created above.
     $ ./configure \
          --disable-proof \ # We need this for now
          [usual options --with-antlr-dir=... ANTLR=...  --with-build=debug ] \
-         CC=$PREFIX/bin/clang CXX=$PREFIX/bin/clang++ LD=$PREFIX/bin/clang \
+         CC=$BUILD_DIR/bin/clang CXX=$BUILD_DIR/bin/clang++ LD=$BUILD_DIR/bin/clang \
          CFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" \
          LDFLAGS="-fsanitize=address" \

@@ Line 602: / Line 602: @@
     $ ./configure \
-         --disable-proof \#We need this for now
+         --disable-proof \ # We need this for now
          [usual options --with-antlr-dir=... ANTLR=...  --with-build=debug ] \
          CC=$PREFIX/bin/clang CXX=$PREFIX/bin/clang++ LD=$PREFIX/bin/clang \

@@ Line 602: / Line 602: @@
     $ ./configure \
-       --disable-proof \#We need this for now
+        --disable-proof \#We need this for now
-      [usual options --with-antlr-dir=... ANTLR=...  --with-build=debug ] \
+        [usual options --with-antlr-dir=... ANTLR=...  --with-build=debug ] \
-      CC=$PREFIX/bin/clang CXX=$PREFIX/bin/clang++ LD=$PREFIX/bin/clang \
+        CC=$PREFIX/bin/clang CXX=$PREFIX/bin/clang++ LD=$PREFIX/bin/clang \
-      CFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" \
+        CFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" \
-      LDFLAGS="-fsanitize=address" \
+        LDFLAGS="-fsanitize=address" \
-      CXXFLAGS="-fsanitize=address -fno-omit-frame-pointer -g"
+        CXXFLAGS="-fsanitize=address -fno-omit-frame-pointer -g"
 B) Recompile with make

@@ Line 593: / Line 593: @@
     cd build
     export PREFIX=$HOME/target/llvm
-    cmake -G "Unix Makefiles"  -DCMAKE_INSTALL_PREFIX=$PREFIX ../llvm
+    cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$PREFIX ../llvm
     make
     make install # optional

@@ Line 582: / Line 582: @@
 ==Using ASAN==
-Step 1: Install clang+llvm from source
+Step 1: Install Clang and LLVM from source.
-A) Install cmake
+A) Install cmake.
 B) Follow the instructions for downloading clang from source [http://clang.llvm.org/get_started.html here]. You need to do steps 2 (checkout llvm), 3 (checkout clang) and 5 (checkout compiler-rt).
-C) We now need to do step 7 (Build LLVM and Clang). On step 7, it is recommended to use a prefix in $HOME. We'll use $PREFIX for this directory.
+C) Proceed to step 7 (building LLVM and Clang). It is recommended to use a prefix in $HOME. We'll use $PREFIX for this directory.
-    mkdir build # you likely want this outside of llvm
+    mkdir build # you likely want this outside of the LLVM directory
     cd build
     export PREFIX=$HOME/target/llvm
     cmake -G "Unix Makefiles"  -DCMAKE_INSTALL_PREFIX=$PREFIX ../llvm
     make
-    make install #optional
+    make install # optional
 Step 2: Configuring CVC4
-A) This is mostly all done at configure time. The main goals are to disable proofs (for now), set binary locations, and add compilation+linking flags.
+A) This is mostly all done at configure time. The main goals are to disable proofs (for now), set binary locations, and add compilation and linking flags.
     $ ./configure \

← Older revision		Revision as of 03:34, 2 April 2016
Line 580:		Line 580:

	For more information, see [[Build_Problems#Profiling]].		For more information, see [[Build_Problems#Profiling]].
		+
		+	==Using ASAN==
		+	Step 1: Install clang+llvm from source
		+	A) Install cmake
		+	B) Follow the instructions for downloading clang from source here: http://clang.llvm.org/get_started.html
		+	You need to do steps 2 (checkout llvm), 3 (checkout clang), 5 checkout compiler-rt
		+	C) We now need to do step 7 (Build LLVM and Clang). On step 7, it is recommended to use a prefix in $HOME.
		+	We'll use $PREFIX for this directory.
		+
		+	mkdir build # you likely want this outside of llvm
		+	cd build
		+	export PREFIX=$HOME/target/llvm
		+	cmake -G "Unix Makefiles" -DCMAKE_INSTALL_PREFIX=$PREFIX ../llvm
		+	make
		+	make install #optional
		+
		+	Step 2: Configuring CVC4
		+	A) This is mostly all done at configure time. The main goals are to disable proofs (for now), set binary locations, and add compilation+linking flags.
		+	$ ./configure \
		+	--disable-proof \#We need this for now
		+	[usual options --with-antlr-dir=... ANTLR=... --with-build=debug ] \
		+	CC=$PREFIX/bin/clang CXX=$PREFIX/bin/clang++ LD=$PREFIX/bin/clang \
		+	CFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" \
		+	LDFLAGS="-fsanitize=address" \
		+	CXXFLAGS="-fsanitize=address -fno-omit-frame-pointer -g"
		+
		+	B) Recompile with make
		+
		+	Step 3: Running ASAN
		+	A) Documentation is here: http://clang.llvm.org/docs/AddressSanitizer.html
		+	B) To run CVC4 with one example:
		+	ASAN_SYMBOLIZER_PATH=$PREFIX/bin/llvm-symbolizer ./builds/bin/cvc4 test/regress/regress0/ite5.smt2
		+	C) To run CVC4 on make regress:
		+	ASAN_SYMBOLIZER_PATH=$PREFIX/bin/llvm-symbolizer make regress

	=Coding guidelines=		=Coding guidelines=