Skip to content

float printing was lossy in 2 places, fix this#1306

Merged
nunoplopes merged 1 commit into
AliveToolkit:masterfrom
regehr:print-floats-accurately-2
Apr 22, 2026
Merged

float printing was lossy in 2 places, fix this#1306
nunoplopes merged 1 commit into
AliveToolkit:masterfrom
regehr:print-floats-accurately-2

Conversation

@regehr
Copy link
Copy Markdown
Contributor

@regehr regehr commented Apr 21, 2026

ok let's try this again. the problem was in to_string(fp) -- this is lossy, it does not faithfully print the value. this patch should result in fully round-trippable float printing.

there was an analogous problem in CEX printing, this fixes that too

@regehr
Copy link
Copy Markdown
Contributor Author

regehr commented Apr 21, 2026

here's an example that justifies both parts of this patch:

define float @test_float_fdiv_pzero_f32_out() #0 {
  %result = fdiv float 0x3810000000000000, -2.000000e+00
  ret float %result
}

attributes #0 = { denormal_fpenv(positivezero|ieee) }

current alive2:

----------------------------------------
define float @test_float_fdiv_pzero_f32_out() {
#0:
  %result = fdiv float 0.000000, -2.000000
  ret float %result
}
=>
define float @test_float_fdiv_pzero_f32_out() nofree noundef willreturn memory(none) {
#0:
  ret float 0.000000
}
Transformation doesn't verify!

ERROR: Value mismatch

NOTE: The counterexample is unique.

Example:

Source:
float %result = #x80400000 (-0.000000000000?)

Target:
Source value: #x80400000 (-0.000000000000?)
Target value: #x00000000 (+0.0)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

alive2 with this patch:

----------------------------------------
define float @test_float_fdiv_pzero_f32_out() {
#0:
  %result = fdiv float 1.1754944e-38, -2e+00
  ret float %result
}
=>
define float @test_float_fdiv_pzero_f32_out() nofree noundef willreturn memory(none) {
#0:
  ret float 0e+00
}
Transformation doesn't verify!

ERROR: Value mismatch

NOTE: The counterexample is unique.

Example:

Source:
float %result = #x80400000 (-5.877472e-39)

Target:
Source value: #x80400000 (-5.877472e-39)
Target value: #x00000000 (+0.0)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

@regehr
Copy link
Copy Markdown
Contributor Author

regehr commented Apr 21, 2026

btw I think it's not LLVM who's wrong on this example, it's us

@nunoplopes nunoplopes merged commit 54899fd into AliveToolkit:master Apr 22, 2026
15 of 16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants