diff --git a/kernel/mem.c b/kernel/mem.c
index 5db94573..71ee204f 100644
--- a/kernel/mem.c
+++ b/kernel/mem.c
@@ -619,7 +619,8 @@ static void *mckernel_allocate_aligned_pages_node(int npages, int p2align,
 			}
 			else {
 #ifdef PROFILE_ENABLE
-				profile_event_add(PROFILE_mpol_alloc_missed, npages * 4096);
+				profile_event_add(PROFILE_mpol_alloc_missed,
+						  npages * PAGE_SIZE);
 #endif
 				dkprintf("%s: couldn't fulfill explicit NUMA request for %d pages\n",
 						__FUNCTION__, npages);
@@ -711,7 +712,8 @@ static void *mckernel_allocate_aligned_pages_node(int npages, int p2align,
 	}
 	else {
 #ifdef PROFILE_ENABLE
-		profile_event_add(PROFILE_mpol_alloc_missed, npages * 4096);
+		profile_event_add(PROFILE_mpol_alloc_missed,
+				  npages * PAGE_SIZE);
 #endif
 		dkprintf("%s: couldn't fulfill user policy for %d pages\n",
 			__FUNCTION__, npages);
@@ -1163,7 +1165,7 @@ static void page_fault_handler(void *fault_addr, uint64_t reason, void *regs)
 
 	cpu_enable_interrupt();
 
-	if ((uintptr_t)fault_addr < 4096) {
+	if ((uintptr_t)fault_addr < PAGE_SIZE) {
 		error = -EINVAL;
 	} else {
 		error = page_fault_process_vm(thread->vm, fault_addr, reason);
diff --git a/kernel/syscall.c b/kernel/syscall.c
index 8fa0b937..6fbbd6ea 100644
--- a/kernel/syscall.c
+++ b/kernel/syscall.c
@@ -3100,7 +3100,7 @@ getcred(int *_buf)
 	struct syscall_request request IHK_DMA_ALIGN;
 	unsigned long phys;
 
-	if((((unsigned long)_buf) ^ ((unsigned long)(_buf + 8))) & ~4095)
+	if ((((unsigned long)_buf) ^ ((unsigned long)(_buf + 8))) & PAGE_MASK)
 		buf = _buf + 8;
 	else
 		buf = _buf;
@@ -5757,7 +5757,8 @@ long do_futex(int n, unsigned long arg0, unsigned long arg1,
 				request.number = n;
 				unsigned long __phys;                                          
 
-				if((((unsigned long)tv) ^ ((unsigned long)(tv + 1))) & ~4095)
+				if ((((unsigned long)tv) ^
+				    ((unsigned long)(tv + 1))) & PAGE_MASK)
 					tv_now = tv + 1;
 				if (ihk_mc_pt_virt_to_phys(cpu_local_var(current)->vm->address_space->page_table, 
 						(void *)tv_now, &__phys)) { 
diff --git a/lib/vsprintf.c b/lib/vsprintf.c
index 618f1e2e..cad46829 100644
--- a/lib/vsprintf.c
+++ b/lib/vsprintf.c
@@ -23,6 +23,7 @@
 #include <types.h>
 #include <ctype.h>
 #include <limits.h>
+#include <memory.h>
 
 unsigned char _ctype[] = {
 	_C,_C,_C,_C,_C,_C,_C,_C,                        /* 0-7 */
@@ -584,7 +585,7 @@ static char *string(char *buf, char *end, char *s, struct printf_spec spec)
 {
 	int len, i;
 
-	if ((unsigned long)s < 4096)
+	if ((unsigned long)s < PAGE_SIZE)
 		s = "<NULL>";
 
 	len = strnlen(s, spec.precision);