PVS2C emits undefined integer bit-operation calls; related primitive attachment errors

[delenius]

Environment

• PVS 8.1, commit 5ce1d3a7cb5c1a458b0ed879930c6fe45f35e88c
• Tag: pvs8.1-master-20260624
• Ubuntu 24.04.4, x86-64
• SBCL 2.2.9
• GCC 13.3.0

Summary

PVS2C emits undefined calls such as u8xor(...) even though the generated header includes integer_bv_ops_c.h, where the corresponding function is named integer_bv_ops__u8xor(...).

This affects the u8, u16, u32, and u64 XOR, AND, OR, and NOT operations.

There are also several related errors in c-primitive-attachments.lisp:

1. The u64xor attachment implements AND instead of XOR.
2. The unary NOT attachments specify two argument types.
3. The u32div attachment is misspelled u32dixv.

Minimal reproducer

Create bitops.pvs:

bitops: THEORY
BEGIN
  x8, y8: VAR uint8
  x16, y16: VAR uint16
  x32, y32: VAR uint32
  x64, y64: VAR uint64

  xor8(x8, y8): uint8 = u8xor(x8, y8)
  and8(x8, y8): uint8 = u8and(x8, y8)
  or8(x8, y8): uint8 = u8or(x8, y8)
  not8(x8): uint8 = u8not(x8)

  xor16(x16, y16): uint16 = u16xor(x16, y16)
  xor32(x32, y32): uint32 = u32xor(x32, y32)
  xor64(x64, y64): uint64 = u64xor(x64, y64)
END bitops

Generate C:

PVS_HOME="$HOME/repos/PVS"

"$PVS_HOME/pvs" -raw -q \
  -E '(progn
        (pvs::pvs2c-theory "bitops")
        (pvs::exit-pvs))'

PVS2C successfully generates:

pvs2c/include/bitops_c.h
pvs2c/src/bitops_c.c

Compile it:

cc -std=c17 -Wall -Werror=implicit-function-declaration \
  -I pvs2c/include \
  -I "$PVS_HOME/lib/pvs2c/include" \
  -c pvs2c/src/bitops_c.c

Actual result

Compilation fails:

error: implicit declaration of function ‘u8xor’
error: implicit declaration of function ‘u8and’
error: implicit declaration of function ‘u8or’
error: implicit declaration of function ‘u8not’
error: implicit declaration of function ‘u16xor’
error: implicit declaration of function ‘u32xor’
error: implicit declaration of function ‘u64xor’

For example, the generated C contains:

result = u8xor(ivar_1, ivar_2);

However, integer_bv_ops_c.h defines:

static inline uint8_t
integer_bv_ops__u8xor(uint8_t x8, uint8_t y8)
{
    return x8 ^ y8;
}

bitops_c.h already includes integer_bv_ops_c.h, so this is not a missing-include problem. The emitted function name does not match the declaration.

Suspected cause

src/groundeval/pvs2ir.lisp includes all integer bit operations in *pvs2ir-primitives*.

pvs2ir-constant creates the primitive IR function using only (id expr), discarding the theory name. The default branch of ir2c-primitive-apply then emits that unqualified name:

(t (list
    (format nil "~a = ~a(~{~a~^, ~})"
            return-var ir-function-name ir-arg-names)))

This bypasses the qualified C attachments registered by def-c-attach-primitive, whose names are constructed as integer_bv_ops__u8xor, etc.

Possible fixes would be:

• Remove these operations from *pvs2ir-primitives* so the normal attached-function path is used; or
• Add explicit ir2c-primitive-apply cases that emit ^, &, |, and ~ directly.

Incorrect u64xor attachment

src/groundeval/c-primitive-attachments.lisp currently contains:

(def-c-attach-primitive "integer_bv_ops" "u64xor" "uint64"
  '(|x64| |y64|) '(|uint64| |uint64|)
  "{return x64 & y64;}")

The body should use ^, not &.

Directly testing the generated attachment with 0xaa and 0xcc produces:

actual=0x88 expected=0x66

This error will become observable if the qualified attachment path is used to fix the primary naming problem.

Incorrect unary-NOT metadata

The four unary NOT attachments each declare one argument but two argument types:

(def-c-attach-primitive "integer_bv_ops" "u8not" "uint8"
  '(|x8|)
  '(|uint8| |uint8|)
  "{return ~x8;}")

The argument-type list should contain one element:

'(|uint8|)

The same issue applies to u16not, u32not, and u64not.

Misspelled u32div attachment

The attachment is registered as:

(def-c-attach-primitive "integertypes" "u32dixv" ...)

The PVS prelude operation is named u32div. Because the attachment name does not match, PVS2C generates a normal external integertypes__u32div implementation instead of using the intended inline attachment.

Expected result

PVS2C-generated C should compile without implicit declarations or compatibility macros. All generated bit operations should have correct semantics for every integer width.