check-examples

#! /usr/bin/env bash

## This file accepts a couple options (before any files)
## and then iterates over the remaining command-line arguments as files.
## The options are
##    -d <name>  -- here <name> is a default command (see below)
##    -l <lang>  -- <lang> is the name of a language to use as default
##                   (a language name as used with ```, e.g.,
##                   dafny, java, text, cli, ...)
##    -x <int>   -- <int> is an (non-negative) integer literal giving 
##                  a default exit code
##    -m         -- compare against error messages in headings
## It expects a file to be in github markdown format.
##
## It extracts each block of text that is between lines bounded by a pair
## of lines beginning with ```. The opening ``` is typically follwed
## immediately (without whitespace) by a language identifier. If no
## language identifier is present, the default language specified by the -l
## option is used; if there is no such option, an error is output.
## The extracted text is placed in a temporary file.
##
## If the text blocks are not in matching pairs of ``` markers or if 
## markers other than 3 backticks are used, the script will fail -- it is
## not robust against such non-well-formedness.
## Also, the backticks must start the line without leading whitespace and 
## the language identifier must follow without whitespace.
##
## Each block of extracted text is tested by applying a command.
## The command is stated by including in the ```dafny line the string
## <!-- command --> where in that HTML comment string, the 'command' is one
## of the commands below. If there is no such HTML comment, then the default
## command given by an option is used; if there is no such option, an error
## message is issued.
##
## In the description of behavior below, if -m has been given as an option
## then the comparison of the output line containing 'Error' is against the
## error message as recorded in the '##' heading just before the test
##
## Commands (here $F is the name of a file containing the dafny source code
## under test):
##   %no-check : do nothing
##   %check-verify <expect> or
##   %check-verify-warn : runs the command 
##              "dafny verify --use-basename-for-filename $F" and checks
##              (1) if <expect> is absent then the exit code is 0 and
##                  the output is just a success message
##              (2) if <expect> is non-empty. then the exit code is 4 and
##                  the actual output matches the content of the file <expect>
##                  if the command is %check-verify-warn, the exit code is 0
##   %check-resolve <expect> : runs the command
##              "dafny resolve --use-basename-for-filename $F" and checks
##              (1) if <expect> is absent then the exit code is 0 and
##                  the output is just a success message
##              (2) if <expect> is non-empty. then the exit code is 2 and
##                  the actual output matches the content of the file <expect>
##   %check-translate <expect> : runs the command
##              "dafny translate --useBaseNameForFileName --unicode-char=true $F" and checks
##              (1) if <expect> is absent then the exit code is 0 and
##                  the output is just a success message
##              (2) if <expect> is non-empty. then the exit code is r32 and
##                  the actual output matches the content of the file <expect>
##   %check-run <expect> : runs the command
##              "dafny run --use-basename-for-filename $F" and,
##              if <expect> is present, checks that the output matches the
##              content of the file names <expect>
##   %check-error
##   check

# See also the feature request to make this a proper Dafny ecosystem feature:
# https://github.com/dafny-lang/dafny/issues/4680

dir=$(dirname "${BASH_SOURCE[0]}")

dafny="$dir/../../../Scripts/dafny"

defaultCommand=
defaultExit=
defaultLang=
useHeadings=0
defOptions="--function-syntax:4 --use-basename-for-filename"
legacyOptions="-functionSyntax:4 -useBaseNameForFileName"

while getopts 'md:x:l:' opt; do
  case "$opt" in
    "d") defaultCommand="$OPTARG";;
    "x") defaultExit="$OPTARG";;
    "l") defaultLang="$OPTARG";;
    "m") useHeadings=1
  esac
done
shift $(($OPTIND - 1))

## Temporary file
text=text.dfy

## Tracks if there have been any failures
ANYFAIL=0

## Loop over all remaining command-line arguments
for file in $@ ; do
dir=$(dirname "$file")
filename=$(basename "$file")

## Whether this file fails
FAIL=0
## line number
n=0
## if inblock==1 we are in a ```-delimited block
inblock=0

msg=
## Read and process each line of the file.  The file is input on stdin 
## by redirection after the 'done' corresponding to this while-do
use=
command=
expect=
options=( )
default=0
while IFS= read -r line
do 
  let n++

  ## For header lines, extract the error message from the header text
  ## everything but the initial ##[ ]*, the enclosing ** and the appended {#_errorid_}
  ## The sed commands turn this into a pattern matching regex to match against the output of applying dafny to the example in the text:
  ## remove the trailing error id if present; remove initial ## **; remove trailing '**'; turn any italicized text, which marks some
  ## hole in the template to a '.*' matcher.
  ## May not be robust against parentheses, brackets or other regex-special symbols in the error message -- none of these encountered so far.

  ( echo "$line" | grep -E -e '[#][#] ' > /dev/null ) \
   && msg=`echo "$line" | sed -E -e 's/ \{#.*\}[ ]*$//' -e 's/^##[ ]*[*]*//' -e 's/[*]*$//' -e 's/\\*/\\\\*/' -e 's/_[a-z]+_/.*/g'`

  ## Check for the test command information
  echo "$line" | grep '^[ ]*<!-- [ ]*%' > /dev/null
  if [ "$?" == "0" ]; then 
      ##echo COMMAND "$line"
      contents=( `echo "$line" | sed -e 's/[^<]*<!--//' -e 's/-->//'` )
      echo "$line" | grep -e '%default' > /dev/null
      if [ "$?" == "0" ]; then 
        default=1; 
        echo "$line" | grep -e '%useHeadings' > /dev/null
        if [ "$?" == "0" ]; then useHeadings=1; fi
        defaultCommand=${contents[0]}
        continue
      fi
      command=${contents[0]}
      contents=( ${contents[@]:1} )
      while [ ${#contents[@]} != "0" ]; do
        if [ "${contents[0]}" == "%use" ]; then
          use=${contents[1]}
          contents=( ${contents[@]:2} )
        elif [ "${contents[0]}" == "%save" ]; then
          save=${contents[1]}
          contents=( ${contents[@]:2} )
        elif [ "${contents[0]}" == "%options" ]; then
          contents=${contents[@]:1}
          options=${contents[@]}
          contents=()
        elif [ -z "${contents[0]}" ]; then
          contents=()
        else
          expect=${contents[0]}
          contents=( ${contents[@]:1} )
        fi
      done
  fi
  ## Check for the marker
  echo "$line" | grep -e '^[ ]*[`][`][`]' > /dev/null 
  if [ "$?" == "0" ]; then
    if [ "$inblock" == "0" ]; then
      ## get language
      lang=`echo "$line" | sed -e 's/^[ ]*\`\`\`[\`]*//' -e 's/[ ]*$//'`
      if [ -z "$lang" ]; then
        lang=$defaultLang
        if [ -z "$lang" ]; then
          echo NO LANGUAGE LABEL $n "$line"
          FAIL=1
        fi
      fi

      inblock=1
      rm -f $text
      touch $text
    else
      ## End of backtick block, so check the text
      if [ -z "$command" -a "$lang" == "dafny" ]; then
        command="$defaultCommand"
        if [ -z "$command" ]; then
          echo "NO COMMAND GIVEN $n $line"
          FAIL=1
        fi
      fi
      inblock=0
      if [ -n "$use" ]; then
        ##echo " " USING $use
        cat "$use" >> $text
      fi
      if [ -n "$save" ]; then
         cp $text $save
         save=
      fi
      if [ "$lang" == "dafny" -o "$lang" == "cli" ]; then
        echo TESTING $n $file "$command" $expect
      fi
      if [ "$command" == "%no-check" ]; then
        echo -n ""
      elif [ "$command" == "%check-verify" -o "$command" == "%check-verify-warn" -o "$command" == "%check-resolve"  -o "$command" == "%check-run" -o "$command" == "%check-translate" -o "$command" == "%check-test" -o "$command" == "%check-resolve-warn"  -o "$command" == "%check-legacy" ]; then
        capture=1
        dOptions=$defOptions
        if [ "$command" == "%check-verify" ]; then
          ##cat $text
          com=verify
          ec=4
        elif [ "$command" == "%check-verify-warn" ]; then
          com=verify
          ec=0
        elif [ "$command" == "%check-resolve" ]; then
          com=resolve
          ec=2
        elif [ "$command" == "%check-resolve-warn" ]; then
          com=resolve
          dOptions="$dOptions --allow-warnings"
          ec=0
        elif [ "$command" == "%check-translate" ]; then
          com=translate
          ec=3
        elif [ "$command" == "%check-run" ]; then
          com=run
          ec=0
          if [ "$useHeadings" == "1" ]; then ec=3; fi
        elif [ "$command" == "%check-test" ]; then
          com=test
          ec=2
          ##if [ "$useHeadings" == "1" ]; then ec=3; fi
        elif [ "$command" == "%check-legacy" ]; then
          com=
          ec=0
          dOptions=$legacyOptions
          if [ "$useHeadings" == "1" ]; then ec=3; fi
          if [ "$defaultCommand" == "%check-resolve" ]; then ec=2 ; fi
        fi
        if [ "$lang" != "dafny" ]; then
          echo EXPECTED A dafny BLOCK, NOT $lang
          FAIL=1
        else
          if [ "$capture" == "2" ]; then
            "$dafny" $com $dOptions ${options[@]} $text 2> actual > /dev/null
          elif [ "$com" == "%check-legacy" ]; then
            "$dafny" $com $dOptions ${options[@]} $text > actual
          else
            "$dafny" $com --function-syntax:4 $dOptions ${options[@]} $text --standard-libraries > actual
          fi
          actualec=$?
          if [ "$useHeadings" == "1" ]; then
            act=`cat actual | grep -E '(Error|Warning)' | sed -e 's/^[^:]*: //'`
            if [ -n "$msg" ]; then
              dif=`echo $act | sed -e "s/$msg//g" | sed -e 's/[ ]*//'`
              if [ -z "$act" ] ; then
                 echo NO ERROR MESSAGE FOUND
                 FAIL=1
              fi
              if [ -n "$dif" ] ; then
                 echo NO MATCH 
                 echo PAT "$msg"
                 echo ACT "$act"
                 echo DIF "$dif"
                 FAIL=1
              fi
              msg=
              if [ "$actualec" != "$ec" ]; then
                echo EXPECTED EXIT CODE $ec, got "$actualec"
                FAIL=1
              fi
            else 
              if [ -n "$act" ]; then
                echo "EXPECTED NO ERROR, got " $act
                FAIL=1
              fi
              if [ "$actualec" != "0" ]; then
                echo EXPECTED EXIT CODE 0, got $actualec
                FAIL=1
              fi
            fi
          elif [ -z "$expect" ]; then
            if [ "$actualec" != "0" ]; then
              echo "TEST FAILED" $file line $n  $command $expect
              cat $text
              cat actual
              FAIL=1
            fi
            # Warnings differ from version to version; "No trigger" is sometimes on a different line
            if [ `cat actual | grep -v "Warning" | grep -v "No trigger" | wc -l ` != "2" ]; then
              echo ACTUAL ERROR OUTPUT BUT NONE EXPECTED `cat actual | wc -l `
              cat actual
              FAIL=1
            fi
          else
            if [ "$actualec" != "$ec" ]; then
              echo EXPECTED EXIT CODE $ec, got $actualec
              FAIL=1
            fi
            if [ -e "$dir/$expect" ]; then
              # Warnings differ from version to version; "No trigger" is sometimes on a different line
              cat actual | grep -v "Warning" | grep -v "No trigger" | diff - "$dir/$expect"
              if [ "$?" != "0" ]; then
                FAIL=1
                echo Actual output differs from expected
                echo "TEST FAILED" $file line $n  $command $expect
                cat $text
                cat actual
              fi
            else
              echo EXPECT FILE $expect DOES NOT EXIST
              cat actual
              FAIL=1
            fi
          fi
        fi
      elif [ "$command" == "%check-cli" ]; then
        if [ "$lang" != "bash" ]; then
          echo EXPECTED A bash BLOCK, NOT $lang
          FAIL=1
        else
          . $text > actual
          ec=$?
          if [ "$ec" != "1" ]; then
             echo EXPECTED EXIT CODE OF 1, GOT $ec
             FAIL=1
          else
            act=`cat actual`
	    dif=`echo $act | sed -e "s/$msg//"`
            if [ -n "$dif" ]; then
              echo ACTUAL OUTPUT DOES NOT MATCH EXPECTED: "$msg" VS "$act"
              FAIL=1
            fi
          fi
        fi
      elif [ "$command" == "%check-error" ]; then
        "$dafny" resolve -useBaseNameForFileName --unicode-char:true $text | head -1 | sed -e 's/[^:]*: //' > actual
        act=`cat actual`
	dif=`echo "$act" | sed -e "s/$msg//"`
        if [ -n "$dif" ] ; then
           echo NO MATCH "$msg" VS "$act"
           FAIL=1
        fi
        msg=
      elif [ "$lang" == "dafny" ]; then
         echo UNKNOWN TEST COMMAND $command
         FAIL=1
      fi
      use=
      command=
      expect=
      options=( )
    fi
  elif [ "$inblock" == "1" ]; then
    ## If in a backtick block, save the text to the temporary file
    echo "$line" | sed -e 's/^[ ]*\.\.\./   /' >> $text
  fi
done < $file
rm -rf *.tmp $text.*

if [ "$inblock" == "1" ]; then
  echo UNCLOSED BACKTICK BLOCK
  FAIL=1
fi

if [ "$FAIL" == "1" ] ; then 
  echo Test Failure: $file
  ANYFAIL=1
fi

rm -f actual $text *.tmp
done
exit $ANYFAIL