Skip to content

Commit

Permalink
Static compile
Browse files Browse the repository at this point in the history
  • Loading branch information
Ubuntu committed Aug 30, 2024
1 parent a8fe19a commit bd241b6
Show file tree
Hide file tree
Showing 6 changed files with 49 additions and 31 deletions.
2 changes: 1 addition & 1 deletion src/dpa/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ include ../makefile.include

ifeq ($(STATIC_DPA), 1)
CXX += -static-libstdc++ -static-libgcc -static
LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
else
LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl
Expand Down
6 changes: 4 additions & 2 deletions src/makefile.include
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,8 @@ endif
GPP=g++ -std=c++17

#### flags
CFLAG_OPT = -g -O3
#CFLAG_OPT = -g -O3
CFLAG_OPT = -O3

#### includes
INCLUDE_DIRS =
Expand All @@ -59,7 +60,8 @@ CFLAGS_INC = $(INCLUDE_DIRS)
CFLAGS = -c $(CFLAGS_INC) $(CFLAG_OPT)

#### optional flags
FLAG_PG = -pg
#FLAG_PG = -pg
FLAG_PG =

#### link flags
LINK_FLAGS = $(CFLAG_OPT)
Expand Down
12 changes: 8 additions & 4 deletions src/reach/Makefile
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
include ../makefile.include

CFLAGS += -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label
CFLAGS += -fPIC -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label

ifeq ($(STATIC_REA), 1)
CXX += -static-libstdc++ -static-libgcc -static
LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
else
LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl
endif

ifeq ($(ENABLE_Y2), 1)
Y2_DIR = $(DEPS)/yices2
Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a
Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a $(STATIC_GMPXX) $(STATIC_GMP)
INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include
LINKLIBS += $(Y2_LIB)
CFLAGS += -D_Y2
Expand All @@ -38,11 +38,15 @@ endif

ifeq ($(ENABLE_M5), 1)
MSAT_DIR = $(DEPS)/mathsat
MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a # $(STATIC_GMPXX) $(STATIC_GMP)
MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a $(STATIC_GMPXX) $(STATIC_GMP)
INCLUDE += -I$(MSAT_DIR)/include
LINKLIBS += $(MSAT_LIB)
CFLAGS += -D_M5
endif
ifeq ($(CONFIG_M5), 1)
CFLAGS += -DBACKEND_M5
REACH_SUFFIX = m5
endif

ifeq ($(ENABLE_Z3), 1)
Z3_DIR = $(DEPS)/z3
Expand Down
34 changes: 23 additions & 11 deletions src/reach/reach_backend.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,23 @@
/// Configurations
/// Note: Only one of the below flag should be enabled

// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries
// #define BACKEND_Y2 // Yices 2 for all queries
// #define BACKEND_BT // Boolector for all queries
// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries
// #define BACKEND_MT // MathSAT 5 for all queries


// Use Y2 backend for all abstract queries
/// Config: BACKEND_Y2BT
#ifdef BACKEND_Y2BT
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE y2_API // Solver for getting unsat core
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core

#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
#endif

/// Config: BACKEND_Y2
#ifdef BACKEND_Y2
Expand All @@ -56,16 +68,16 @@
#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
#endif

/// Config: BACKEND_Y2BT
#ifdef BACKEND_Y2BT
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE y2_API // Solver for getting unsat core
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core
/// Config: BACKEND_M5
#ifdef BACKEND_M5
#define SOLVER_CTI m5_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH m5_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN m5_API // Solver for checking if frame restriction global
#define SOLVER_AB m5_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE m5_API // Solver for getting unsat core
#define SOLVER_MUS m5_API // Solver for getting minimal unsat core

#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
#define SOLVER_BV m5_API // Solver for concrete / bit-vector queries
#endif


Expand Down
2 changes: 1 addition & 1 deletion src/vwn/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ LINKLIBS =

ifeq ($(STATIC_VWN), 1)
CXX += -static-libstdc++ -static-libgcc -static
LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
LINK_FLAGS += -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
LINKLIBS += $(STATIC_GMPXX) $(STATIC_GMP)
else
Expand Down
24 changes: 12 additions & 12 deletions workers.txt
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
python3 avr.py --split
python3 avr.py --backend y2 --split
python3 avr.py --kind --abstract sa --backend bt
python3 avr.py --kind --abstract sa --split
python3 avr.py --abstract sa --backend bt
python3 avr.py --kind --abstract sa --backend y2 --split
python3 avr.py --abstract sa
python3 avr.py
python3 avr.py --bmc --abstract sa --backend bt --split
python3 avr.py --bmc --abstract sa+heavy
python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
python3 avr.py --abstract sa4 --split --forward 1 --interpol 1
python3 avr.py --abstract sa+heavy --backend bt --split
python3 avr.py
python3 avr.py --abstract sa8 --level 5 --granularity 3 --forward 1 --interpol 1
python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1
python3 avr.py --split --level 0
python3 avr.py --abstract sa8 --backend y2 --split --interpol 1
python3 avr.py --kind --abstract sa --backend bt --split
python3 avr.py --abstract sa8 --split --interpol 1
python3 avr.py --abstract sa16 --split --forward 1 --backend bt
python3 avr.py --abstract sa32 --backend bt --level 0 --granularity 3
python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
python3 avr.py --bmc --abstract sa --backend y2
python3 avr.py --abstract sa --backend bt
python3 avr.py --abstract sa+heavy
python3 avr.py --bmc --abstract sa+heavy --backend bt
python3 avr.py --kind --abstract sa+heavy --backend bt

0 comments on commit bd241b6

Please sign in to comment.