Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: support tests for invalid syntax #388

Merged
merged 5 commits into from
Nov 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 15 additions & 2 deletions pkg/corset/ast.go
Original file line number Diff line number Diff line change
Expand Up @@ -175,15 +175,15 @@ type DefInterleaved struct {
// The target column being defined
Target string
// The source columns used to define the interleaved target column.
Sources []string
Sources []*DefSourceColumn
}

// CanFinalise checks whether or not this interleaving is ready to be finalised.
// Specifically, it checks whether or not the source columns of this
// interleaving are themselves finalised.
func (p *DefInterleaved) CanFinalise(module uint, env *Environment) bool {
for _, col := range p.Sources {
if !env.IsColumnFinalised(module, col) {
if !env.IsColumnFinalised(module, col.Name) {
return false
}
}
Expand All @@ -200,6 +200,19 @@ func (p *DefInterleaved) Lisp() sexp.SExp {
panic("got here")
}

// DefSourceColumn provides information about a column being permuted by a
// sorted permutation.
type DefSourceColumn struct {
// Name of the column to be permuted
Name string
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefSourceColumn) Lisp() sexp.SExp {
panic("got here")
}

// DefLookup represents a lookup constraint between a set N of source
// expressions and a set of N target expressions. The source expressions must
// have a single context (i.e. all be in the same module) and likewise for the
Expand Down
18 changes: 14 additions & 4 deletions pkg/corset/parser.go
Original file line number Diff line number Diff line change
Expand Up @@ -302,6 +302,10 @@ func (p *Parser) parseColumnDeclaration(e sexp.SExp) (*DefColumn, *SyntaxError)

// Parse a vanishing declaration
func (p *Parser) parseDefConstraint(elements []sexp.SExp) (*DefConstraint, *SyntaxError) {
// Initial sanity checks
if elements[1].AsSymbol() == nil {
return nil, p.translator.SyntaxError(elements[1], "expected constraint handle")
}
//
handle := elements[1].AsSymbol().Value
// Vanishing constraints do not have global scope, hence qualified column
Expand Down Expand Up @@ -331,15 +335,15 @@ func (p *Parser) parseDefInterleaved(elements []sexp.SExp) (*DefInterleaved, *Sy
// Extract target and source columns
target := elements[1].AsSymbol().Value
sexpSources := elements[2].AsList()
sources := make([]string, sexpSources.Len())
sources := make([]*DefSourceColumn, sexpSources.Len())
//
for i := 0; i != sexpSources.Len(); i++ {
ith := sexpSources.Get(i)
if ith.AsSymbol() == nil {
return nil, p.translator.SyntaxError(ith, "malformed source column")
}
// Extract column name
sources[i] = ith.AsSymbol().Value
sources[i] = &DefSourceColumn{ith.AsSymbol().Value}
}
// Done
return &DefInterleaved{target, sources}, nil
Expand Down Expand Up @@ -408,15 +412,15 @@ func (p *Parser) parseDefPermutation(elements []sexp.SExp) (*DefPermutation, *Sy
return nil, err
}
// Parse source column
if sources[i], err = p.parsePermutedColumnDeclaration(sexpSources.Get(i)); err != nil {
if sources[i], err = p.parsePermutedColumnDeclaration(i == 0, sexpSources.Get(i)); err != nil {
return nil, err
}
}
//
return &DefPermutation{targets, sources}, nil
}

func (p *Parser) parsePermutedColumnDeclaration(e sexp.SExp) (*DefPermutedColumn, *SyntaxError) {
func (p *Parser) parsePermutedColumnDeclaration(signRequired bool, e sexp.SExp) (*DefPermutedColumn, *SyntaxError) {
var err *SyntaxError
//
defcolumn := &DefPermutedColumn{"", false}
Expand All @@ -436,6 +440,8 @@ func (p *Parser) parsePermutedColumnDeclaration(e sexp.SExp) (*DefPermutedColumn
}
// Parse column name
defcolumn.Name = l.Get(1).AsSymbol().Value
} else if signRequired {
return nil, p.translator.SyntaxError(e, "missing sort direction")
} else {
defcolumn.Name = e.String(false)
}
Expand All @@ -458,6 +464,10 @@ func (p *Parser) parsePermutedColumnSign(sign *sexp.Symbol) (bool, *SyntaxError)

// Parse a property assertion
func (p *Parser) parseDefProperty(elements []sexp.SExp) (*DefProperty, *SyntaxError) {
// Initial sanity checks
if elements[1].AsSymbol() == nil {
return nil, p.translator.SyntaxError(elements[1], "expected constraint handle")
}
//
handle := elements[1].AsSymbol().Value
// Translate expression
Expand Down
114 changes: 81 additions & 33 deletions pkg/corset/resolver.go
Original file line number Diff line number Diff line change
Expand Up @@ -125,11 +125,11 @@ func (r *resolver) resolveAssignments(circuit *Circuit) []SyntaxError {
// to process all columns before we can sure that they are all declared
// correctly.
func (r *resolver) resolveAssignmentsInModule(module string, decls []Declaration) []SyntaxError {
// FIXME: the following is actually broken since we must allocate all input
// columns in all modules before any assignments are preregistered.
errors := r.initialiseAssignmentsInModule(module, decls)
// Check for any errors
if len(errors) > 0 {
if errors := r.initialiseAssignmentsInModule(module, decls); len(errors) > 0 {
return errors
}
// Check assignments
if errors := r.checkAssignmentsInModule(module, decls); len(errors) > 0 {
return errors
}
// Iterate until all columns finalised
Expand Down Expand Up @@ -170,6 +170,29 @@ func (r *resolver) initialiseAssignmentsInModule(module string, decls []Declarat
return errors
}

func (r *resolver) checkAssignmentsInModule(module string, decls []Declaration) []SyntaxError {
errors := make([]SyntaxError, 0)
mid := r.env.Module(module)
//
for _, d := range decls {
if col, ok := d.(*DefInterleaved); ok {
for _, c := range col.Sources {
if !r.env.HasColumn(mid, c.Name) {
errors = append(errors, *r.srcmap.SyntaxError(c, "unknown source column"))
}
}
} else if col, ok := d.(*DefPermutation); ok {
for _, c := range col.Sources {
if !r.env.HasColumn(mid, c.Name) {
errors = append(errors, *r.srcmap.SyntaxError(c, "unknown source column"))
}
}
}
}
// Done
return errors
}

// Iterate the column allocation to a fix point by iteratively fleshing out column information.
func (r *resolver) finaliseAssignmentsInModule(module string, decls []Declaration) []SyntaxError {
mid := r.env.Module(module)
Expand Down Expand Up @@ -253,7 +276,7 @@ func (r *resolver) finaliseInterleavedAssignment(module uint, decl *DefInterleav
// Determine type and length multiplier
for i, source := range decl.Sources {
// Lookup info of column being interleaved.
info := r.env.Column(module, source)
info := r.env.Column(module, source.Name)
if i == 0 {
length_multiplier = info.multiplier
datatype = info.datatype
Expand Down Expand Up @@ -290,7 +313,9 @@ func (r *resolver) finalisePermutationAssignment(module uint, decl *DefPermutati
ith := decl.Sources[i]
src := r.env.Column(module, ith.Name)
// Sanity check length multiplier
if i == 0 {
if i == 0 && src.datatype.AsUint() == nil {
errors = append(errors, *r.srcmap.SyntaxError(ith, "fixed-width type required"))
} else if i == 0 {
multiplier = src.multiplier
} else if multiplier != src.multiplier {
// Problem
Expand Down Expand Up @@ -357,53 +382,69 @@ func (r *resolver) resolveConstraintsInModule(module string, decls []Declaration

// Resolve those variables appearing in either the guard or the body of this constraint.
func (r *resolver) resolveDefConstraintInModule(module string, decl *DefConstraint) []SyntaxError {
var errors []SyntaxError
var (
errors []SyntaxError
context = tr.VoidContext()
)
// Resolve guard
if decl.Guard != nil {
errors = r.resolveExpressionInModule(module, false, decl.Guard)
errors = r.resolveExpressionInModule(module, false, &context, decl.Guard)
}
// Resolve constraint body
errors = append(errors, r.resolveExpressionInModule(module, false, decl.Constraint)...)
errors = append(errors, r.resolveExpressionInModule(module, false, &context, decl.Constraint)...)
// Done
return errors
}

// Resolve those variables appearing in the body of this range constraint.
func (r *resolver) resolveDefInRangeInModule(module string, decl *DefInRange) []SyntaxError {
var errors []SyntaxError
var (
errors []SyntaxError
context = tr.VoidContext()
)
// Resolve property body
errors = append(errors, r.resolveExpressionInModule(module, false, decl.Expr)...)
errors = append(errors, r.resolveExpressionInModule(module, false, &context, decl.Expr)...)
// Done
return errors
}

// Resolve those variables appearing in the body of this lookup constraint.
func (r *resolver) resolveDefLookupInModule(module string, decl *DefLookup) []SyntaxError {
var errors []SyntaxError
var (
errors []SyntaxError
sourceContext = tr.VoidContext()
targetContext = tr.VoidContext()
)

// Resolve source expressions
errors = append(errors, r.resolveExpressionsInModule(module, true, decl.Sources)...)
errors = append(errors, r.resolveExpressionsInModule(module, true, &sourceContext, decl.Sources)...)
// Resolve target expressions
errors = append(errors, r.resolveExpressionsInModule(module, true, decl.Targets)...)
errors = append(errors, r.resolveExpressionsInModule(module, true, &targetContext, decl.Targets)...)
// Done
return errors
}

// Resolve those variables appearing in the body of this property assertion.
func (r *resolver) resolveDefPropertyInModule(module string, decl *DefProperty) []SyntaxError {
var errors []SyntaxError
var (
errors []SyntaxError
context = tr.VoidContext()
)
// Resolve property body
errors = append(errors, r.resolveExpressionInModule(module, false, decl.Assertion)...)
errors = append(errors, r.resolveExpressionInModule(module, false, &context, decl.Assertion)...)
// Done
return errors
}

// Resolve a sequence of zero or more expressions within a given module. This
// simply resolves each of the arguments in turn, collecting any errors arising.
func (r *resolver) resolveExpressionsInModule(module string, global bool, args []Expr) []SyntaxError {
func (r *resolver) resolveExpressionsInModule(module string, global bool,
context *tr.Context, args []Expr) []SyntaxError {
var errors []SyntaxError
// Visit each argument
for _, arg := range args {
if arg != nil {
errs := r.resolveExpressionInModule(module, global, arg)
errs := r.resolveExpressionInModule(module, global, context, arg)
errors = append(errors, errs...)
}
}
Expand All @@ -416,25 +457,25 @@ func (r *resolver) resolveExpressionsInModule(module string, global bool, args [
// variable accesses. As above, the goal is ensure variable refers to something
// that was declared and, more specifically, what kind of access it is (e.g.
// column access, constant access, etc).
func (r *resolver) resolveExpressionInModule(module string, global bool, expr Expr) []SyntaxError {
func (r *resolver) resolveExpressionInModule(module string, global bool, context *tr.Context, expr Expr) []SyntaxError {
if _, ok := expr.(*Constant); ok {
return nil
} else if v, ok := expr.(*Add); ok {
return r.resolveExpressionsInModule(module, global, v.Args)
return r.resolveExpressionsInModule(module, global, context, v.Args)
} else if v, ok := expr.(*Exp); ok {
return r.resolveExpressionInModule(module, global, v.Arg)
return r.resolveExpressionInModule(module, global, context, v.Arg)
} else if v, ok := expr.(*IfZero); ok {
return r.resolveExpressionsInModule(module, global, []Expr{v.Condition, v.TrueBranch, v.FalseBranch})
return r.resolveExpressionsInModule(module, global, context, []Expr{v.Condition, v.TrueBranch, v.FalseBranch})
} else if v, ok := expr.(*List); ok {
return r.resolveExpressionsInModule(module, global, v.Args)
return r.resolveExpressionsInModule(module, global, context, v.Args)
} else if v, ok := expr.(*Mul); ok {
return r.resolveExpressionsInModule(module, global, v.Args)
return r.resolveExpressionsInModule(module, global, context, v.Args)
} else if v, ok := expr.(*Normalise); ok {
return r.resolveExpressionInModule(module, global, v.Arg)
return r.resolveExpressionInModule(module, global, context, v.Arg)
} else if v, ok := expr.(*Sub); ok {
return r.resolveExpressionsInModule(module, global, v.Args)
return r.resolveExpressionsInModule(module, global, context, v.Args)
} else if v, ok := expr.(*VariableAccess); ok {
return r.resolveVariableInModule(module, global, v)
return r.resolveVariableInModule(module, global, context, v)
} else {
return r.srcmap.SyntaxErrors(expr, "unknown expression")
}
Expand All @@ -443,18 +484,25 @@ func (r *resolver) resolveExpressionInModule(module string, global bool, expr Ex
// Resolve a specific variable access contained within some expression which, in
// turn, is contained within some module. Note, qualified accesses are only
// permitted in a global context.
func (r *resolver) resolveVariableInModule(module string, global bool, expr *VariableAccess) []SyntaxError {
func (r *resolver) resolveVariableInModule(module string, global bool, context *tr.Context,
expr *VariableAccess) []SyntaxError {
// Check whether this is a qualified access, or not.
if global && expr.Module != nil {
module = *expr.Module
} else if expr.Module != nil {
if !global && expr.Module != nil {
return r.srcmap.SyntaxErrors(expr, "qualified access not permitted here")
} else if expr.Module != nil && !r.env.HasModule(*expr.Module) {
return r.srcmap.SyntaxErrors(expr, fmt.Sprintf("unknown module %s", *expr.Module))
} else if expr.Module != nil {
module = *expr.Module
}
// FIXME: handle qualified variable accesses
//
mid := r.env.Module(module)
// Attempt resolve as a column access in enclosing module
if cinfo, ok := r.env.LookupColumn(mid, expr.Name); ok {
ctx := tr.NewContext(mid, cinfo.multiplier)
// Update context
if *context = context.Join(ctx); context.IsConflicted() {
return r.srcmap.SyntaxErrors(expr, "conflicting context")
}
// Register the binding to complete resolution.
expr.Binding = &Binder{true, ctx, cinfo.cid}
// Done
Expand Down
2 changes: 1 addition & 1 deletion pkg/corset/translator.go
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,7 @@ func (t *translator) translateDefInterleaved(decl *DefInterleaved, module uint)
info := t.env.Column(module, decl.Target)
// Determine source column identifiers
for i, source := range decl.Sources {
sources[i] = t.env.Column(module, source).cid
sources[i] = t.env.Column(module, source.Name).cid
}
// Construct context for this assignment
context := tr.NewContext(module, info.multiplier)
Expand Down
Loading