Merge branch 'master' into _update-deps/runtimeverification/k

.github/workflows/test-pr.yml

@@ -39,7 +39,9 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: ${CONTAINER}
-      - name: 'Build and run integration tests'
+      - name: 'Build K definitions'
+        run: docker exec -u user ${CONTAINER} make kdist
+      - name: 'Run integration tests'
         run: docker exec -u user ${CONTAINER} make cov-integration
       - name: 'Tear down Docker container'
         if: always()

Makefile

@@ -52,7 +52,7 @@ kdist: kdist-build
 KDIST_ARGS :=
 
 kdist-build: poetry-install have-k
-	$(POETRY_RUN) kdist --verbose build -j3 $(KDIST_ARGS)
+	$(POETRY_RUN) kdist --verbose build -j4 $(KDIST_ARGS)
 
 kdist-clean: poetry-install
 	$(POETRY_RUN) kdist clean

package/smoke-test.sh

@@ -4,7 +4,7 @@ set -euxo pipefail
 
 kimp --help
 
-kimp run --verbose examples/sumto10.imp --env 'x=0,y=1' --env z=2
+kimp run --verbose examples/sumto10.imp --env 'x=0,y=1' --env b1=false --env b2=true
 
 kimp prove --verbose examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec
 

src/kimp/__main__.py

@@ -132,7 +132,16 @@ def create_argument_parser() -> ArgumentParser:
 
     # Run
     def env(s: str) -> list[tuple[str, int]]:
-        return [(var.strip(), int(val)) for var, val in (assign.split('=') for assign in s.split(','))]
+        def parse(s: str) -> int:
+            match s:
+                case 'true':
+                    return True
+                case 'false':
+                    return False
+                case _:
+                    return int(s)
+
+        return [(var.strip(), parse(val)) for var, val in (assign.split('=') for assign in s.split(','))]
 
     run_subparser = command_parser.add_parser('run', help='Run an IMP program', parents=[shared_args])
     run_subparser.add_argument('input_file', metavar='INPUT_FILE', type=file_path, help='Path to .imp file')

src/kimp/kdist/imp-semantics/calc.k

@@ -0,0 +1,35 @@
+requires "expr.k"
+
+
+module CALC-SYNTAX
+  imports EXPR-SYNTAX
+  imports ID-SYNTAX
+
+  syntax Expr ::= Id
+
+  syntax Stmt ::= Id "=" Expr ";" [group(stmt), strict(2), format(%1 %2 %3%4)]
+  syntax Stmt ::= right:
+                  Stmt Stmt       [group(seq-stmt), format(%1%n%2)]
+
+  syntax priority stmt > seq-stmt
+endmodule
+
+
+module CALC
+  imports CALC-SYNTAX
+  imports EXPR-RULES
+
+  configuration
+    <k   color="green">  $PGM:Stmt </k>
+    <env color="yellow"> $ENV:Map  </env>
+
+  rule [step]: <k> S1:Stmt S2:Stmt => S1 ~> S2 ... </k>
+
+  rule [var]:
+    <k> X:Id => V ... </k>
+    <env> X |-> V ... </env>
+
+  rule [assign]:
+    <k> X = V:Value ; => .K ... </k>
+    <env> E => E [ X <- V ] </env>
+endmodule

src/kimp/kdist/imp-semantics/expr.k

@@ -0,0 +1,72 @@
+module EXPR-SYNTAX
+  imports UNSIGNED-INT-SYNTAX
+  imports BOOL-SYNTAX
+
+  syntax Value   ::= Int
+                   | Bool
+
+  syntax KResult ::= Value
+
+  syntax Expr    ::= Value
+                   | "(" Expr ")"   [bracket, format(%1%2%3)]
+
+  syntax Expr    ::= "-" Expr       [strict, format(%1%2)]
+                   | "!" Expr       [strict, format(%1%2)]
+                   > left:
+                     Expr "*" Expr  [seqstrict]
+                   | Expr "/" Expr  [seqstrict]
+                   > left:
+                     Expr "+" Expr  [seqstrict]
+                   | Expr "-" Expr  [seqstrict]
+                   > left:
+                     Expr ">=" Expr [seqstrict]
+                   | Expr ">"  Expr [seqstrict]
+                   | Expr "<=" Expr [seqstrict]
+                   | Expr "<"  Expr [seqstrict]
+                   > left:
+                     Expr "==" Expr [seqstrict]
+                   | Expr "!=" Expr [seqstrict]
+                   > left:
+                     Expr "&&" Expr [strict(1)]
+                   > left:
+                     Expr "||" Expr [strict(1)]
+endmodule
+
+
+module EXPR-RULES
+  imports EXPR-SYNTAX
+  imports INT
+  imports BOOL
+
+  rule - X => 0 -Int X
+  rule ! B => notBool B
+
+  rule X + Y => X +Int Y
+  rule X - Y => X -Int Y
+  rule X * Y => X *Int Y
+  rule X / Y => X /Int Y
+
+  rule I1 >= I2 => I1 >=Int I2
+  rule I1 >  I2 => I1 >Int  I2
+  rule I1 <= I2 => I1 <=Int I2
+  rule I1 <  I2 => I1 <Int  I2
+
+  rule B1 == B2 => B1 ==Bool B2
+  rule I1 == I2 => I1 ==Int I2
+
+  rule B1 != B2 => B1 =/=Bool B2
+  rule I1 != I2 => I1 =/=Int  I2
+
+  rule true  && B => B
+  rule false && _ => false
+
+  rule true  || _ => true
+  rule false || B => B
+endmodule
+
+
+module EXPR
+    imports EXPR-RULES
+
+    configuration <k> $PGM:Expr </k>
+endmodule

src/kimp/kdist/imp-semantics/imp-verification.k

@@ -1,4 +1,5 @@
-requires "statements.k"
+requires "imp.k"
+
 
 module IMP-VERIFICATION-SYNTAX
     imports ID-SYNTAX
@@ -9,7 +10,7 @@ endmodule
 
 module IMP-VERIFICATION
     imports IMP-VERIFICATION-SYNTAX
-    imports STATEMENTS
+    imports IMP
 
     // inequality sign normalization
     rule          A  >Int B  => B  <Int A [simplification]

src/kimp/kdist/imp-semantics/imp.k

@@ -0,0 +1,38 @@
+requires "calc.k"
+
+
+module IMP-SYNTAX
+  imports CALC-SYNTAX
+
+  syntax Stmt ::= "if" "(" Expr ")" Stmt "else" Stmt [group(stmt), strict(1), avoid, format(%1 %2%3%4% %5 %6 %7)] // dangling else
+                | "if" "(" Expr ")" Stmt             [group(stmt), format(%1 %2%3%4 %5)]
+                | "while" "(" Expr ")" Stmt          [group(stmt), format(%1 %2%3%4 %5)] // not strict!
+                | "{" Stmt "}"                       [group(stmt), format(%1%i%n%2%d%n%3)]
+                | "{" "}"                            [group(stmt), format(%1%2)]
+endmodule
+
+
+module IMP
+  imports IMP-SYNTAX
+  imports CALC
+
+  rule [if-true]:  <k> if ( true  ) S1 else _  => S1 ... </k>
+  rule [if-false]: <k> if ( false ) _  else S2 => S2 ... </k>
+
+  rule [if-else]: <k> if ( C ) S => if ( C ) S else {} ... </k>
+
+  rule [while]:
+    <k>
+      while ( C ) S
+      =>
+      if ( C ) {
+        S
+        while ( C ) S
+      }
+      ...
+    </k>
+
+  rule [block]: <k> { S } => S ~> { } ... </k>
+
+  rule [done]: <k> { } => .K ... </k>
+endmodule