Changes suggested by Ingo: style fix, and a system_time optimization.

src/system/boot/platform/bios_ia32/mmu.cpp

@@ -522,7 +522,7 @@ mmu_get_virtual_mapping(addr_t virtualAddress, addr_t *_physicalAddress)
 	if ((tableEntry & (1 << 0)) == 0)
 		return false;
 
-	*_physicalAddress = tableEntry & 0xFFFFF000;
+	*_physicalAddress = tableEntry & 0xfffff000;
 	return true;
 }
 

src/system/libroot/os/arch/x86_64/system_time_asm.S

@@ -28,7 +28,10 @@ FUNCTION_END(__x86_setup_system_time)
 
 /* int64 system_time(); */
 FUNCTION(system_time):
+	// (rdtsc * cv_factor) >> 32.
+
 	movq	cv_factor, %rcx
+	shl		$32, %rcx
 
 	// Load 64-bit TSC into %eax (low), %edx (high).
 	rdtsc
@@ -40,17 +43,19 @@ FUNCTION(system_time):
 	// Multiply by conversion factor, result in %rax (low), %rdx (high).
 	mulq	%rcx
 
-	// Shift the result right by 32 bits.
-	shr		$32, %rax
-	shl		$32, %rdx
-	orq		%rdx, %rax
+	// Conversion factor preshifted by 32, whole result in high.
+	movq	%rdx, %rax
 	ret
 FUNCTION_END(system_time)
 
 
 /* int64 system_time_nsecs(); */
 FUNCTION(system_time_nsecs):
-	// Same algorithm as system_time(), just with a different factor.
+	// Same algorithm as system_time(), but with a different factor.
+	// (rdtsc * cv_factor_nsecs) >> 32.
+	// Cannot pre-shift the factor here, otherwise we may lose the upper
+	// 32 bits.
+
 	movq	cv_factor_nsecs, %rcx
 
 	// Load 64-bit TSC into %eax (low), %edx (high).