diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,36 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.17, 2026-08-10 +* Latest Hackage released version: 3.18, 2026-08-13 + +### Version 3.18, 2026-08-13 + + * Add a Tcl/Tk GUI (`GUI/tclGUI/crackNum.tcl`) that works on Linux and macOS. + When `--gui` is used on Linux, `crackNum` now launches this interface + (requires `wish`) instead of erroring out. + + * The Tcl/Tk GUI script is now a cabal data-file, so it is installed along + with the binary: `cabal install crackNum` is enough for `crackNum --gui` to + work on Linux, with no PATH setup. To run a different copy of the script, + set `CRACKNUM_TCL`, or put it on your PATH as `crackNum.tcl`. + + * Both GUIs now expose the number of lanes (`-l`), so multi-lane decoding is + reachable from the graphical interface, and `--gui -l4 ...` is honored + rather than silently dropped. + + * Both front-ends now live under `GUI/`: the macOS app moved from `gui/` to + `GUI/swiftGUI/`, and the Tcl/Tk script to `GUI/tclGUI/`. + + * Encoding a NaN now always displays the canonical quiet-NaN pattern (sign 0, + all-ones exponent, leading significand bit set; `0x7FC00000` for a single). + SMTLib's floating-point sort has a single NaN value, so the solver returns an + abstract NaN and the concrete bit-pattern shown was whatever the model + materialized -- which could differ between solver/library versions. The + E4M3 path already pinned its NaN this way; the rest now do too. + + * Exponent/significand sizes of 1 bit are accepted by `-f`, but the solver + requires at least 2 of each. This now produces a regular error message + instead of an uncaught exception with a backtrace. ### Version 3.17, 2026-08-10 diff --git a/GUI/tclGUI/README.md b/GUI/tclGUI/README.md new file mode 100644 --- /dev/null +++ b/GUI/tclGUI/README.md @@ -0,0 +1,91 @@ +# CrackNum Tcl/Tk GUI + +A cross-platform GUI for [crackNum](https://github.com/LeventErkok/crackNum), written in Tcl/Tk. +Works on Linux and macOS anywhere `wish` (Tk 8.6+) is available. + +## Requirements + +- `crackNum` on your PATH +- `z3` on your PATH +- `wish` (Tk 8.6+) + +On NixOS / Nix: + +```bash +nix profile install nixpkgs#tk +``` + +On Debian/Ubuntu: + +```bash +sudo apt install tk +``` + +On RHEL/Fedora/Rocky: + +```bash +sudo dnf install tk +``` + +## Installation + +Nothing to do: this script is a cabal data-file, so `cabal install crackNum` +puts it on disk next to the binary, and `crackNum --gui` finds it there. + +If you do not have it — say you only have the binary, or you moved it — get the +sources with either of: + +```bash +cabal get crackNum +git clone http://github.com/LeventErkok/crackNum.git +``` + +### Running a different copy + +`crackNum` looks for the script in three places, first match wins: + +| Order | Location | Use it for | +|-------|--------------------------------------|-----------------------------------| +| 1 | `$CRACKNUM_TCL` | pointing at an explicit file | +| 2 | `crackNum.tcl` on your PATH | shadowing with a checkout | +| 3 | the copy installed with the package | the normal case; nothing to set | + +So to test a modified script: + +```bash +export CRACKNUM_TCL=/path/to/crackNum/GUI/tclGUI/crackNum.tcl +``` + +or put its directory on your PATH (the script must be executable for this route): + +```bash +export PATH=/path/to/crackNum/GUI/tclGUI:$PATH +``` + +When working inside a checkout, `cabal run crackNum -- --gui` also works: cabal +sets `crackNum_datadir` so the in-tree copy is used. + +## Usage + +Launch via the `crackNum` binary: + +```bash +crackNum --gui +crackNum --gui -fsp 2.5 +crackNum --gui -w32 0xDEADBEEF +``` + +Or directly with `wish`: + +```bash +wish crackNum.tcl +wish crackNum.tcl -fsp 2.5 +``` + +## Keyboard shortcuts + +| Key | Action | +|----------|-----------------| +| Ctrl+W | Close window | +| Ctrl+Q | Quit | +| Return | Crack the value | diff --git a/GUI/tclGUI/crackNum.tcl b/GUI/tclGUI/crackNum.tcl new file mode 100644 --- /dev/null +++ b/GUI/tclGUI/crackNum.tcl @@ -0,0 +1,524 @@ +#!/usr/bin/env wish +# CrackNum GUI — Tcl/Tk front-end for the crackNum command-line tool. +# Works on Linux and macOS. Requires wish (Tk 8.5+) and crackNum on PATH. + +# --------------------------------------------------------------------------- +# Tool discovery +# --------------------------------------------------------------------------- + +proc locate {name} { + set path [split [expr { + [info exists ::env(PATH)] ? $::env(PATH) : "/usr/bin:/bin" + }] :] + foreach dir $path { + set candidate [file join $dir $name] + if {[file executable $candidate]} { return $candidate } + } + return "" +} + +set CRACKNUM [locate crackNum] +set Z3 [locate z3] + +# --------------------------------------------------------------------------- +# Format table +# --------------------------------------------------------------------------- +# Each entry: {id label flag_kind flag_arg} +# flag_kind = fixed | customFloat | word | customWord | int | customInt +# flag_arg = the flag suffix for "fixed", or bit-count for "word"/"int" + +set FORMAT_SECTIONS { + {"Float" { + {ffp4 "FP4 (E2M1)" fixed fp4} + {fe4m3 "FP8 (E4M3)" fixed e4m3} + {fe5m2 "FP8 (E5M2)" fixed e5m2} + {fhp "Half" fixed hp} + {fbp "Brain" fixed bp} + {fsp "Single" fixed sp} + {fdp "Double" fixed dp} + {fcs "Custom" customFloat {}} + }} + {"Word (Unsigned)" { + {w8 "8-bit" word 8} + {w16 "16-bit" word 16} + {w32 "32-bit" word 32} + {w64 "64-bit" word 64} + {wcs "Custom" customWord {}} + }} + {"Integer (Signed)" { + {i8 "8-bit" int 8} + {i16 "16-bit" int 16} + {i32 "32-bit" int 32} + {i64 "64-bit" int 64} + {ics "Custom" customInt {}} + }} +} + +set ROUNDING_MODES {RNE RNA RTP RTN RTZ} +array set ROUNDING_LABELS { + RNE "RNE (Nearest, ties to even)" + RNA "RNA (Nearest, ties to away)" + RTP "RTP (Toward +∞)" + RTN "RTN (Toward -∞)" + RTZ "RTZ (Toward 0)" +} + +# --------------------------------------------------------------------------- +# State +# --------------------------------------------------------------------------- +set state(selection) "" ;# selected format id +set state(value) "" +set state(rounding) "RNE" +set state(lanes) 1 +set state(bitWidth) 64 +set state(expWidth) 11 +set state(fontSize) 11 + +set WELCOME {Enter a value above, then pick a format on the left to crack it. + +You can: + - ENCODE: from a mathematical value to its internal representation + - DECODE: from an internal representation to its mathematical value + +Encoding: + - Enter a decimal value (2.5, -4.1e5) or hex float (0x2.4p3). + - You can pass NaN, Inf, -0, -Inf for special values. + - For floats, pick a rounding mode. + - Input must NOT start with 0x, 0b, or N'h (else we decode instead). + +Decoding: + - Use hex (0x), binary (0b), or Verilog (N'h) notation. + - You may use _, - or space as separators for readability. + - Verilog input longer than the format is decoded as SIMD lanes.} + +# --------------------------------------------------------------------------- +# Build the precision flag from the selected format +# --------------------------------------------------------------------------- +proc precisionFlag {} { + global state FORMAT_SECTIONS + + set sel $state(selection) + if {$sel eq ""} { return "" } + + foreach section $FORMAT_SECTIONS { + foreach fmt [lindex $section 1] { + lassign $fmt id label kind arg + if {$id ne $sel} continue + + switch $kind { + fixed { return "-f$arg" } + word { return "-w$arg" } + int { return "-i$arg" } + customWord { return "-w$state(bitWidth)" } + customInt { return "-i$state(bitWidth)" } + customFloat { + # Only check that the widths describe a well-formed layout; crackNum + # itself owns the remaining limits (and reports solver restrictions + # readably). + set bw $state(bitWidth) + set ew $state(expWidth) + set sig [expr {$bw - $ew - 1}] + if {$ew < 1 || $sig < 0} { + return [list invalid \ +"Invalid custom FP format: + Total width: $bw + Sign : 1 + Exponent : [format %4d $ew] + Significand: [format %4d $sig] (Total = Sign + Exponent + Significand) + +Exponent must be at least 1 bit, and the total width must leave room for it and the sign."] + } + return "-f${ew}+[expr {$bw - $ew}]" + } + } + } + } + return "" +} + +# --------------------------------------------------------------------------- +# Run crackNum and return output text +# --------------------------------------------------------------------------- +proc runCrackNum {} { + global state CRACKNUM Z3 + + if {$CRACKNUM eq ""} { + return "crackNum: Cannot locate the 'crackNum' binary on your PATH.\n\nMake sure it is installed and reachable (e.g. `which crackNum` works in your terminal)." + } + if {$Z3 eq ""} { + return "crackNum: Cannot locate the 'z3' binary on your PATH.\n\nMake sure it is installed and reachable (e.g. `which z3` works in your terminal)." + } + + set flagResult [precisionFlag] + if {$flagResult eq ""} { return "" } + + if {[lindex $flagResult 0] eq "invalid"} { + return [lindex $flagResult 1] + } + + set flag $flagResult + set rm "-r$state(rounding)" + set val [expr {$state(value) eq "" ? "0" : $state(value)}] + + # Pass SBV_Z3 so crackNum finds z3 even when PATH is minimal. + set savedZ3 [expr {[info exists ::env(SBV_Z3)] ? $::env(SBV_Z3) : ""}] + set ::env(SBV_Z3) $Z3 + + set cmd [list $CRACKNUM $flag $rm] + # Only pass -l when it's actually multi-lane: giving -l1 explicitly would + # suppress crackNum's lane inference for Verilog (N'h) input. + if {[string is integer -strict $state(lanes)] && $state(lanes) > 1} { + lappend cmd -l$state(lanes) + } + lappend cmd -- $val + + # 2>@1 folds stderr into the captured result, so errors show up in the pane. + set rc [catch {exec {*}$cmd 2>@1} output] + + if {$savedZ3 eq ""} { unset -nocomplain ::env(SBV_Z3) } \ + else { set ::env(SBV_Z3) $savedZ3 } + + if {$rc && ![string match "*ENCODED*" $output] && ![string match "*DECODED*" $output]} { + append output "\n\n** Call to crackNum failed! Make sure the value makes sense for the chosen format." + append output "\n**" + append output "\n** Run: $cmd" + append output "\n**" + append output "\n** Value : $val" + } + return $output +} + +# --------------------------------------------------------------------------- +# Show output in the text widget +# --------------------------------------------------------------------------- +proc showOutput {text} { + .output configure -state normal + .output delete 1.0 end + .output insert end $text + .output configure -state disabled +} + +proc crack {} { + global state FORMAT_SECTIONS + + set sel $state(selection) + if {$sel eq ""} return + + set out [runCrackNum] + + # Determine label for header + set label "" + foreach section $FORMAT_SECTIONS { + foreach fmt [lindex $section 1] { + if {[lindex $fmt 0] eq $sel} { set label [lindex $fmt 1] } + } + } + + if {[string match "*ENCODED*" $out]} { set kind "Encoding in format" } \ + elseif {[string match "*DECODED*" $out]} { set kind "Decoded using format" } \ + else { set kind "Format" } + + showOutput "\[$kind: $label\]\n\n$out" +} + +# --------------------------------------------------------------------------- +# Font size helpers +# --------------------------------------------------------------------------- +proc applyFontSize {} { + global state + .output configure -font [list Courier $state(fontSize)] +} + +proc zoomIn {} { incr ::state(fontSize); applyFontSize } +proc zoomOut {} { + if {$::state(fontSize) > 6} { incr ::state(fontSize) -1; applyFontSize } +} + +# --------------------------------------------------------------------------- +# Build UI +# --------------------------------------------------------------------------- + +wm title . "CrackNum" +wm minsize . 1200 700 +wm geometry . 1200x700 + +image create photo appIcon -data { +iVBORw0KGgoAAAANSUhEUgAAACAAAAAgCAYAAABzenr0AAAFzklEQVRYhc1X60+TdxT28mVfddOh +TFARUdZybaHlWmkLtLUUWu69QaH0BrSlXFqhDAtYlIuIQXQaN7dodF6mc8sUjDNZXLboZGYmi38D +/8AmH569v9LC2/atEE2WvcmTc85zznPOeW9p302b/s8HgM0Utr4nNr/L4A98099xbf1faFt7Llha +XJ9b3wVES3qQXqTnhs547tJDVmXz1EKBYgg50n7kSPrDrXSAFgd9abifG/DX6goUn6Gi6dT8xIX7 +h956RUiBuHZ4iSvxgFPuBrfcE4YoTrLG03ORMUGO5BhEtb4lcoIxL7tcc2KeW96H7NLeMHBCtqw3 +KkfnOTFqQnrSu0LrX2C8Hd6J61yepA9ZIheyxN1BS/MjYzofyq36sfU8qRtkVtS9N7vmtJlCJzJK +HCCW7q9xjoAfzTPVxtaTWWHPAhVs0dgmLelHOpFBIZ0RHaDnI+ti8Ux6Mou8ovQFtqqtE9a0YhsI +2EH7NqzWCNqjNOvp1aYJK+MC7CILQmAVmgNgF67FbAImn2Y3olebTjIsYPRbU/NaQHCYv2ID4Edw +/DWfXhfLZ9I3tIxEL9BgHLEe5jXjEK8JXTUOqKQWdMwuQmacQ2nTGbT6f4L/wT/QeO9Tr5oLw69u +oW7MD6GpD1WDPnieXoX97kVIu70QW93Qz01h5PUdaM9OQmRyQ+oaCPQmYF6AIlNytEjJ1aGryobq +MhPMM3+gvOUcRPpp6Eef4PgPy6gf+B6ZYgeO/XkdSv8IjrR1Q/7ZELp/uQLz3TmUdfejxNwD9dwE +Bl/fRP3MSRwxdaPMdQyB/jk61DUNMS0wZD3IUYPAKW9DtciA5qlFCA2zEGhOo973GO57y1B67iND +1Imul1+j4sQQClsdkHgH0P7zJTTfmYHQ2Yfiti7UzPrR89dVqM6MoqjNiRJHL5JJf66aWsAbvQAh +k7PrcYCCXWKAUqCDevwFinVnUdAwCdXgI9hvvYG89x7YAhusi5dRPjyAvJZOCD1uGJ6cR+PtKRTb +Xchv64RiZhi2V19Cfvo4+C12FHW6kJzdEOhfreuPXoCQSZm1SMqoQWeZHlVFGtSPPUeh9gz49eNQ +DDyC7Ztl6h7fBavYAuOLixD7POA121Di6YH+ySzqbo6joMMBfms7js4ch/nVZUgnB8EztAf4pMwa +kBlKtZt5gf3pSuxPV6FD2AhFXh2qRn8Hv/E0cqvHIPUswHBtGWLHt0gtNEHz7BwEQz3I1rehsK8L +dY+nobhxAjxbOzgGE0qnvdC9PA/ROPXj1GwK8KT3PmoG8wIUuY9dib1sBdqLalHBU0HqewZu7SQ4 +Kj9EPQ/ReOUNBB23kZLfCtVv08gfdCBd2wp+TwcUj8ZRfs0HjsWMDL0Rgkk3ahbPomisF5lUnG22 +UL0rA1Coe6MXUKpd1sRP5SCw5lVBxq2EcOBXZKpOIk0xgiLnj6i89Df4lhs4QL1K0qenwO3vAKtB +hyynGaUPRiH4yosMoxFsrQH8Uy7Ink+CN+oES6NHmrE10DuRVQFFgyt6AQW1QEKqDHtSpdhzeAUk +TkgNWRmNW6mj86HcRvTMCzQ4rfEHxYhPoXAwGrtj+FGaDehldfboBeQUuetACQh2JwtXLM2nx5F8 +KLdRvay6PWqBLRKV2bIrSYC4/cWIoyzdJ3Y1DoHOR9asoyezIhfYXKN1aD/eV4gA9gYtDTsZuJi5 +dfRkVtSfU7vLx41PLsaOxDzsSMgL2J2J+StxYigOt0w16+nJDDJrU+RB/ihm8ZULOxL5+GgPj0Ju +EDyqIS1OCM+Fc7ygz6wnNoNXNR/zG2F0fI6VzBItffgJFyFsj+dE2TAunhvm0/N0HUFymnjJMzRx +iHF46FkgBWyOdD4ukYdtu7OwnQLdbtu14m+n+cSu+rS6kC5uLw+ZuUcXyAlu6FONXCKr3ctV1pi1 +IonGUirXWQOQBW2kH4lgjmhJD9JrQ59mTFeEvKLv8WG65Z0+Tv/L419cdFY2wXUZTgAAAABJRU5E +rkJggg== +} +wm iconphoto . appIcon + +# ---- Menu bar ------------------------------------------------------------ +menu .mb -tearoff 0 +. configure -menu .mb + +menu .mb.file -tearoff 0 +.mb add cascade -label "File" -menu .mb.file -underline 0 +.mb.file add command -label "Close" -accelerator "Ctrl+W" -command { destroy . } +bind . { destroy . } +bind . { destroy . } + +menu .mb.edit -tearoff 0 +.mb add cascade -label "Edit" -menu .mb.edit -underline 0 +.mb.edit add command -label "Cut" -accelerator "Ctrl+X" -command { event generate [focus] <> } +.mb.edit add command -label "Copy" -accelerator "Ctrl+C" -command { event generate [focus] <> } +.mb.edit add command -label "Paste" -accelerator "Ctrl+V" -command { event generate [focus] <> } +.mb.edit add separator +.mb.edit add command -label "Select All" -accelerator "Ctrl+A" -command { event generate [focus] <> } + +# ---- Top bar: zoom, help, value entry ------------------------------------ +frame .top +pack .top -fill x -padx 8 -pady 6 + +foreach {fr txt fnt cmd} { + .top.zf1 "A" {TkDefaultFont 8} zoomOut + .top.zf2 "A" {TkDefaultFont 14} zoomIn +} { + frame $fr -width 28 -height 28 + pack propagate $fr 0 + button $fr.b -text $txt -font $fnt -command $cmd + pack $fr.b -fill both -expand yes + pack $fr -side left -padx 2 +} +button .top.help -text "?" -command { showOutput $::WELCOME } +pack .top.help -side left -padx 2 + +entry .top.val -textvariable state(value) -font {Courier 11} -width 28 +pack .top.val -side right -padx {0 4} +bind .top.val crack + +label .top.lbl -text "Value:" +pack .top.lbl -side right -padx {4 2} + +# ---- Main pane: sidebar + output ---------------------------------------- +frame .main +pack .main -fill both -expand yes -padx 8 -pady {0 8} + +# Sidebar +frame .main.side -width 240 +pack .main.side -side left -fill y -padx {0 6} +pack propagate .main.side 0 + +# Format list +ttk::style configure Treeview -rowheight 22 +ttk::style configure Treeview.Item -padding {4 0} + +ttk::treeview .main.side.lb -selectmode browse -show tree -height 18 +pack .main.side.lb -fill both -expand yes + +.main.side.lb tag configure hdr -font {TkDefaultFont 9 bold} +.main.side.lb tag configure item -font {TkDefaultFont 9} + +# Populate treeview; build item-id <-> format-id mappings +array set ITEM_FMT {} ;# treeview item id -> format id +array set FMT_ITEM {} ;# format id -> treeview item id + +foreach section $FORMAT_SECTIONS { + set title [lindex $section 0] + set sid [.main.side.lb insert {} end -text $title -open yes -tags hdr] + foreach fmt [lindex $section 1] { + set fid [lindex $fmt 0] + set iid [.main.side.lb insert $sid end -text [lindex $fmt 1] -tags item] + set ITEM_FMT($iid) $fid + set FMT_ITEM($fid) $iid + } +} + +bind .main.side.lb <> { + set sel [.main.side.lb selection] + if {$sel ne "" && [info exists ITEM_FMT($sel)]} { + set state(selection) $ITEM_FMT($sel) + crack + } else { + .main.side.lb selection remove $sel + } +} + +# Rounding +frame .main.side.rm +pack .main.side.rm -fill x -pady {6 0} +label .main.side.rm.lbl -text "Rounding mode:" -anchor w +pack .main.side.rm.lbl -fill x +ttk::combobox .main.side.rm.cb -state readonly -width 28 +pack .main.side.rm.cb -fill x + +foreach rm {RNE RNA RTP RTN RTZ} { lappend rm_labels $::ROUNDING_LABELS($rm) } +.main.side.rm.cb configure -values $rm_labels +# Show the full label in the combo but store the code in state(rounding) +proc rmLabel2Code {label} { + foreach rm {RNE RNA RTP RTN RTZ} { + if {$::ROUNDING_LABELS($rm) eq $label} { return $rm } + } + return RNE +} +proc rmCode2Label {code} { return $::ROUNDING_LABELS($code) } +.main.side.rm.cb set [rmCode2Label $state(rounding)] +bind .main.side.rm.cb <> { + set state(rounding) [rmLabel2Code [.main.side.rm.cb get]] + crack +} + +# Lanes (decoding only; crackNum rejects -l when encoding) +frame .main.side.ln +pack .main.side.ln -fill x -pady {6 0} +label .main.side.ln.l -text "Lanes:" +pack .main.side.ln.l -side left +entry .main.side.ln.e -textvariable state(lanes) -width 6 -justify right \ + -font {Courier 11} +pack .main.side.ln.e -side right +bind .main.side.ln.e crack + +label .main.side.ln2 \ + -text "(lanes apply to decoding only)" \ + -font {TkDefaultFont 8} -foreground gray -wraplength 200 -justify left +pack .main.side.ln2 -fill x + +# Custom parameters +labelframe .main.side.custom -text "Custom parameters" -padx 4 -pady 4 +pack .main.side.custom -fill x -pady {8 0} + +frame .main.side.custom.bw +pack .main.side.custom.bw -fill x -pady 2 +label .main.side.custom.bw.l -text "Total width:" +pack .main.side.custom.bw.l -side left +entry .main.side.custom.bw.e -textvariable state(bitWidth) -width 6 -justify right \ + -font {Courier 11} +pack .main.side.custom.bw.e -side right +bind .main.side.custom.bw.e crack + +frame .main.side.custom.ew +pack .main.side.custom.ew -fill x -pady 2 +label .main.side.custom.ew.l -text "Exponent width:" +pack .main.side.custom.ew.l -side left +entry .main.side.custom.ew.e -textvariable state(expWidth) -width 6 -justify right \ + -font {Courier 11} +pack .main.side.custom.ew.e -side right +bind .main.side.custom.ew.e crack + +label .main.side.custom.note \ + -text "(exponent width applies to custom floats)" \ + -font {TkDefaultFont 8} -foreground gray -wraplength 200 -justify left +pack .main.side.custom.note -fill x -pady {4 0} + +# Output pane +frame .main.out +pack .main.out -side left -fill both -expand yes + +text .output -state disabled -wrap none \ + -font [list Courier $state(fontSize)] \ + -padx 8 -pady 8 \ + -xscrollcommand {.main.out.sx set} \ + -yscrollcommand {.main.out.sy set} +scrollbar .main.out.sy -orient vertical -command {.output yview} +scrollbar .main.out.sx -orient horizontal -command {.output xview} + +grid .output .main.out.sy -in .main.out -sticky nsew +grid .main.out.sx -in .main.out -sticky ew +grid columnconfigure .main.out 0 -weight 1 +grid rowconfigure .main.out 0 -weight 1 + +# --------------------------------------------------------------------------- +# Parse crackNum-style command-line args (forwarded by `crackNum --gui ...`) +# --------------------------------------------------------------------------- +proc parseArgs {argv} { + global state FORMAT_SECTIONS FMT_ITEM + + set values {} + set i 0 + while {$i < [llength $argv]} { + set a [lindex $argv $i] + if {$a eq "--"} { + lappend values {*}[lrange $argv [expr {$i+1}] end] + break + } + if {[string match "-f*" $a]} { + set v [string tolower [string range $a 2 end]] + switch $v { + sp { set state(selection) fsp } + dp { set state(selection) fdp } + hp { set state(selection) fhp } + bp { set state(selection) fbp } + e4m3 { set state(selection) fe4m3 } + e5m2 { set state(selection) fe5m2 } + fp4 { set state(selection) ffp4 } + default { + if {[regexp {^(\d+)\+(\d+)$} $v _ e s]} { + set state(selection) fcs + set state(expWidth) $e + set state(bitWidth) [expr {$e + $s}] + } + } + } + } elseif {[string match "-w*" $a]} { + set v [string range $a 2 end] + if {$v in {8 16 32 64}} { set state(selection) w$v } \ + elseif {[string is integer -strict $v] && $v > 0} { + set state(selection) wcs + set state(bitWidth) $v + } + } elseif {[string match "-i*" $a]} { + set v [string range $a 2 end] + if {$v in {8 16 32 64}} { set state(selection) i$v } \ + elseif {[string is integer -strict $v] && $v > 0} { + set state(selection) ics + set state(bitWidth) $v + } + } elseif {[string match "-r*" $a]} { + set rm [string toupper [string range $a 2 end]] + if {$rm in {RNE RNA RTP RTN RTZ}} { set state(rounding) $rm } + } elseif {[string match "-l*" $a]} { + set v [string range $a 2 end] + if {[string is integer -strict $v] && $v > 0} { set state(lanes) $v } + } elseif {![string match "-*" $a]} { + lappend values $a + } + incr i + } + if {[llength $values]} { set state(value) [join $values " "] } + + # Sync treeview selection highlight + if {$state(selection) ne "" && [info exists FMT_ITEM($state(selection))]} { + set iid $FMT_ITEM($state(selection)) + .main.side.lb selection set $iid + .main.side.lb see $iid + } + + # Sync rounding combo label. Must happen even when no format was given: + # `crackNum --gui -rRTZ` sets state(rounding) but leaves no selection. + .main.side.rm.cb set [rmCode2Label $state(rounding)] +} + +# --------------------------------------------------------------------------- +# Start +# --------------------------------------------------------------------------- +showOutput $WELCOME +parseArgs $argv +if {$state(selection) ne ""} { crack } +focus .top.val +.top.val icursor end diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -115,35 +115,48 @@ Hex: 0x1.f18p-8 ``` -### Graphical interface (macOS, optional) +### Graphical interface (optional) -Optionally, crackNum comes with a native macOS GUI: pick a format on the left, -type a value, and see the encoding/decoding in detail. It is entirely optional — -crackNum is fully functional as a command-line tool without it. The GUI is just -a thin front-end that calls the `crackNum` binary underneath, so it supports -exactly the same formats. +Optionally, crackNum comes with a GUI: pick a format on the left, type a value, +and see the encoding/decoding in detail. It is entirely optional — crackNum is +fully functional as a command-line tool without it. The GUI is just a thin +front-end that calls the `crackNum` binary underneath, so it supports exactly +the same formats. -![crackNum macOS GUI](https://raw.githubusercontent.com/LeventErkok/crackNum/master/crackNumGUI.png) +![crackNum GUI](https://raw.githubusercontent.com/LeventErkok/crackNum/master/crackNumGUI.png) -Building it requires the Swift compiler that comes with the Xcode Command Line -Tools (`xcode-select --install`). From a checkout of this repository: +**macOS** — a native Swift/AppKit app (`GUI/swiftGUI/`). Building requires the +Swift compiler that comes with the Xcode Command Line Tools +(`xcode-select --install`): ``` -$ cd gui +$ cd GUI/swiftGUI $ make install # builds CrackNum.app and copies it into /Applications ``` -Once installed, launch it from Spotlight/Launchpad, or straight from the -command line via the `--gui` option, which forwards any format/rounding flags -and value to the app: +**Linux** — a Tcl/Tk script (`GUI/tclGUI/crackNum.tcl`). The script ships with the +package and is installed alongside the binary, so there is nothing to build; you +only need `wish` (Tk 8.6+): ``` +$ nix profile install nixpkgs#tk # or: sudo apt install tk / sudo dnf install tk +``` + +Then `crackNum --gui` just works. If you want to run a modified copy of the +script, either put it on your PATH as `crackNum.tcl`, or point at it directly +with `CRACKNUM_TCL=/path/to/crackNum.tcl`. See +[`GUI/tclGUI/README.md`](GUI/tclGUI/README.md) for details. + +On both platforms, launch the GUI from the command line via the `--gui` option, +which forwards any format/rounding flags and value to the app: + +``` $ crackNum --gui -- open the graphical interface $ crackNum --gui -fsp 2.5 -- open it with single-precision selected, and 2.5 cracked $ crackNum --gui 0xdeadbeef -- open it pre-filled with a value to decode ``` -See [`gui/README.md`](gui/README.md) for more details and other build targets. +See [`GUI/swiftGUI/README.md`](GUI/swiftGUI/README.md) for macOS build details and other build targets. ### Usage info ``` @@ -156,7 +169,7 @@ -h, -? --help print help, with examples -v --version print version info -d --debug debug mode, developers only - --gui launch the graphical interface (macOS) + --gui launch the graphical interface Examples: Encoding: @@ -181,7 +194,7 @@ crackNum -ffp4 0b0111 -- decode as an FP4 (E2M1) float crackNum -l4 -fhp 64\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation - GUI (macOS): + GUI: crackNum --gui -- launch the graphical interface crackNum --gui 0xdeadbeef -- launch the GUI, pre-filled with the given value diff --git a/crackNum.cabal b/crackNum.cabal --- a/crackNum.cabal +++ b/crackNum.cabal @@ -1,6 +1,6 @@ Cabal-version : 2.2 Name : crackNum -Version : 3.17 +Version : 3.18 Synopsis : Crack various integer and floating-point data formats Description : Crack IEEE-754 float formats and arbitrary sized words and integers, showing the layout. . @@ -13,7 +13,12 @@ Copyright : Levent Erkok Category : Tools Build-type : Simple -Extra-Source-Files : README.md, COPYRIGHT, CHANGES.md +Extra-Source-Files : README.md, COPYRIGHT, CHANGES.md, GUI/tclGUI/README.md + +-- The Tcl/Tk GUI is a data-file (not merely an extra-source-file) so that it is +-- actually installed alongside the binary, and can be found at run time via +-- Paths_crackNum.getDataFileName. See 'locateTcl' in Main.hs. +Data-files : GUI/tclGUI/crackNum.tcl source-repository head type: git diff --git a/src/CrackNum/Main.hs b/src/CrackNum/Main.hs --- a/src/CrackNum/Main.hs +++ b/src/CrackNum/Main.hs @@ -34,6 +34,7 @@ import System.Console.GetOpt (ArgOrder(Permute), getOpt, ArgDescr(..), OptDescr(..), usageInfo) import System.Exit (exitFailure, ExitCode(..)) import System.IO (hPutStr, stderr) +import System.Directory (findExecutable, doesFileExist) import System.Process (rawSystem) import qualified System.Info as Info @@ -48,7 +49,7 @@ import qualified Data.SBV as SBV import Data.Version (showVersion) -import Paths_crackNum (version) +import Paths_crackNum (version, getDataFileName) import CrackNum.TestSuite @@ -228,7 +229,7 @@ , Option "h?" ["help"] (NoArg Help) "print help, with examples" , Option "v" ["version"] (NoArg Version) "print version info" , Option "d" ["debug"] (NoArg Debug) "debug mode, developers only" - , Option "" ["gui"] (NoArg GUI) "launch the graphical interface (macOS)" + , Option "" ["gui"] (NoArg GUI) "launch the graphical interface" ] -- | Help info @@ -261,7 +262,7 @@ , " " ++ pn ++ " -ffp4 0b0111 -- decode as an FP4 (E2M1) float" , " " ++ pn ++ " -l4 -fhp 64\\'hbdffaaffdc71fc60 -- decode as half-precision float over 4 lanes using verilog notation" , "" - , " GUI (macOS):" + , " GUI:" , " " ++ pn ++ " --gui -- launch the graphical interface" , " " ++ pn ++ " --gui 0xdeadbeef -- launch the GUI, pre-filled with the given value" , "" @@ -285,18 +286,66 @@ die xs = do hPutStr stderr $ unlines $ "ERROR:" : map (" " ++) xs exitFailure --- | Launch the graphical interface (macOS only), forwarding all remaining arguments +-- | Where the Tcl/Tk GUI script lives relative to the package root; also its +-- location within the installed data-directory. (See Data-files in the cabal file.) +tclRelPath :: FilePath +tclRelPath = "GUI/tclGUI/crackNum.tcl" + +-- | Locate the Tcl/Tk GUI script. Normally it is installed together with the +-- binary, so this just works; we look in three places, in order: +-- +-- 1. $CRACKNUM_TCL, if set: an explicit override, mirroring $CRACKNUM_GUI on macOS. +-- 2. The PATH, so a source checkout can shadow the installed copy while hacking. +-- 3. The copy cabal installed in our data-directory. +locateTcl :: IO FilePath +locateTcl = do mbEnv <- lookupEnv "CRACKNUM_TCL" + case mbEnv of + Just p -> do ok <- doesFileExist p + if ok + then pure p + else die [ "The CRACKNUM_TCL environment variable is set, but does not name a file:" + , "" + , " " ++ p + ] + Nothing -> do mbPath <- findExecutable "crackNum.tcl" + case mbPath of + Just p -> pure p + Nothing -> do installed <- getDataFileName tclRelPath + ok <- doesFileExist installed + if ok + then pure installed + else die (noTcl installed) + where noTcl installed = + [ "Cannot find the CrackNum GUI script (crackNum.tcl)." + , "" + , "Looked in:" + , " $CRACKNUM_TCL (not set)" + , " crackNum.tcl on your PATH (not found)" + , " " ++ installed + , "" + , "This script is normally installed along with crackNum, so seeing this" + , "means the installed copy is missing or the binary has been moved." + , "" + , "If you have a source checkout, point at it directly:" + , "" + , " export CRACKNUM_TCL=/path/to/crackNum/" ++ tclRelPath + , "" + , "Otherwise, get a copy of the sources with either of:" + , "" + , " cabal get crackNum" + , " git clone http://github.com/LeventErkok/crackNum.git" + ] + +-- | Launch the graphical interface, forwarding all remaining arguments -- (format flags, rounding mode, and/or the value to crack) so the GUI can preselect --- them. The GUI itself calls back into this executable to do the actual cracking. The --- location of the app can be overridden with the CRACKNUM_GUI environment variable --- (pointing at the .app bundle); otherwise we ask LaunchServices to find it by name. +-- them. The GUI itself calls back into this executable to do the actual cracking. +-- +-- On macOS the GUI is a Swift/AppKit app; CRACKNUM_GUI can override the .app bundle +-- location. On Linux the GUI is a Tcl/Tk script; both 'wish' and 'crackNum.tcl' are +-- located via PATH. launchGUI :: [String] -> IO () launchGUI vals - | Info.os /= "darwin" - = die [ "The --gui option is only available on macOS." - , "On other platforms, use crackNum directly from the command line." - ] - | True + | Info.os == "darwin" = do mbApp <- lookupEnv "CRACKNUM_GUI" let args = case mbApp of Just p -> ["-n", p, "--args"] ++ vals @@ -310,11 +359,34 @@ , "get the crackNum sources and build the GUI (macOS 13+, Swift toolchain):" , "" , " git clone http://github.com/LeventErkok/crackNum.git" - , " cd crackNum/gui" + , " cd crackNum/GUI/swiftGUI" , " make install # builds and copies CrackNum.app into /Applications" , "" , "Then re-run: crackNum --gui" ++ (if null vals then "" else ' ' : unwords vals) ] + | Info.os == "linux" + = do mbWish <- findExecutable "wish" + wish <- case mbWish of + Just w -> pure w + Nothing -> die [ "Cannot find 'wish' on your PATH." + , "Install Tcl/Tk to get wish, e.g.:" + , "" + , " nix profile install nixpkgs#tk" + , " sudo apt install tk # Debian/Ubuntu" + , " sudo dnf install tk # RHEL/Fedora" + ] + tcl <- locateTcl + ec <- rawSystem wish (tcl : vals) + case ec of + ExitSuccess -> pure () + ExitFailure _ -> die [ "Unable to launch the CrackNum GUI." + , "" + , "Tried: " ++ wish ++ " " ++ tcl + ] + | True + = die [ "The --gui option is not supported on this platform (" ++ Info.os ++ ")." + , "Use crackNum directly from the command line." + ] -- | main entry point to crackNum @@ -369,10 +441,26 @@ | tryInfer = fromMaybe lanesGiven lanesInferred | True = lanesGiven - if decode - then decodeAllLanes isVerilog debug lanes kind arg - else encodeLane debug lanes kind rm arg + let act | decode = decodeAllLanes isVerilog debug lanes kind arg + | True = encodeLane debug lanes kind rm arg + act `C.catch` solverLimitation kind + +-- | We accept exponent/significand sizes down to 1 bit, but SMTLib's FloatingPoint +-- sort (and hence z3) requires at least 2 of each. Rather than letting such a format +-- surface as a raw solver exception with a backtrace, report it as a plain error. +-- Anything else is re-thrown untouched. +solverLimitation :: NKind -> SBVException -> IO a +solverLimitation kind e = case kind of + SFloat (FP eb sb) | eb < 2 || sb < 2 -> die [ "The solver does not support this format:" + , " " ++ plural eb "exponent bit" ++ ", " ++ plural sb "significand bit" + , "z3 requires at least 2 of each." + ] + _ -> C.throwIO e + where plural :: Int -> String -> String + plural 1 what = "1 " ++ what + plural n what = show n ++ " " ++ what ++ "s" + decodeAllLanes :: Bool -> Bool -> Int -> NKind -> String -> IO () decodeAllLanes isVerilog debug lanes kind arg = do when (lanes < 0) $ die @@ -614,6 +702,12 @@ mapM_ (putStrLn . fixVal) $ takeWhile (not . isClassification) (lines (show ieeeResult)) mapM_ putStrLn $ dropWhile (not . isClassification) (lines modifiedResult) +-- | The canonical quiet-NaN pattern for a float with @eb@ exponent bits and @sb@ +-- significand bits (including the implicit one): sign 0, all-ones exponent, and only +-- the leading stored significand bit set. For single-precision this is 0x7FC00000. +canonicalNaN :: Int -> Int -> Integer +canonicalNaN eb sb = (2 ^ eb - 1) * 2 ^ (sb - 1) + 2 ^ (sb - 2) + -- | Encoding encodeLane :: Bool -> Int -> NKind -> RM -> String -> IO () encodeLane debug lanes num rm inp @@ -626,8 +720,17 @@ SInt n -> print =<< ei True n SWord n -> print =<< ei False n SFloat s -> ef s (s == E5M2) - where satCmd = satWith z3{crackNum=True, verbose=debug, isNonModelVar = (/= "ENCODED")} + where cfg = z3{crackNum=True, verbose=debug, isNonModelVar = (/= "ENCODED")} + satCmd = satWith cfg + -- SMTLib's FloatingPoint sort has exactly one NaN value: the solver answers + -- with the abstract (_ NaN eb sb), so the concrete bit-pattern we display is + -- picked when that abstract value is materialized, and is not stable across + -- solver/library upgrades. Pin it to the canonical quiet NaN, the same way + -- the E4M3 path does. (We still note that the representation isn't unique.) + satCmdNaN :: Int -> Int -> Predicate -> IO SatResult + satCmdNaN eb sb = satWith cfg{crackNumSurfaceVals = [("ENCODED", canonicalNaN eb sb)]} + ei :: Bool -> Int -> IO SatResult ei sgn n = case reads inp of [(v :: Integer, "")] -> satCmd $ p v @@ -655,21 +758,27 @@ ef :: FP -> Bool -> IO () ef SP _ = case reads (fixup True inp) of - [(v :: Float, "")] -> do print =<< satCmd (p v) + [(v :: Float, "")] -> do print =<< run v (p v) note $ snd $ convert 8 24 _ -> ef (FP 8 24) False where p :: Float -> Predicate p f = do x <- sFloat "ENCODED" pure $ x .=== literal f + run f | isNaN f = satCmdNaN 8 24 + | True = satCmd + ef DP _ = case reads (fixup True inp) of - [(v :: Double, "")] -> do print =<< satCmd (p v) + [(v :: Double, "")] -> do print =<< run v (p v) note $ snd $ convert 11 53 _ -> ef (FP 11 53) False where p :: Double -> Predicate p d = do x <- sDouble "ENCODED" pure $ x .=== literal d + run d | isNaN d = satCmdNaN 11 53 + | True = satCmd + ef (FP i j) wasE5M2 = do let (v, mbS) = convert i j if bfIsNaN v && fixup False inp /= "NaN" then -- maybe it's a hexfloat? @@ -678,7 +787,9 @@ res <- satCmd (pRat hr) if wasE5M2 then fixE5M2Type res else print res - else do res <- satCmd (p v) + else do let run | bfIsNaN v = satCmdNaN i j + | True = satCmd + res <- run (p v) if wasE5M2 then fixE5M2Type res else print res note mbS diff --git a/src/CrackNum/TestSuite.hs b/src/CrackNum/TestSuite.hs --- a/src/CrackNum/TestSuite.hs +++ b/src/CrackNum/TestSuite.hs @@ -157,5 +157,9 @@ , testGroup "Bad" [ gold "badInvocation0" "-f3+4 0b01" , gold "badInvocation1" "-f3+4 0xFFFF" + -- We accept 1-bit exponents/significands, but the solver needs 2 of + -- each; make sure that surfaces as an error, not a raw exception. + , gold "badInvocation2" "-f3+1 0.5" + , gold "badInvocation3" "-f1+3 0b0000" ] ]