lang: funcs: core: fmt: Add more invariants to printf

This adds even more invariants to print that I might have missed. It may
be redundant, or it may help.
This commit is contained in:
James Shubin
2021-05-19 08:31:36 -04:00
parent 97baad4cb1
commit 1fd06ecbf9

View File

@@ -105,7 +105,7 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
if cfavInvar.Func != expr {
continue
}
// cfavInvar.Expr is the ExprCall!
// cfavInvar.Expr is the ExprCall! (the return pointer)
// cfavInvar.Args are the args that ExprCall uses!
if len(cfavInvar.Args) == 0 {
return nil, fmt.Errorf("unable to build function with no args")
@@ -114,6 +114,20 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
var invariants []interfaces.Invariant
var invar interfaces.Invariant
// add the relationship to the returned value
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Expr,
Expr2: dummyOut,
}
invariants = append(invariants, invar)
// add the relationships to the called args
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Args[0],
Expr2: dummyFormat,
}
invariants = append(invariants, invar)
// first arg must be a string
invar = &interfaces.EqualsInvariant{
Expr: cfavInvar.Args[0],
@@ -121,6 +135,17 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
}
invariants = append(invariants, invar)
// XXX: We could add an alternate mode for this
// function where instead of knowing args[0]
// statically, if we happen to know all of the input
// arg types, we build the function, without verifying
// that the format string is valid... In this case, if
// it was built dynamically or happened to not be in
// the right format, we'd just print out some yucky
// result. The golang printf does something similar
// when it can't catch things statically at compile
// time.
value, err := cfavInvar.Args[0].Value() // is it known?
if err != nil {
return nil, fmt.Errorf("format string is not known statically")
@@ -150,12 +175,19 @@ func (obj *PrintfFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant, erro
}
dummyArg := &interfaces.ExprAny{}
invar := &interfaces.EqualsInvariant{
invar = &interfaces.EqualsInvariant{
Expr: dummyArg,
Type: x,
}
invariants = append(invariants, invar)
// add the relationships to the called args
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Args[i+1],
Expr2: dummyArg,
}
invariants = append(invariants, invar)
mapped[argName] = dummyArg
ordered = append(ordered, argName)
}