Commit 9b98a547 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Add comments documenting exported functions and one extra test

parent aec28468
Pipeline #620 passed with stages
in 3 minutes and 21 seconds
......@@ -162,7 +162,7 @@ var cmdJson = &cobra.Command{
Args: cobra.ExactArgs(1),
Hidden: true,
Run: func(cmd *cobra.Command, args []string) {
err := vplogic.Json(args[0])
err := vplogic.JSON(args[0])
if err != nil {
cmdErrorFatal(err)
}
......
......@@ -239,6 +239,10 @@ var verifpalTests = []VerifpalTest{
Model: "exa.vp",
ResultsCode: "c1",
},
{
Model: "fakeauth.vp",
ResultsCode: "a0",
},
}
func TestMain(t *testing.T) {
......
......@@ -204,13 +204,13 @@ func constructKnowledgeMapRenderGenerates(
func constructKnowledgeMapRenderAssignment(
valKnowledgeMap KnowledgeMap, blck Block, declaredAt int, expr Expression,
) (KnowledgeMap, error) {
constants, err := sanityAssignmentConstants(expr.Right, []Constant{}, valKnowledgeMap)
constants, err := sanityAssignmentConstants(expr.Assigned, []Constant{}, valKnowledgeMap)
if err != nil {
return KnowledgeMap{}, err
}
switch expr.Right.Kind {
switch expr.Assigned.Kind {
case "primitive":
err := sanityPrimitive(expr.Right.Primitive, expr.Left)
err := sanityPrimitive(expr.Assigned.Primitive, expr.Constants)
if err != nil {
return KnowledgeMap{}, err
}
......@@ -238,7 +238,7 @@ func constructKnowledgeMapRenderAssignment(
)
}
}
for i, c := range expr.Left {
for i, c := range expr.Constants {
ii := valueGetKnowledgeMapIndexFromConstant(valKnowledgeMap, c)
if ii >= 0 {
return valKnowledgeMap, fmt.Errorf(
......@@ -254,12 +254,12 @@ func constructKnowledgeMapRenderAssignment(
Declaration: "assignment",
Qualifier: "private",
}
switch expr.Right.Kind {
switch expr.Assigned.Kind {
case "primitive":
expr.Right.Primitive.Output = i
expr.Assigned.Primitive.Output = i
}
valKnowledgeMap.Constants = append(valKnowledgeMap.Constants, c)
valKnowledgeMap.Assigned = append(valKnowledgeMap.Assigned, expr.Right)
valKnowledgeMap.Assigned = append(valKnowledgeMap.Assigned, expr.Assigned)
valKnowledgeMap.Creator = append(valKnowledgeMap.Creator, blck.Principal.Name)
valKnowledgeMap.KnownBy = append(valKnowledgeMap.KnownBy, []map[string]string{{}})
valKnowledgeMap.DeclaredAt = append(valKnowledgeMap.DeclaredAt, declaredAt)
......
......@@ -191,9 +191,9 @@ func coqPrincipalBlock(block Block, valKnowledgeMap KnowledgeMap) (string, error
func coqAssignemntExpression(expression Expression, valKnowledgeMap KnowledgeMap) ([]string, error) {
expressions := []string{}
switch expression.Right.Kind {
switch expression.Assigned.Kind {
case "equation":
cre, err := coqResolveEquation(expression.Right.Equation, valKnowledgeMap)
cre, err := coqResolveEquation(expression.Assigned.Equation, valKnowledgeMap)
if err != nil {
return []string{}, err
}
......@@ -201,13 +201,13 @@ func coqAssignemntExpression(expression Expression, valKnowledgeMap KnowledgeMap
"EXP assignment private %s unleaked;", cre,
))
case "primitive":
switch expression.Right.Primitive.Name {
switch expression.Assigned.Primitive.Name {
case "HASH", "PW_HASH", "CONCAT":
exp := fmt.Sprintf(
"EXP assignment private (prim(%s%d ",
expression.Right.Primitive.Name,
len(expression.Right.Primitive.Arguments))
for _, argument := range expression.Right.Primitive.Arguments {
expression.Assigned.Primitive.Name,
len(expression.Assigned.Primitive.Arguments))
for _, argument := range expression.Assigned.Primitive.Arguments {
crv, err := coqResolveValue(argument, valKnowledgeMap)
if err != nil {
return []string{}, err
......@@ -216,14 +216,14 @@ func coqAssignemntExpression(expression Expression, valKnowledgeMap KnowledgeMap
}
expressions = append(expressions, fmt.Sprintf("%s)) unleaked;", exp))
case "SPLIT", "SHAMIR_SPLIT", "HKDF":
for i, lhs := range expression.Left {
for i, lhs := range expression.Constants {
if strings.HasPrefix(lhs.Name, "unnamed_") {
continue
} else {
exp := fmt.Sprintf(
"EXP assignment private (prim(%s%d ",
expression.Right.Primitive.Name, (i + 1))
for _, argument := range expression.Right.Primitive.Arguments {
expression.Assigned.Primitive.Name, (i + 1))
for _, argument := range expression.Assigned.Primitive.Arguments {
crv, err := coqResolveValue(argument, valKnowledgeMap)
if err != nil {
return []string{}, err
......@@ -234,7 +234,7 @@ func coqAssignemntExpression(expression Expression, valKnowledgeMap KnowledgeMap
}
}
default:
crp, err := coqResolvePrimitive(expression.Right.Primitive, valKnowledgeMap)
crp, err := coqResolvePrimitive(expression.Assigned.Primitive, valKnowledgeMap)
if err != nil {
return nil, err
}
......
......@@ -137,9 +137,9 @@ func goExpression(expression Expression) (string, error) {
"in an implementation template",
)
case "assignment":
right := goValue(expression.Right)
right := goValue(expression.Assigned)
left := []Constant{}
for i, c := range expression.Left {
for i, c := range expression.Constants {
left = append(left, c)
if strings.HasPrefix(c.Name, "unnamed") {
left[i].Name = "_"
......
......@@ -12,7 +12,8 @@ import (
"github.com/logrusorgru/aurora"
)
// InfoMessage prints a Verifpal status message.
// InfoMessage prints a Verifpal status message either in color or non-color format,
// depending on what is supported by the terminal.
func InfoMessage(m string, t string, showAnalysis bool) {
analysisCount := 0
if showAnalysis {
......@@ -25,6 +26,7 @@ func InfoMessage(m string, t string, showAnalysis bool) {
}
}
// InfoMessageRegular prints a Verifpal status message in non-color format.
func InfoMessageRegular(m string, t string, analysisCount int) {
infoString := ""
if analysisCount > 0 {
......@@ -58,6 +60,7 @@ func InfoMessageRegular(m string, t string, analysisCount int) {
}
}
// InfoMessageColor prints a Verifpal status message in color format.
func InfoMessageColor(m string, t string, analysisCount int) {
infoString := ""
if analysisCount > 0 {
......
/* SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi <nadim@symbolic.software>
* SPDX-License-Identifier: GPL-3.0-only */
// 806d8db3ce9f3ded40fd35fdba02fb84
// Package vplogic provides the core logic for all of Verifpal, allowing it to
// be imported as a package for use within other software.
package vplogic
import (
......@@ -10,30 +13,32 @@ import (
"os"
)
func Json(request string) error {
// JSON processes JSON requests made to Verifpal via the Visual Studio Code extension.
func JSON(request string) error {
reader := bufio.NewReader(os.Stdin)
inputString, _ := reader.ReadString(byte(0x04))
inputString = inputString[:len(inputString)-1]
switch request {
case "knowledgeMap":
return JsonKnowledgeMap(inputString)
return JSONKnowledgeMap(inputString)
case "principalStates":
return JsonPrincipalStates(inputString)
return JSONPrincipalStates(inputString)
case "prettyValue":
return JsonPrettyValue(inputString)
return JSONPrettyValue(inputString)
case "prettyQuery":
return JsonPrettyQuery(inputString)
return JSONPrettyQuery(inputString)
case "prettyPrint":
return JsonPrettyPrint(inputString)
return JSONPrettyPrint(inputString)
case "prettyDiagram":
return JsonPrettyDiagram(inputString)
return JSONPrettyDiagram(inputString)
case "verify":
return JsonVerify(inputString)
return JSONVerify(inputString)
}
return fmt.Errorf("invalid json subcommand")
}
func JsonKnowledgeMap(inputString string) error {
// JSONKnowledgeMap returns the KnowledgeMap struct for a given model in JSON format.
func JSONKnowledgeMap(inputString string) error {
m, err := Parse("model.vp", []byte(inputString))
if err != nil {
return err
......@@ -47,7 +52,8 @@ func JsonKnowledgeMap(inputString string) error {
return nil
}
func JsonPrincipalStates(inputString string) error {
// JSONPrincipalStates returns the KnowledgeMap struct for a given model in JSON format.
func JSONPrincipalStates(inputString string) error {
m, err := Parse("model.vp", []byte(inputString))
if err != nil {
return err
......@@ -61,7 +67,8 @@ func JsonPrincipalStates(inputString string) error {
return nil
}
func JsonPrettyValue(inputString string) error {
// JSONPrettyValue pretty-prints a Verifpal value expression and returns the result in JSON format.
func JSONPrettyValue(inputString string) error {
a := Value{}
err := json.Unmarshal([]byte(inputString), &a)
if err != nil {
......@@ -71,7 +78,8 @@ func JsonPrettyValue(inputString string) error {
return nil
}
func JsonPrettyQuery(inputString string) error {
// JSONPrettyQuery pretty-prints a Verifpal query expression and returns the result in JSON format.
func JSONPrettyQuery(inputString string) error {
q := Query{}
err := json.Unmarshal([]byte(inputString), &q)
if err != nil {
......@@ -81,7 +89,8 @@ func JsonPrettyQuery(inputString string) error {
return nil
}
func JsonPrettyPrint(inputString string) error {
// JSONPrettyPrint pretty-prints a Verifpal model and returns the result in JSON format.
func JSONPrettyPrint(inputString string) error {
m, err := Parse("model.vp", []byte(inputString))
if err != nil {
return err
......@@ -94,7 +103,8 @@ func JsonPrettyPrint(inputString string) error {
return nil
}
func JsonPrettyDiagram(inputString string) error {
// JSONPrettyDiagram formats a Verifpal model into a sequence diagram and returns the result in JSON format.
func JSONPrettyDiagram(inputString string) error {
m, err := Parse("model.vp", []byte(inputString))
if err != nil {
return err
......@@ -107,7 +117,8 @@ func JsonPrettyDiagram(inputString string) error {
return nil
}
func JsonVerify(inputString string) error {
// JSONVerify returns the verification result of a Verifpal model in JSON format.
func JSONVerify(inputString string) error {
m, err := Parse("model.vp", []byte(inputString))
if err != nil {
return err
......
......@@ -674,37 +674,37 @@ var g = &grammar{
},
{
name: "Constant",
pos: position{line: 205, col: 1, offset: 4697},
pos: position{line: 205, col: 1, offset: 4705},
expr: &actionExpr{
pos: position{line: 205, col: 13, offset: 4709},
pos: position{line: 205, col: 13, offset: 4717},
run: (*parser).callonConstant1,
expr: &seqExpr{
pos: position{line: 205, col: 13, offset: 4709},
pos: position{line: 205, col: 13, offset: 4717},
exprs: []interface{}{
&labeledExpr{
pos: position{line: 205, col: 13, offset: 4709},
pos: position{line: 205, col: 13, offset: 4717},
label: "Const",
expr: &ruleRefExpr{
pos: position{line: 205, col: 19, offset: 4715},
pos: position{line: 205, col: 19, offset: 4723},
name: "Identifier",
},
},
&zeroOrOneExpr{
pos: position{line: 205, col: 30, offset: 4726},
pos: position{line: 205, col: 30, offset: 4734},
expr: &seqExpr{
pos: position{line: 205, col: 31, offset: 4727},
pos: position{line: 205, col: 31, offset: 4735},
exprs: []interface{}{
&ruleRefExpr{
pos: position{line: 205, col: 31, offset: 4727},
pos: position{line: 205, col: 31, offset: 4735},
name: "_",
},
&litMatcher{
pos: position{line: 205, col: 33, offset: 4729},
pos: position{line: 205, col: 33, offset: 4737},
val: ",",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 205, col: 37, offset: 4733},
pos: position{line: 205, col: 37, offset: 4741},
name: "_",
},
},
......@@ -716,17 +716,17 @@ var g = &grammar{
},
{
name: "Constants",
pos: position{line: 214, col: 1, offset: 4837},
pos: position{line: 214, col: 1, offset: 4845},
expr: &actionExpr{
pos: position{line: 214, col: 14, offset: 4850},
pos: position{line: 214, col: 14, offset: 4858},
run: (*parser).callonConstants1,
expr: &labeledExpr{
pos: position{line: 214, col: 14, offset: 4850},
pos: position{line: 214, col: 14, offset: 4858},
label: "Constants",
expr: &oneOrMoreExpr{
pos: position{line: 214, col: 24, offset: 4860},
pos: position{line: 214, col: 24, offset: 4868},
expr: &ruleRefExpr{
pos: position{line: 214, col: 24, offset: 4860},
pos: position{line: 214, col: 24, offset: 4868},
name: "Constant",
},
},
......@@ -735,38 +735,38 @@ var g = &grammar{
},
{
name: "Phase",
pos: position{line: 226, col: 1, offset: 5103},
pos: position{line: 226, col: 1, offset: 5111},
expr: &actionExpr{
pos: position{line: 226, col: 10, offset: 5112},
pos: position{line: 226, col: 10, offset: 5120},
run: (*parser).callonPhase1,
expr: &seqExpr{
pos: position{line: 226, col: 10, offset: 5112},
pos: position{line: 226, col: 10, offset: 5120},
exprs: []interface{}{
&litMatcher{
pos: position{line: 226, col: 10, offset: 5112},
pos: position{line: 226, col: 10, offset: 5120},
val: "phase",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 226, col: 18, offset: 5120},
pos: position{line: 226, col: 18, offset: 5128},
name: "_",
},
&litMatcher{
pos: position{line: 226, col: 20, offset: 5122},
pos: position{line: 226, col: 20, offset: 5130},
val: "[",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 226, col: 24, offset: 5126},
pos: position{line: 226, col: 24, offset: 5134},
name: "_",
},
&labeledExpr{
pos: position{line: 226, col: 26, offset: 5128},
pos: position{line: 226, col: 26, offset: 5136},
label: "Number",
expr: &oneOrMoreExpr{
pos: position{line: 226, col: 33, offset: 5135},
pos: position{line: 226, col: 33, offset: 5143},
expr: &charClassMatcher{
pos: position{line: 226, col: 33, offset: 5135},
pos: position{line: 226, col: 33, offset: 5143},
val: "[0-9]",
ranges: []rune{'0', '9'},
ignoreCase: false,
......@@ -775,16 +775,16 @@ var g = &grammar{
},
},
&ruleRefExpr{
pos: position{line: 226, col: 40, offset: 5142},
pos: position{line: 226, col: 40, offset: 5150},
name: "_",
},
&litMatcher{
pos: position{line: 226, col: 42, offset: 5144},
pos: position{line: 226, col: 42, offset: 5152},
val: "]",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 226, col: 46, offset: 5148},
pos: position{line: 226, col: 46, offset: 5156},
name: "_",
},
},
......@@ -793,47 +793,47 @@ var g = &grammar{
},
{
name: "GuardedConstant",
pos: position{line: 239, col: 1, offset: 5370},
pos: position{line: 239, col: 1, offset: 5378},
expr: &actionExpr{
pos: position{line: 239, col: 20, offset: 5389},
pos: position{line: 239, col: 20, offset: 5397},
run: (*parser).callonGuardedConstant1,
expr: &seqExpr{
pos: position{line: 239, col: 20, offset: 5389},
pos: position{line: 239, col: 20, offset: 5397},
exprs: []interface{}{
&litMatcher{
pos: position{line: 239, col: 20, offset: 5389},
pos: position{line: 239, col: 20, offset: 5397},
val: "[",
ignoreCase: false,
},
&labeledExpr{
pos: position{line: 239, col: 24, offset: 5393},
pos: position{line: 239, col: 24, offset: 5401},
label: "Guarded",
expr: &ruleRefExpr{
pos: position{line: 239, col: 32, offset: 5401},
pos: position{line: 239, col: 32, offset: 5409},
name: "Identifier",
},
},
&litMatcher{
pos: position{line: 239, col: 43, offset: 5412},
pos: position{line: 239, col: 43, offset: 5420},
val: "]",
ignoreCase: false,
},
&zeroOrOneExpr{
pos: position{line: 239, col: 47, offset: 5416},
pos: position{line: 239, col: 47, offset: 5424},
expr: &seqExpr{
pos: position{line: 239, col: 48, offset: 5417},
pos: position{line: 239, col: 48, offset: 5425},
exprs: []interface{}{
&ruleRefExpr{
pos: position{line: 239, col: 48, offset: 5417},
pos: position{line: 239, col: 48, offset: 5425},
name: "_",
},
&litMatcher{
pos: position{line: 239, col: 50, offset: 5419},
pos: position{line: 239, col: 50, offset: 5427},
val: ",",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 239, col: 54, offset: 5423},
pos: position{line: 239, col: 54, offset: 5431},
name: "_",
},
},
......@@ -845,78 +845,78 @@ var g = &grammar{
},
{
name: "Primitive",
pos: position{line: 250, col: 1, offset: 5593},
pos: position{line: 250, col: 1, offset: 5601},
expr: &actionExpr{
pos: position{line: 250, col: 14, offset: 5606},
pos: position{line: 250, col: 14, offset: 5614},
run: (*parser).callonPrimitive1,
expr: &seqExpr{
pos: position{line: 250, col: 14, offset: 5606},
pos: position{line: 250, col: 14, offset: 5614},
exprs: []interface{}{
&labeledExpr{
pos: position{line: 250, col: 14, offset: 5606},
pos: position{line: 250, col: 14, offset: 5614},
label: "Name",
expr: &ruleRefExpr{
pos: position{line: 250, col: 19, offset: 5611},
pos: position{line: 250, col: 19, offset: 5619},
name: "PrimitiveName",
},
},
&litMatcher{
pos: position{line: 250, col: 33, offset: 5625},
pos: position{line: 250, col: 33, offset: 5633},
val: "(",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 250, col: 37, offset: 5629},
pos: position{line: 250, col: 37, offset: 5637},
name: "_",
},
&labeledExpr{
pos: position{line: 250, col: 39, offset: 5631},
pos: position{line: 250, col: 39, offset: 5639},
label: "Arguments",
expr: &oneOrMoreExpr{
pos: position{line: 250, col: 49, offset: 5641},
pos: position{line: 250, col: 49, offset: 5649},
expr: &ruleRefExpr{
pos: position{line: 250, col: 49, offset: 5641},
pos: position{line: 250, col: 49, offset: 5649},
name: "Value",
},
},
},
&ruleRefExpr{
pos: position{line: 250, col: 56, offset: 5648},
pos: position{line: 250, col: 56, offset: 5656},
name: "_",
},
&litMatcher{
pos: position{line: 250, col: 58, offset: 5650},
pos: position{line: 250, col: 58, offset: 5658},
val: ")",
ignoreCase: false,
},
&labeledExpr{
pos: position{line: 250, col: 62, offset: 5654},
pos: position{line: 250, col: 62, offset: 5662},
label: "Check",
expr: &zeroOrOneExpr{
pos: position{line: 250, col: 68, offset: 5660},
pos: position{line: 250, col: 68, offset: 5668},
expr: &litMatcher{
pos: position{line: 250, col: 68, offset: 5660},
pos: position{line: 250, col: 68, offset: 5668},
val: "?",
ignoreCase: false,
},
},
},
&zeroOrOneExpr{
pos: position{line: 250, col: 73, offset: 5665},
pos: position{line: 250, col: 73, offset: 5673},
expr: &seqExpr{
pos: position{line: 250, col: 74, offset: 5666},
pos: position{line: 250, col: 74, offset: 5674},
exprs: []interface{}{
&ruleRefExpr{
pos: position{line: 250, col: 74, offset: 5666},
pos: position{line: 250, col: 74, offset: 5674},
name: "_",
},
&litMatcher{
pos: position{line: 250, col: 76, offset: 5668},
pos: position{line: 250, col: 76, offset: 5676},
val: ",",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 250, col: 80, offset: 5672},
pos: position{line: 250, col: 80, offset: 5680},
name: "_",
},
},
......@@ -928,15 +928,15 @@ var g = &grammar{
},
{
name: "PrimitiveName",
pos: position{line: 266, col: 1, offset: 5938},
pos: position{line: 266, col: 1, offset: 5946},
expr: &actionExpr{
pos: position{line: 266, col: 18, offset: 5955},
pos: position{line: 266, col: 18, offset: 5963},
run: (*parser).callonPrimitiveName1,
expr: &labeledExpr{
pos: position{line: 266, col: 18, offset: 5955},
pos: position{line: 266, col: 18, offset: 5963},
label: "Name",
expr: &ruleRefExpr{
pos: position{line: 266, col: 23, offset: 5960},
pos: position{line: 266, col: 23, offset: 5968},
name: "Identifier",
},
},
......@@ -944,44 +944,44 @@ var g = &grammar{
},
{
name: "Equation",
pos: position{line: 270, col: 1, offset: 6020},
pos: position{line: 270, col: 1, offset: 6028},
expr: &actionExpr{
pos: position{line: 270, col: 13, offset: 6032},
pos: position{line: 270, col: 13, offset: 6040},
run: (*parser).callonEquation1,
expr: &seqExpr{
pos: position{line: 270, col: 13, offset: 6032},
pos: position{line: 270, col: 13, offset: 6040},
exprs: []interface{}{
&labeledExpr{
pos: position{line: 270, col: 13, offset: 6032},
pos: position{line: 270, col: 13, offset: 6040},
label: "First",
expr: &ruleRefExpr{
pos: position{line: 270, col: 19, offset: 6038},
pos: position{line: 270, col: 19, offset: 6046},
name: "Constant",
},
},
&seqExpr{
pos: position{line: 270, col: 29, offset: 6048},
pos: position{line: 270, col: 29, offset: 6056},
exprs: []interface{}{
&ruleRefExpr{
pos: position{line: 270, col: 29, offset: 6048},
pos: position{line: 270, col: 29, offset: 6056},
name: "_",
},
&litMatcher{
pos: position{line: 270, col: 31, offset: 6050},
pos: position{line: 270, col: 31, offset: 6058},
val: "^",
ignoreCase: false,
},
&ruleRefExpr{
pos: position{line: 270, col: 35, offset: 6054},
pos: position{line: 270, col: 35, offset: 6062},
name: "_",
},
},
},
&labeledExpr{
pos: position{line: 270, col: 38, offset: 6057},
pos: position{line: 270, col: 38, offset: 6065},
label: "Second",
expr: &ruleRefExpr{
pos: position{line: 270, col: 45, offset: 6064},
pos: position{line: 270, col: 45, offset: 6072},
name: "Constant",
},
},
......@@ -991,20 +991,20 @@ var g = &grammar{
},
{
name: "Value",
pos: position{line: 282, col: 1, offset: 6213},
pos: position{line: 282, col: 1, offset: 6221},
expr: &choiceExpr{
pos: position{line: 282, col: 10, offset: 6222},
pos: position{line: 282, col: 10, offset: 6230},
alternatives: []interface{}{
&ruleRefExpr{
pos: position{line: 282, col: 10, offset: 6222},
pos: position{line: 282, col: 10, offset: 6230},
name: "Primitive",
},
&ruleRefExpr{
pos: position{line: 282, col: 20, offset: 6232},
pos: position{line: 282, col: 20, offset: 6240},
name: "Equation",