>Synopsis: a64l should sign-extend its result when long has more than 32 bit >Category: POSIX standard library >Environment: System : OpenBSD 6.2 Details : OpenBSD 6.2 (GENERIC.MP) #134: Tue Oct 3 21:22:29 MDT 2017 [email protected]:/usr/src/sys/arch/amd64/compile/GENERIC.MP
Architecture: OpenBSD.amd64 Machine : amd64 >Description: As per POSIX, a64l is required to sign-extend its result if the type long - which the type of its result - has more than 32 bit. On amd64, the type long is a signed 64 bit integer. Note that this relies on a slightly weird aspect of the POSIX specification: The lower 32 bit of any long are used for l64a and the behavior is unspecified if the value is negative. If long has more than 32 bit, it is never negative, as long as only the lower 32 bit are used! (Note that the glibc implementation guarantees that the behavior is never unspecified by always treating the argument as unsigned.) This allows generating the string "zzzzz1" by giving the (positive) number 2**32-1 to l64a. This in turn ensures that the behavior of a64l is not unspecified, as the string has been generated by a call to l64a. When undoing the conversion, the lower 32 bit of the result are 0xFFFFFFFF which, when sign-extended should yield -1. The exact wording of the POSIX 2008 standard is available at: http://pubs.opengroup.org/onlinepubs/9699919799/functions/a64l.html This behavior was detected using Symbolic Execution techniques developed in the course of the SYMBIOSYS research project at COMSYS, RWTH Aachen University. This research is supported by the European Research Council (ERC) under the EU's Horizon 2020 Research and Innovation Programme grant agreement n. 647295 (SYMBIOSYS). >How-To-Repeat: Compile and run the following C program on/for a machine where long is more than 32 bit, such as amd64: #include <assert.h> #include <stdlib.h> #include <stdint.h> #include <string.h> int main(void) { char const* s = l64a(0xFFFFFFFFu); assert(0 == strcmp(s, "zzzzz1")); // OK long result = a64l(s); long sign_extended = (long)(int32_t)result; assert(sign_extended == result); // FAILS } >Fix: The FreeBSD implementation of a64l (https://svnweb.freebsd.org/base/head/lib/libc/stdlib/a64l.c?view=markup) is only slightly different from the OpenBSD implementation (http://cvsweb.openbsd.org/cgi-bin/cvsweb/src/lib/libc/stdlib/a64l.c?annotate=1.5) and does not exhibit this problem, as it performs the calculation in an int instead of a long. Alternatively, a slightly more clean approach would be to cast the result of the operation to int32_t when returning (which will explicitly show that the result is the sign-extended version of the lower 32 bit of the conversion, as required per POSIX). dmesg: OpenBSD 6.2 (GENERIC.MP) #134: Tue Oct 3 21:22:29 MDT 2017 [email protected]:/usr/src/sys/arch/amd64/compile/GENERIC.MP real mem = 2130640896 (2031MB) avail mem = 2059108352 (1963MB) mpath0 at root scsibus0 at mpath0: 256 targets mainbus0 at root bios0 at mainbus0: SMBIOS rev. 2.5 @ 0xe1000 (10 entries) bios0: vendor innotek GmbH version "VirtualBox" date 12/01/2006 bios0: innotek GmbH VirtualBox acpi0 at bios0: rev 2 acpi0: sleep states S0 S5 acpi0: tables DSDT FACP APIC SSDT acpi0: wakeup devices acpitimer0 at acpi0: 3579545 Hz, 32 bits acpimadt0 at acpi0 addr 0xfee00000: PC-AT compat cpu0 at mainbus0: apid 0 (boot processor) cpu0: Intel(R) Core(TM) i7-4558U CPU @ 2.80GHz, 2800.42 MHz cpu0: FPU,VME,DE,PSE,TSC,MSR,PAE,MCE,CX8,APIC,SEP,MTRR,PGE,MCA,CMOV,PAT,PSE36,CFLUSH,MMX,FXSR,SSE,SSE2,HTT,SSE3,PCLMUL,SSSE3,CX16,SSE4.1,SSE4.2,MOVBE,POPCNT,AES,XSAVE,AVX,RDRAND,NXE,RDTSCP,LONG,LAHF,ABM,ITSC cpu0: 256KB 64b/line 8-way L2 cache cpu0: TSC frequency 2800422180 Hz cpu0: smt 0, core 0, package 0 mtrr: CPU supports MTRRs but not enabled by BIOS cpu0: apic clock running at 1000MHz cpu1 at mainbus0: apid 1 (application processor) cpu1: Intel(R) Core(TM) i7-4558U CPU @ 2.80GHz, 2800.25 MHz cpu1: FPU,VME,DE,PSE,TSC,MSR,PAE,MCE,CX8,APIC,SEP,MTRR,PGE,MCA,CMOV,PAT,PSE36,CFLUSH,MMX,FXSR,SSE,SSE2,HTT,SSE3,PCLMUL,SSSE3,CX16,SSE4.1,SSE4.2,MOVBE,POPCNT,AES,XSAVE,AVX,RDRAND,NXE,RDTSCP,LONG,LAHF,ABM,ITSC cpu1: 256KB 64b/line 8-way L2 cache cpu1: smt 0, core 1, package 0 ioapic0 at mainbus0: apid 2 pa 0xfec00000, version 20, 24 pins , remapped to apid 2 acpiprt0 at acpi0: bus 0 (PCI0) acpicpu0 at acpi0: C1(@1 halt!) acpicpu1 at acpi0: C1(@1 halt!) "PNP0F03" at acpi0 not configured acpibat0 at acpi0: BAT0 model "1" serial 0 type VBOX oem "innotek" acpiac0 at acpi0: AC unit online acpivideo0 at acpi0: GFX0 pci0 at mainbus0 bus 0 pchb0 at pci0 dev 0 function 0 "Intel 82441FX" rev 0x02 pcib0 at pci0 dev 1 function 0 "Intel 82371SB ISA" rev 0x00 pciide0 at pci0 dev 1 function 1 "Intel 82371AB IDE" rev 0x01: DMA, channel 0 configured to compatibility, channel 1 configured to compatibility wd0 at pciide0 channel 0 drive 0: <VBOX HARDDISK> wd0: 128-sector PIO, LBA, 32768MB, 67108864 sectors wd0(pciide0:0:0): using PIO mode 4, Ultra-DMA mode 2 atapiscsi0 at pciide0 channel 1 drive 0 scsibus1 at atapiscsi0: 2 targets cd0 at scsibus1 targ 0 lun 0: <VBOX, CD-ROM, 1.0> ATAPI 5/cdrom removable cd0(pciide0:1:0): using PIO mode 4, Ultra-DMA mode 2 vga1 at pci0 dev 2 function 0 "InnoTek VirtualBox Graphics Adapter" rev 0x00 wsdisplay0 at vga1 mux 1: console (80x25, vt100 emulation) wsdisplay0: screen 1-5 added (80x25, vt100 emulation) em0 at pci0 dev 3 function 0 "Intel 82540EM" rev 0x02: apic 2 int 19, address 08:00:27:06:5c:f1 "InnoTek VirtualBox Guest Service" rev 0x00 at pci0 dev 4 function 0 not configured auich0 at pci0 dev 5 function 0 "Intel 82801AA AC97" rev 0x01: apic 2 int 21, ICH ac97: codec id 0x83847600 (SigmaTel STAC9700) audio0 at auich0 ohci0 at pci0 dev 6 function 0 "Apple Intrepid USB" rev 0x00: apic 2 int 22, version 1.0 piixpm0 at pci0 dev 7 function 0 "Intel 82371AB Power" rev 0x08: apic 2 int 23 iic0 at piixpm0 isa0 at pcib0 isadma0 at isa0 pckbc0 at isa0 port 0x60/5 irq 1 irq 12 pckbd0 at pckbc0 (kbd slot) wskbd0 at pckbd0: console keyboard, using wsdisplay0 pms0 at pckbc0 (aux slot) wsmouse0 at pms0 mux 0 pcppi0 at isa0 port 0x61 spkr0 at pcppi0 usb0 at ohci0: USB revision 1.0 uhub0 at usb0 configuration 1 interface 0 "Apple OHCI root hub" rev 1.00/1.00 addr 1 vscsi0 at root scsibus2 at vscsi0: 256 targets softraid0 at root scsibus3 at softraid0: 256 targets root on wd0a (61c6ce69bd397a01.a) swap on wd0b dump on wd0b usbdevs: Controller /dev/usb0: addr 1: full speed, self powered, config 1, OHCI root hub(0x0000), Apple(0x106b), rev 1.00 port 1 powered port 2 powered port 3 powered port 4 powered port 5 powered port 6 powered port 7 powered port 8 powered port 9 powered port 10 powered port 11 powered port 12 powered
