Language Reference

perlchecker supports a strict subset of Perl designed for SMT-based verification. This page documents every supported construct.

Types

Type	Description
I64	64-bit signed integer
Str	UTF-8 string (bounded to 32 characters in the SMT model)
Array<I64>	Ordered sequence of integers
Array<Str>	Ordered sequence of strings
Hash<Str, I64>	String-keyed map with integer values
Hash<Str, Str>	String-keyed map with string values

There is no implicit coercion between I64 and Str. Using an operator that expects one type with a value of the other is a type error.

Variables and Assignment

Declaration:

my $x;           # declare without initializing
my $x = 42;      # declare with initial value

Assignment:

$x = $x + 1;

Compound assignment operators:

+=, -=, *=, /=, %=, **=, &=, |=, ^=, <<=, >>=, .=

These desugar to the equivalent binary operation. For example, $x += 1 becomes $x = $x + 1.

Increment and decrement:

$x++ and $x-- desugar to $x = $x + 1 and $x = $x - 1.

Arithmetic Operators

Operator	Example	Notes
+	$x + $y	Addition
-	$x - $y	Subtraction
*	$x * $y	Multiplication
/	$x / $y	Truncating division. Paths where the divisor is 0 are discarded.
%	$x % $y	Modulo. Paths where the divisor is 0 are discarded.
**	$x ** $y	Exponentiation (right-associative)
- (unary)	-$x	Negation

Comparison Operators

Numeric

Operator	Description
<	Less than
<=	Less than or equal
>	Greater than
>=	Greater than or equal
==	Equal
!=	Not equal
<=>	Spaceship (three-way compare): returns -1, 0, or 1

String

Operator	Description
eq	Equal
ne	Not equal
lt	Less than (lexicographic)
gt	Greater than (lexicographic)
le	Less than or equal (lexicographic)
ge	Greater than or equal (lexicographic)
cmp	String compare: returns -1, 0, or 1

Logical Operators

Operator	Description
&&, and	Logical AND (and has lower precedence)
||, or	Logical OR (or has lower precedence)
!, not	Logical NOT (not has lower precedence)

Bitwise Operators

Operator	Example	Description
&	$x & $y	Bitwise AND
|	$x | $y	Bitwise OR
^	$x ^ $y	Bitwise XOR
~	~$x	Bitwise complement
<<	$x << $n	Left shift
>>	$x >> $n	Right shift

String Operators

Operator	Example	Description
.	$a . $b	Concatenation
x	"ab" x 3	String repetition (count must be a constant)

Control Flow

if / elsif / else

if ($x > 0) {
    return 1;
} elsif ($x == 0) {
    return 0;
} else {
    return -1;
}

unless

Equivalent to if with a negated condition:

unless ($x == 0) {
    return $x;
}

while

while ($x > 0) {
    $x = $x - 1;
}

Loops are unrolled to a bounded depth (default: 5 iterations). Use --max_loop_unroll to adjust.

until

Equivalent to while with a negated condition:

until ($x == 0) {
    $x = $x - 1;
}

for (C-style)

for (my $i = 0; $i < $n; $i++) {
    $sum = $sum + $arr[$i];
}

do-while / do-until

do {
    $x = $x - 1;
} while ($x > 0);

do {
    $x = $x - 1;
} until ($x == 0);

Statement Modifiers

A statement can be followed by if or unless to make it conditional:

return $x if ($x > 0);
return 0 unless ($found == 1);
$x = $x + 1 if ($flag == 1);
die "negative" if ($x < 0);
die "bad" unless ($x >= 0);
last if ($done == 1);
next unless ($valid == 1);

Loop Control

Statement	Description
last	Exit the innermost loop (like break in C)
next	Skip to the next iteration (like continue in C)

Both support statement modifiers: last if ($cond);, next unless ($cond);.

Built-in Functions

String Functions

Signature	Description
length($s) → I64	Number of characters
substr($s, $off, $len) → Str	Substring starting at $off with length $len
substr($s, $off) → Str	Substring from $off to end of string
index($s, $sub) → I64	Position of $sub in $s, or -1 if not found
index($s, $sub, $start) → I64	Same, searching from $start
chomp($s) → Str	Remove trailing newline
reverse($s) → Str	Reverse the string
contains($s, $sub) → I64	1 if $s contains $sub, else 0
starts_with($s, $prefix) → I64	1 if $s starts with $prefix, else 0
ends_with($s, $suffix) → I64	1 if $s ends with $suffix, else 0
replace($s, $from, $to) → Str	Replace all occurrences of $from with $to
char_at($s, $i) → Str	Character at position $i as a 1-character string
ord($s) → I64	ASCII code of the first character
chr($n) → Str	Character from ASCII code

Numeric Functions

Signature	Description
abs($n) → I64	Absolute value
min($a, $b) → I64	Minimum of two integers
max($a, $b) → I64	Maximum of two integers
int($x) → I64	Truncate to integer

Array Functions

Signature	Description
scalar(@arr) → I64	Number of elements in the array
push(@arr, $val)	Append $val to the end of @arr
pop(@arr) → element	Remove and return the last element

Array and Hash Operations

Array access:

my $val = $arr[$i];     # read element at index $i
$arr[$i] = $new_val;    # write element at index $i

Hash access:

my $val = $h{"key"};    # read value for key
$h{$key} = $new_val;    # write value for key

Arrays and hashes are modeled using Z3’s Array theory (select/store). Reading a hash key that was never written returns an unconstrained symbolic value.

Function Calls

Functions can call other annotated functions in the same file:

my $result = other_function($x, $y);

Calls are inlined during verification. The callee must be defined before the caller in the source file. Recursion is not allowed.

Ternary Operator

my $result = ($x > 0) ? $x : -$x;

Nested ternary expressions are supported.

Error and Output Statements

Statement	Description
die "msg"	Terminate execution with an error. If reachable, verification fails.
croak "msg"	Alias for die
confess "msg"	Alias for die
warn "msg"	No-op for verification
print $expr	No-op for verification
say $expr	No-op for verification

Integer Literals

42           # decimal
0xFF         # hexadecimal
0o77         # octal
0b1010       # binary
1_000_000    # underscores allowed as visual separators

String Literals

Double-quoted (supports escape sequences):

"hello\nworld"    # \n, \t, \\, \" supported

Single-quoted (minimal escaping):

'hello'           # only \\ and \' are escape sequences

Special Variables

These variables have special meaning in annotation expressions and are not user-declarable.

Variable	Description
$result	The function’s return value (available in # post: annotations)
$overflow	Boolean: true if any arithmetic on the current path overflowed I64 range

$overflow is typically used in assertions to prove arithmetic safety:

my $sum = $x + $y;
# assert: !$overflow

Without the assertion, arithmetic wraps silently (two’s complement BV64). This section may be extended with additional special variables in the future.