Skip to content

Commit 6b85fef

Browse files
committed
error unions, output folder path
1 parent 8386542 commit 6b85fef

File tree

4 files changed

+348
-73
lines changed

4 files changed

+348
-73
lines changed

src/formal_verifier.zig

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,9 @@ pub const FormalVerificationError = error{
1414
InvalidQuantifier,
1515
UnboundedLoop,
1616
ComplexityTooHigh,
17+
ErrorUnionVerificationFailed,
18+
ErrorPropagationIncomplete,
19+
TryWithoutErrorUnion,
1720
};
1821

1922
/// SMT solver backend types
@@ -267,6 +270,7 @@ pub const FormalVerifier = struct {
267270
theory_db: MathTheoryDB,
268271
symbolic_executor: SymbolicExecutor,
269272
proof_cache: ProofCache,
273+
error_union_verifier: ErrorUnionVerifier,
270274
verification_config: VerificationConfig,
271275

272276
pub const VerificationConfig = struct {
@@ -498,8 +502,8 @@ pub const FormalVerifier = struct {
498502
.Mapping => MathDomain.Function,
499503
.DoubleMap => MathDomain.Function,
500504
.Identifier => MathDomain.Integer, // Default for custom types
501-
.ErrorUnion => MathDomain.Integer, // Error unions are treated as integers
502-
.Result => MathDomain.Integer, // Result types are treated as integers
505+
.ErrorUnion => MathDomain.Algebraic, // Error unions use algebraic data types
506+
.Result => MathDomain.Algebraic, // Result types use algebraic data types
503507
};
504508
}
505509
return MathDomain.Integer;
@@ -510,13 +514,78 @@ pub const FormalVerifier = struct {
510514
}
511515
};
512516

517+
/// Error union verification methods
518+
pub const ErrorUnionVerifier = struct {
519+
allocator: Allocator,
520+
521+
pub fn init(allocator: Allocator) ErrorUnionVerifier {
522+
return ErrorUnionVerifier{
523+
.allocator = allocator,
524+
};
525+
}
526+
527+
pub fn deinit(self: *ErrorUnionVerifier) void {
528+
_ = self;
529+
}
530+
531+
/// Verify that all error paths are handled in try-catch blocks
532+
pub fn verifyErrorPropagation(self: *ErrorUnionVerifier, try_block: *ast.TryBlockNode) FormalVerificationError!bool {
533+
_ = self;
534+
// TODO: Implement error propagation verification
535+
// - Check that all possible error conditions are handled
536+
// - Verify that error variables are properly typed
537+
// - Ensure no error paths are missed
538+
539+
if (try_block.catch_block == null) {
540+
return FormalVerificationError.ErrorPropagationIncomplete;
541+
}
542+
543+
return true;
544+
}
545+
546+
/// Verify that try expressions are only used with error union types
547+
pub fn verifyTryExpression(self: *ErrorUnionVerifier, try_expr: *ast.TryExpr) FormalVerificationError!bool {
548+
_ = self;
549+
_ = try_expr;
550+
// TODO: Implement try expression verification
551+
// - Check that the expression being tried returns an error union
552+
// - Verify that error propagation is correct
553+
// - Ensure proper error handling context
554+
555+
return true;
556+
}
557+
558+
/// Generate SMT constraints for error union types
559+
pub fn generateErrorUnionConstraints(self: *ErrorUnionVerifier, error_union_type: *ast.ErrorUnionType, variable_name: []const u8) FormalVerificationError![]const u8 {
560+
_ = error_union_type;
561+
562+
// Generate SMT-LIB constraints for error union
563+
const constraint = try std.fmt.allocPrint(self.allocator, "(assert (or (= (tag {s}) success) (= (tag {s}) error)))", .{ variable_name, variable_name });
564+
565+
return constraint;
566+
}
567+
568+
/// Verify error union invariants
569+
pub fn verifyErrorUnionInvariants(self: *ErrorUnionVerifier, function: *ast.FunctionNode) FormalVerificationError!bool {
570+
_ = self;
571+
_ = function;
572+
// TODO: Implement error union invariant verification
573+
// - Check that error union functions properly handle all error cases
574+
// - Verify that success cases don't leak errors
575+
// - Ensure error union consistency across function calls
576+
577+
return true;
578+
}
579+
};
580+
513581
pub fn init(allocator: Allocator) FormalVerifier {
514582
return FormalVerifier{
515583
.allocator = allocator,
516584
.smt_solver = SMTSolverType.Internal,
517585
.theory_db = MathTheoryDB.init(allocator),
518586
.symbolic_executor = SymbolicExecutor.init(allocator),
519587
.proof_cache = ProofCache.init(allocator),
588+
.error_union_verifier = ErrorUnionVerifier.init(allocator),
520589
.verification_config = VerificationConfig{},
521590
};
522591
}
@@ -525,6 +594,7 @@ pub const FormalVerifier = struct {
525594
self.theory_db.deinit();
526595
self.symbolic_executor.deinit();
527596
self.proof_cache.deinit();
597+
self.error_union_verifier.deinit();
528598
}
529599

530600
/// Verify a complex formal condition

src/main.zig

Lines changed: 118 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -29,62 +29,58 @@ pub fn main() !void {
2929
return;
3030
}
3131

32-
const command = args[1];
33-
34-
if (std.mem.eql(u8, command, "lex")) {
35-
if (args.len < 3) {
36-
try printUsage();
37-
return;
38-
}
39-
try runLexer(allocator, args[2]);
40-
} else if (std.mem.eql(u8, command, "parse")) {
41-
if (args.len < 3) {
42-
try printUsage();
43-
return;
44-
}
45-
try runParser(allocator, args[2]);
46-
} else if (std.mem.eql(u8, command, "analyze")) {
47-
if (args.len < 3) {
48-
try printUsage();
49-
return;
50-
}
51-
try runSemanticAnalysis(allocator, args[2]);
52-
} else if (std.mem.eql(u8, command, "ir")) {
53-
if (args.len < 3) {
54-
try printUsage();
55-
return;
56-
}
57-
try runIRGeneration(allocator, args[2]);
58-
} else if (std.mem.eql(u8, command, "compile")) {
59-
if (args.len < 3) {
60-
try printUsage();
61-
return;
62-
}
63-
try runFullCompilation(allocator, args[2]);
64-
} else if (std.mem.eql(u8, command, "ast")) {
65-
if (args.len < 3) {
66-
try printUsage();
67-
return;
68-
}
69-
try runASTGeneration(allocator, args[2]);
70-
} else if (std.mem.eql(u8, command, "hir")) {
71-
if (args.len < 3) {
72-
try printUsage();
73-
return;
74-
}
75-
try runHIRGeneration(allocator, args[2]);
76-
} else if (std.mem.eql(u8, command, "yul")) {
77-
if (args.len < 3) {
78-
try printUsage();
79-
return;
80-
}
81-
try runYulGeneration(allocator, args[2]);
82-
} else if (std.mem.eql(u8, command, "bytecode")) {
83-
if (args.len < 3) {
32+
// Parse arguments to find output directory option
33+
var output_dir: ?[]const u8 = null;
34+
var command: ?[]const u8 = null;
35+
var input_file: ?[]const u8 = null;
36+
var i: usize = 1;
37+
38+
while (i < args.len) {
39+
if (std.mem.eql(u8, args[i], "-o") or std.mem.eql(u8, args[i], "--output-dir")) {
40+
if (i + 1 >= args.len) {
41+
try printUsage();
42+
return;
43+
}
44+
output_dir = args[i + 1];
45+
i += 2;
46+
} else if (command == null) {
47+
command = args[i];
48+
i += 1;
49+
} else if (input_file == null) {
50+
input_file = args[i];
51+
i += 1;
52+
} else {
8453
try printUsage();
8554
return;
8655
}
87-
try runBytecodeGeneration(allocator, args[2]);
56+
}
57+
58+
if (command == null or input_file == null) {
59+
try printUsage();
60+
return;
61+
}
62+
63+
const cmd = command.?;
64+
const file_path = input_file.?;
65+
66+
if (std.mem.eql(u8, cmd, "lex")) {
67+
try runLexer(allocator, file_path);
68+
} else if (std.mem.eql(u8, cmd, "parse")) {
69+
try runParser(allocator, file_path);
70+
} else if (std.mem.eql(u8, cmd, "analyze")) {
71+
try runSemanticAnalysis(allocator, file_path);
72+
} else if (std.mem.eql(u8, cmd, "ir")) {
73+
try runIRGeneration(allocator, file_path);
74+
} else if (std.mem.eql(u8, cmd, "compile")) {
75+
try runFullCompilation(allocator, file_path);
76+
} else if (std.mem.eql(u8, cmd, "ast")) {
77+
try runASTGeneration(allocator, file_path, output_dir);
78+
} else if (std.mem.eql(u8, cmd, "hir")) {
79+
try runHIRGeneration(allocator, file_path, output_dir);
80+
} else if (std.mem.eql(u8, cmd, "yul")) {
81+
try runYulGeneration(allocator, file_path, output_dir);
82+
} else if (std.mem.eql(u8, cmd, "bytecode")) {
83+
try runBytecodeGeneration(allocator, file_path, output_dir);
8884
} else {
8985
try printUsage();
9086
}
@@ -93,7 +89,9 @@ pub fn main() !void {
9389
fn printUsage() !void {
9490
const stdout = std.io.getStdOut().writer();
9591
try stdout.print("Ora DSL Compiler v0.1\n", .{});
96-
try stdout.print("Usage: ora <command> <file>\n", .{});
92+
try stdout.print("Usage: ora [options] <command> <file>\n", .{});
93+
try stdout.print("\nOptions:\n", .{});
94+
try stdout.print(" -o, --output-dir <dir> - Specify output directory for generated files\n", .{});
9795
try stdout.print("\nCommands:\n", .{});
9896
try stdout.print(" lex <file> - Tokenize a .ora file\n", .{});
9997
try stdout.print(" parse <file> - Parse a .ora file to AST\n", .{});
@@ -104,6 +102,8 @@ fn printUsage() !void {
104102
try stdout.print(" hir <file> - Generate HIR and save to JSON file\n", .{});
105103
try stdout.print(" yul <file> - Generate Yul code from HIR\n", .{});
106104
try stdout.print(" bytecode <file> - Generate EVM bytecode from HIR\n", .{});
105+
try stdout.print("\nExample:\n", .{});
106+
try stdout.print(" ora -o build ast example.ora\n", .{});
107107
}
108108

109109
/// Run lexer on file and display tokens
@@ -517,7 +517,7 @@ fn printAstSummary(writer: anytype, node: *lib.AstNode, indent: u32) !void {
517517
}
518518

519519
/// Generate AST and save to JSON file
520-
fn runASTGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
520+
fn runASTGeneration(allocator: std.mem.Allocator, file_path: []const u8, output_dir: ?[]const u8) !void {
521521
const stdout = std.io.getStdOut().writer();
522522

523523
// Read source file
@@ -550,7 +550,21 @@ fn runASTGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
550550
try stdout.print("Generated {} AST nodes\n", .{ast_nodes.len});
551551

552552
// Generate output filename
553-
const output_file = try std.mem.concat(allocator, u8, &[_][]const u8{ std.fs.path.stem(file_path), ".ast.json" });
553+
const output_file = if (output_dir) |dir| blk: {
554+
// Create output directory if it doesn't exist
555+
std.fs.cwd().makeDir(dir) catch |err| switch (err) {
556+
error.PathAlreadyExists => {},
557+
else => return err,
558+
};
559+
560+
const basename = std.fs.path.stem(file_path);
561+
const filename = try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".ast.json" });
562+
defer allocator.free(filename);
563+
break :blk try std.fs.path.join(allocator, &[_][]const u8{ dir, filename });
564+
} else blk: {
565+
const basename = std.fs.path.stem(file_path);
566+
break :blk try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".ast.json" });
567+
};
554568
defer allocator.free(output_file);
555569

556570
// Save AST to JSON file
@@ -570,7 +584,7 @@ fn runASTGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
570584
}
571585

572586
/// Generate HIR and save to JSON file
573-
fn runHIRGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
587+
fn runHIRGeneration(allocator: std.mem.Allocator, file_path: []const u8, output_dir: ?[]const u8) !void {
574588
const stdout = std.io.getStdOut().writer();
575589

576590
// Read source file
@@ -627,7 +641,21 @@ fn runHIRGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
627641
try stdout.print(" {} contracts converted to HIR\n", .{hir_program.contracts.len});
628642

629643
// Generate output filename
630-
const output_file = try std.mem.concat(allocator, u8, &[_][]const u8{ std.fs.path.stem(file_path), ".hir.json" });
644+
const output_file = if (output_dir) |dir| blk: {
645+
// Create output directory if it doesn't exist
646+
std.fs.cwd().makeDir(dir) catch |err| switch (err) {
647+
error.PathAlreadyExists => {},
648+
else => return err,
649+
};
650+
651+
const basename = std.fs.path.stem(file_path);
652+
const filename = try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".hir.json" });
653+
defer allocator.free(filename);
654+
break :blk try std.fs.path.join(allocator, &[_][]const u8{ dir, filename });
655+
} else blk: {
656+
const basename = std.fs.path.stem(file_path);
657+
break :blk try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".hir.json" });
658+
};
631659
defer allocator.free(output_file);
632660

633661
// Save HIR to JSON file
@@ -647,7 +675,7 @@ fn runHIRGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
647675
}
648676

649677
/// Generate Yul code from HIR
650-
fn runYulGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
678+
fn runYulGeneration(allocator: std.mem.Allocator, file_path: []const u8, output_dir: ?[]const u8) !void {
651679
const stdout = std.io.getStdOut().writer();
652680

653681
// Read source file
@@ -703,7 +731,21 @@ fn runYulGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
703731
try stdout.print("{s}\n", .{yul_code});
704732

705733
// Save to file
706-
const output_file = try std.mem.concat(allocator, u8, &[_][]const u8{ std.fs.path.stem(file_path), ".yul" });
734+
const output_file = if (output_dir) |dir| blk: {
735+
// Create output directory if it doesn't exist
736+
std.fs.cwd().makeDir(dir) catch |err| switch (err) {
737+
error.PathAlreadyExists => {},
738+
else => return err,
739+
};
740+
741+
const basename = std.fs.path.stem(file_path);
742+
const filename = try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".yul" });
743+
defer allocator.free(filename);
744+
break :blk try std.fs.path.join(allocator, &[_][]const u8{ dir, filename });
745+
} else blk: {
746+
const basename = std.fs.path.stem(file_path);
747+
break :blk try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".yul" });
748+
};
707749
defer allocator.free(output_file);
708750

709751
const file = std.fs.cwd().createFile(output_file, .{}) catch |err| {
@@ -717,7 +759,7 @@ fn runYulGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
717759
}
718760

719761
/// Generate EVM bytecode from HIR
720-
fn runBytecodeGeneration(allocator: std.mem.Allocator, file_path: []const u8) !void {
762+
fn runBytecodeGeneration(allocator: std.mem.Allocator, file_path: []const u8, output_dir: ?[]const u8) !void {
721763
const stdout = std.io.getStdOut().writer();
722764

723765
// Read source file
@@ -781,7 +823,21 @@ fn runBytecodeGeneration(allocator: std.mem.Allocator, file_path: []const u8) !v
781823
try stdout.print("Bytecode: {s}\n", .{bytecode});
782824

783825
// Save to file
784-
const output_file = try std.mem.concat(allocator, u8, &[_][]const u8{ std.fs.path.stem(file_path), ".bin" });
826+
const output_file = if (output_dir) |dir| blk: {
827+
// Create output directory if it doesn't exist
828+
std.fs.cwd().makeDir(dir) catch |err| switch (err) {
829+
error.PathAlreadyExists => {},
830+
else => return err,
831+
};
832+
833+
const basename = std.fs.path.stem(file_path);
834+
const filename = try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".bin" });
835+
defer allocator.free(filename);
836+
break :blk try std.fs.path.join(allocator, &[_][]const u8{ dir, filename });
837+
} else blk: {
838+
const basename = std.fs.path.stem(file_path);
839+
break :blk try std.mem.concat(allocator, u8, &[_][]const u8{ basename, ".bin" });
840+
};
785841
defer allocator.free(output_file);
786842

787843
const file = std.fs.cwd().createFile(output_file, .{}) catch |err| {

0 commit comments

Comments
 (0)