I am looking at the diff between the host and guest CPUID, and we have a few candidates: CPUID[4] is all zeroes on the host, and the host has CPUID leaves up to 0x8000001f available, including CPUID[0x8000001d] (which contains cache topology information).  Probably we need to implement CPUID[0x8000001d], I will take a look at Linux code to find out if that's all we need.

Full CPUID diff below:

--- /tmp/host-x86info.txt       2017-07-25 15:01:26.753304233 -0300
+++ /tmp/guest-x86info.txt      2017-07-25 15:01:33.563335744 -0300
@@ -1,29 +1,29 @@
 eax in: 0x00000000, eax = 0000000d ebx = 68747541 ecx = 444d4163 edx = 69746e65
-eax in: 0x00000001, eax = 00800f11 ebx = 00100800 ecx = 7ed8320b edx = 178bfbff
-eax in: 0x00000002, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
+eax in: 0x00000001, eax = 00800f11 ebx = 00080800 ecx = ffd83203 edx = 178bfbff
+eax in: 0x00000002, eax = 00000001 ebx = 00000000 ecx = 0000004d edx = 002c307d
 eax in: 0x00000003, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x00000004, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x00000005, eax = 00000040 ebx = 00000040 ecx = 00000003 edx = 00000000
-eax in: 0x00000006, eax = 00000004 ebx = 00000000 ecx = 00000001 edx = 00000000
-eax in: 0x00000007, eax = 00000000 ebx = 209c01a9 ecx = 00000000 edx = 00000000
+eax in: 0x00000004, eax = 0c000121 ebx = 01c0003f ecx = 0000003f edx = 00000001
+eax in: 0x00000005, eax = 00000000 ebx = 00000000 ecx = 00000003 edx = 00000000
+eax in: 0x00000006, eax = 00000004 ebx = 00000000 ecx = 00000000 edx = 00000000
+eax in: 0x00000007, eax = 00000000 ebx = 209c01ab ecx = 00000000 edx = 00000000
 eax in: 0x00000008, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x00000009, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x0000000a, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x0000000b, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
+eax in: 0x0000000b, eax = 00000001 ebx = 00000002 ecx = 00000100 edx = 00000000
 eax in: 0x0000000c, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x0000000d, eax = 00000007 ebx = 00000340 ecx = 00000340 edx = 00000000
 
-eax in: 0x80000000, eax = 8000001f ebx = 68747541 ecx = 444d4163 edx = 69746e65
-eax in: 0x80000001, eax = 00800f11 ebx = 20000000 ecx = 35c233ff edx = 2fd3fbff
+eax in: 0x80000000, eax = 8000001a ebx = 68747541 ecx = 444d4163 edx = 69746e65
+eax in: 0x80000001, eax = 00800f11 ebx = 00000000 ecx = 000003f3 edx = 2fd3fbff
 eax in: 0x80000002, eax = 20444d41 ebx = 657a7952 ecx = 2037206e edx = 30303731
 eax in: 0x80000003, eax = 67694520 ebx = 432d7468 ecx = 2065726f edx = 636f7250
 eax in: 0x80000004, eax = 6f737365 ebx = 20202072 ecx = 20202020 edx = 00202020
-eax in: 0x80000005, eax = ff40ff40 ebx = ff40ff40 ecx = 20080140 edx = 40040140
-eax in: 0x80000006, eax = 26006400 ebx = 66006400 ecx = 02006140 edx = 00808140
-eax in: 0x80000007, eax = 00000000 ebx = 0000001b ecx = 00000000 edx = 00006599
-eax in: 0x80000008, eax = 00003030 ebx = 00000007 ecx = 0000400f edx = 00000000
+eax in: 0x80000005, eax = 01ff01ff ebx = 01ff01ff ecx = 40020140 edx = 40020140
+eax in: 0x80000006, eax = 00000000 ebx = 42004200 ecx = 02008140 edx = 00808140
+eax in: 0x80000007, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
+eax in: 0x80000008, eax = 00003028 ebx = 00000000 ecx = 00000007 edx = 00000000
 eax in: 0x80000009, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x8000000a, eax = 00000001 ebx = 00008000 ecx = 00000000 edx = 0001bcff
+eax in: 0x8000000a, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x8000000b, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x8000000c, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x8000000d, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
@@ -38,10 +38,5 @@
 eax in: 0x80000016, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x80000017, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
 eax in: 0x80000018, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x80000019, eax = f040f040 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x8000001a, eax = 00000003 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x8000001b, eax = 000003ff ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x8000001c, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
-eax in: 0x8000001d, eax = 00004121 ebx = 01c0003f ecx = 0000003f edx = 00000000
-eax in: 0x8000001e, eax = 00000000 ebx = 00000100 ecx = 00000000 edx = 00000000
-eax in: 0x8000001f, eax = 00000007 ebx = 0000016f ecx = 0000000f edx = 00000000
+eax in: 0x80000019, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000
+eax in: 0x8000001a, eax = 00000000 ebx = 00000000 ecx = 00000000 edx = 00000000