Stream: git-wasmtime

Topic: wasmtime / issue #8380 PCC facts checking failed on some ...

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:38):

feilongjiang added the bug label to Issue #8380.

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:38):

feilongjiang opened issue #8380:

When I run PCC on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

The following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:40):

feilongjiang edited issue #8380:

When I run PCC on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

According to the trace log, I find the following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:41):

feilongjiang edited issue #8380:

When I run PCC on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

According to the trace log, I find the following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:47):

feilongjiang edited issue #8380:

When I run PCC on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 59944, max: 59944 }) subsumes stated fact Some(Range { bit_width: 64, min: 59944, max: 59944 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $8, %v2905l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 8, max: 8 }) subsumes stated fact Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

According to the trace log, I find the following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:48):

feilongjiang edited issue #8380:

When I run PCC on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $59944, %v2906l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 59944, max: 59944 }) subsumes stated fact Some(Range { bit_width: 64, min: 59944, max: 59944 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $8, %v2905l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 8, max: 8 }) subsumes stated fact Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

According to the trace log, I find the following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 06:51):

feilongjiang edited issue #8380:

When I run PCC checks on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $59944, %v2906l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 59944, max: 59944 }) subsumes stated fact Some(Range { bit_width: 64, min: 59944, max: 59944 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $8, %v2905l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 8, max: 8 }) subsumes stated fact Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

According to the trace log, I find the following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 08:44):

abrown commented on issue #8380:

cc: @cfallin

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:05):

feilongjiang commented on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need to mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Any idea about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:16):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need to mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:19):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:39):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions. After that, the fact range of movk may be an alias of the previous vreg, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:42):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:43):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail too.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:43):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail, too.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:46):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg and be overwritten, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail, too.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 12:59):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg and be overwritten, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail, too.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

Edit:
Turns out we should also fix the constant passed to check_constant for movk:

diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index cdc6ca42e..b2dd95577 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -305,7 +305,8 @@ pub(crate) fn check(
             let input = get_fact_or_default(vcode, rn, 64);
             if let Some(input_constant) = input.as_const(64) {
                 let constant = u64::from(imm.bits) << (imm.shift * 16);
-                let constant = input_constant | constant;
+                let mask = 0xFFFF << (imm.shift * 16);
+                let constant = input_constant & !mask | constant;
                 check_constant(ctx, vcode, rd, 64, constant)
             } else {
                 check_output(ctx, vcode, rd, &[], |_vcode| {

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 13:00):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg and be overwritten, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail, too.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

Edit:
Turns out we should also update the constant passed to check_constant for movk:

diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index cdc6ca42e..b2dd95577 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -305,7 +305,8 @@ pub(crate) fn check(
             let input = get_fact_or_default(vcode, rn, 64);
             if let Some(input_constant) = input.as_const(64) {
                 let constant = u64::from(imm.bits) << (imm.shift * 16);
-                let constant = input_constant | constant;
+                let mask = 0xFFFF << (imm.shift * 16);
+                let constant = input_constant & !mask | constant;
                 check_constant(ctx, vcode, rd, 64, constant)
             } else {
                 check_output(ctx, vcode, rd, &[], |_vcode| {

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 13:02):

feilongjiang edited a comment on issue #8380:

Also, find another issue on AArch64 when generating facts for mov instructions:
Currently, movk will generate a fact range by simply orring the old running_value with imm16 << shift [1], but to get the correct fact range, maybe we should use the following snippets:

let mask = 0xFFFF << shift;
running_value &= !mask;
running_value |= imm16 << shift;

For example, for immediate 0x9_ffff_ffff, we need two mov instructions:

  Inst 0: movn %v193, #65526, LSL #32
    v193 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)
  Inst 1: movk %v194, %v193, #0, LSL #48
    v194 ! range(64, 0xffff0009ffffffff, 0xffff0009ffffffff)

The first movn generates the correct fact range as #7593 merged. But for movk, it should be range(64, 0x9ffffffff, 0009ffffffff) since we want to move 0x9_ffff_ffff to the register, right? If the correct fact range is range(64, 0x9ffffffff, 0x9ffffffff), then the later subsume check will fail as 0xffff0009ffffffff can not subsume 0x9ffffffff.

Before https://github.com/bytecodealliance/wasmtime/pull/8173, it will not trigger any error since we only check the range generated by mov instructions (but incorrect fact range). After that, the fact range of movk may be an alias of the previous vreg and be overwritten, which may result in fact range mismatch. E.g.: for the immediate 0xFFFFFFFFFFF0BDC0, the expected fact would be Range { bit_width: 64, min: 0xFFFFFFFFFFF0BDC0, max: 0xFFFFFFFFFFF0BDC0}, but the actual fact is Range { bit_width: 64, min: 0xFFFFFFFFFFFFBDC0, max: 0xFFFFFFFFFFFFBDC0}, then subsume check would fail, too.

Any ideas about that?

  1. https://github.com/bytecodealliance/wasmtime/blob/7daffed81f005bc2fa88d72c44a45a14b91e1566/cranelift/codegen/src/isa/aarch64/lower/isle.rs#L392-L396

Edit:
Turns out we should also update the constant passed to check_constant for movk:

diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index cdc6ca42e..b2dd95577 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -305,7 +305,8 @@ pub(crate) fn check(
             let input = get_fact_or_default(vcode, rn, 64);
             if let Some(input_constant) = input.as_const(64) {
                 let constant = u64::from(imm.bits) << (imm.shift * 16);
-                let constant = input_constant | constant;
+                let mask = 0xFFFF << (imm.shift * 16);
+                let constant = input_constant & !mask | constant;
                 check_constant(ctx, vcode, rd, 64, constant)
             } else {
                 check_output(ctx, vcode, rd, &[], |_vcode| {

view this post on Zulip Wasmtime GitHub notifications bot (Apr 16 2024 at 21:50):

cfallin commented on issue #8380:

PCC isn't actively being worked on right now and we expect some issues when we get back to fuzzing it -- thanks for looking at this! I'd be happy to review a PR with a fix if you have one.

view this post on Zulip Wasmtime GitHub notifications bot (Apr 18 2024 at 20:17):

jameysharp closed issue #8380:

When I run PCC checks on PloyBenchC, I get the following error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

After adding WASMTIME_LOG=trace, the failure was actually caused by the following facts checking:

TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $59944, %v2906l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 59944, max: 59944 }) subsumes stated fact Some(Range { bit_width: 64, min: 59944, max: 59944 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: movl    $8, %v2905l
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 8, max: 8 }) subsumes stated fact Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: Checking facts on inst: lea     71072(%v299), %v2904l
TRACE cranelift_codegen::isa::x64::pcc: compute_addr: Real(ImmReg { simm32: 71072, base: v299, flags: MemFlags { bits: 1921 } }), bits: 32
TRACE cranelift_codegen::machinst::pcc: get_fact_or_default: reg v299 -> Some(Range { bit_width: 64, min: 8, max: 8 })
TRACE cranelift_codegen::isa::x64::pcc: base = Range { bit_width: 64, min: 8, max: 8 }
TRACE cranelift_codegen::ir::pcc: add: Range { bit_width: 64, min: 8, max: 8 } + Range { bit_width: 32, min: 71072, max: 71072 } -> None, add_width: 32
TRACE cranelift_codegen::machinst::pcc: clamp_range: fact None from 32 to 64
TRACE cranelift_codegen::machinst::pcc:  -> clamping to Range { bit_width: 64, min: 0, max: 4294967295 }
TRACE cranelift_codegen::machinst::pcc: checking if derived fact Some(Range { bit_width: 64, min: 0, max: 4294967295 }) subsumes stated fact Some(Range { bit_width: 64, min: 71080, max: 71080 })
INFO cranelift_codegen::ir::pcc: Error checking instruction: lea     71072(%v299), %v2904l
Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Here are the problem facts:

Range { bit_width: 64, min: 8, max: 8 }
Range { bit_width: 32, min: 71072, max: 71072 }

which have different bit_width, adding these two facts return a None fact. And finally check_subsumes_optionals returns an UnsupportedFact error.

According to the trace log, I find the following IRs are suspicious:

block9:
  v4339 ! range(64, 0xea28, 0xea28) = iconst.i32 0xea28
  v2858 ! range(64, 0x8, 0x8) = iconst.i32 8
  v4406 ! range(64, 0x115a0, 0x115a0) = iconst.i32 0x0001_15a0
  v4407 ! range(64, 0x115a8, 0x115a8) = iadd v4406, v2858  ; v4406 = 0x0001_15a0, v2858 = 8

they are all iconst.i32 type but have a 64-bit fact range.
After digging in, I think it may introduced by https://github.com/bytecodealliance/wasmtime/pull/8173, attach_constant_fact creates facts for constants by adding a 64-bit fact regardless of the constant type.

Test Case

PolybenchC 2mm

Steps to Reproduce

First, compile 2mm into wasm with wasi-sdk:

/opt/wasi-sdk/bin/clang -O3 -I utilities -I linear-algebra/kernels/2mm \
  utilities/polybench.c linear-algebra/kernels/2mm/2mm.c \
  -Wl,--export=__heap_base -Wl,--export=__data_end \
  -Wl,--export=malloc -Wl,--export=free \
  -DPOLYBENCH_TIME -o out/2mm.wasm \
  -D_WASI_EMULATED_PROCESS_CLOCKS

Second, run the 2mm.wasm with PCC checking enabled:

~/workspace/wasmtime/target/debug/wasmtime compile -Cpcc=y,parallel-compilation=n 2mm.wasm

Expected Results

PCC facts check passed without error.

Actual Results

Error:

Error: Compilation error: Proof-carrying-code validation error: UnsupportedFact

Versions and Environment

Wasmtime version or commit: latest commit on the main branch (commit id: d53d078)

Operating system: Ubuntu 22.04 LTS

Architecture: x86_64

Extra Info

With the following patch, I can pass the PCC check without error. If it is the root cause, I would like to create a PR to fix that.

@@ -485,7 +487,7 @@ where
     /// Helper to propagate facts on constant values: if PCC is
     /// enabled, then unconditionally add a fact attesting to the
     /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value) {
+    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
         if self.flags.enable_pcc() {
             if let InstructionData::UnaryImm {
                 opcode: Opcode::Iconst,
@@ -493,7 +495,9 @@ where
             } = self.func.dfg.insts[inst]
             {
                 let imm: i64 = imm.into();
-                self.func.dfg.facts[value] = Some(Fact::constant(64, imm as u64));
+                let fact = Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
+                self.func.dfg.facts[value] = fact;
             }
         }
     }

view this post on Zulip Wasmtime GitHub notifications bot (Apr 18 2024 at 20:17):

jameysharp commented on issue #8380:

Now that #8393 is merged, I'm closing this issue because I assume it's fixed, but if you find more bugs you can open a new issue or re-open this one. Thank you!

Last updated: Dec 13 2025 at 21:03 UTC