change include syntax to match updated Spartan

* s/include verbatim/include {:verbatim}/
 * don't include .gen.dfy files from sdfy, instead pass -includeSuffix

verified/ARMdecls-common.sdfy

@@ -1,4 +1,4 @@
-include{:verbatim} "ARMspartan.dfy"
+include {:verbatim} "ARMspartan.dfy"
 
 var{:state ok()}  ok:bool;
 var{:state mem()} mem:memmap;

verified/ARMdecls-refined.sdfy

@@ -1,5 +1,4 @@
 include "ARMdecls-common.sdfy"
-include{:verbatim} "ARMdecls-common.gen.dfy"
 
 var{:state osp()} sp:word;
 var{:state olr()} lr:word;

verified/ARMdecls-unrefined.sdfy

@@ -1,5 +1,4 @@
 include "ARMdecls-common.sdfy"
-include verbatim "ARMdecls-common.gen.dfy"
 
 var{:register OReg(R0)}  r0:int;
 var{:register OReg(R1)}  r1:int;

verified/allocate_page.sdfy

@@ -1,11 +1,9 @@
-include verbatim "Sets.dfy"
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "Sets.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 
 #verbatim
 lemma BoundedAddrspaceRefs(d:PageDb, n:PageNr)

verified/entry.sdfy

@@ -1,12 +1,10 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
-include verbatim "entry.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
+include {:verbatim} "entry.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 
 #verbatim
 function method banked_regs_framesize(): int { 18*4 }

verified/exception_handlers.sdfy

@@ -1,10 +1,9 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
-include verbatim "entry.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
+include {:verbatim} "entry.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 
 procedure switch_to_monitor()
     requires

verified/finalise.sdfy

@@ -1,11 +1,9 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 
 procedure kom_smc_finalise(
     {:register OReg(R1)} as_page:int,

verified/init_addrspace.sdfy

@@ -1,13 +1,10 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 include "memset.sdfy"
-include verbatim "memset.gen.dfy"
 
 /* Register allocation for init_addrspace paths:
  * r0 temp / err out

verified/init_dispatcher.sdfy

@@ -1,15 +1,11 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 include "allocate_page.sdfy"
-include verbatim "allocate_page.gen.dfy"
 include "memset.sdfy"
-include verbatim "memset.gen.dfy"
 
 procedure kom_smc_init_dispatcher(
     inout {:register OReg(R1)} disp_page:int,

verified/init_l2ptable.sdfy

@@ -1,19 +1,14 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
-include verbatim "bitvectors.i.dfy"
-include verbatim "ptebits.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
+include {:verbatim} "bitvectors.i.dfy"
+include {:verbatim} "ptebits.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 include "allocate_page.sdfy"
-include verbatim "allocate_page.gen.dfy"
 include "memset.sdfy"
-include verbatim "memset.gen.dfy"
 include "map_utils.sdfy"
-include verbatim "map_utils.gen.dfy"
 
 #verbatim
 lemma SameEntriesImpliesPageDbCorresponds(s:memstate, p: PageNr,

verified/kom_utils.sdfy

@@ -1,7 +1,6 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "bitvectors.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "bitvectors.i.dfy"
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 
 procedure page_paddr_impl(out operand phys:int, operand pagenr:int, out operand tmp:int)
     requires/ensures

verified/map_insecure.sdfy

@@ -1,12 +1,10 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
-include verbatim "ptebits.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
+include {:verbatim} "ptebits.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "map_secure.sdfy"
-include verbatim "map_secure.gen.dfy"
 
 procedure mkl2pte_insecure(
     inout {:register OReg(R3)} mapping:int,

verified/map_secure.sdfy

@@ -1,16 +1,12 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
-include verbatim "ptebits.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
+include {:verbatim} "ptebits.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 include "allocate_page.sdfy"
-include verbatim "allocate_page.gen.dfy"
 include "map_utils.sdfy"
-include verbatim "map_utils.gen.dfy"
 
 procedure update_l2pte(
     {:register OReg(R2)} as_page:int,

verified/map_utils.sdfy

@@ -1,8 +1,7 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "bitvectors.i.dfy"
-include verbatim "pagedb.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "bitvectors.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 
 procedure fetch_l1pte(
     operand l1pt_va:addr,

verified/memset.sdfy

@@ -1,6 +1,5 @@
-include verbatim "kom_common.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 
 procedure memcpy(operand dst:addr, operand src:addr, inout operand size:addr,
                  out operand tmp:int)

verified/mkdep.py

@@ -16,7 +16,7 @@ def mkdeps(filename):
 
 # this isn't perfect, but it should be good enough
 # (if people are writing adversarial dafny we've got bigger problems!)
-INCLUDE_RE = re.compile(r'^\s*include\s+(\w+\s*)?"([^"]*)"')
+INCLUDE_RE = re.compile(r'^\s*include\s+([^"]+\s*)?"([^"]*)"')
 
 for srcfile in sys.argv[1:]:
     basedir = os.path.dirname(srcfile)

verified/remove.sdfy

@@ -1,11 +1,9 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 
 procedure kom_smc_remove_non_addr_success(
     {:register OReg(R1)} page:int,

verified/sha/sha256-extensions.sdfy

@@ -10,7 +10,6 @@ include{:verbatim} "sha256.i.dfy"
 //include verbatim "sha256-refined-invariants.i.dfy"
 
 include "../ARMdecls-refined.sdfy"
-include{:verbatim} "../ARMdecls-refined.gen.dfy"
 
 
 procedure {:refined} load_32_bit_const(

verified/sha/sha256-refined.sdfy

@@ -5,12 +5,11 @@
 ///////////////////////////////////////////////////
 
 
-include verbatim "sha256.i.dfy"
-include verbatim "sha256-refined-helpers.i.dfy"
-include verbatim "sha256-refined-invariants.i.dfy"
+include {:verbatim} "sha256.i.dfy"
+include {:verbatim} "sha256-refined-helpers.i.dfy"
+include {:verbatim} "sha256-refined-invariants.i.dfy"
 
 include "../ARMdecls-refined.sdfy"
-include verbatim "../ARMdecls-refined.gen.dfy"
 
 #verbatim
 function method Sigma0(i:int) : word

verified/smc_handler.sdfy

@@ -1,29 +1,18 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 include "init_addrspace.sdfy"
-include verbatim "init_addrspace.gen.dfy"
 include "init_dispatcher.sdfy"
-include verbatim "init_dispatcher.gen.dfy"
 include "init_l2ptable.sdfy"
-include verbatim "init_l2ptable.gen.dfy"
 include "map_secure.sdfy"
-include verbatim "map_secure.gen.dfy"
 include "map_insecure.sdfy"
-include verbatim "map_insecure.gen.dfy"
 include "entry.sdfy"
-include verbatim "entry.gen.dfy"
 include "finalise.sdfy"
-include verbatim "finalise.gen.dfy"
 include "stop.sdfy"
-include verbatim "stop.gen.dfy"
 include "remove.sdfy"
-include verbatim "remove.gen.dfy"
 
 //=============================================================================
 // Top-level SMC handler

verified/stop.sdfy

@@ -1,11 +1,9 @@
-include verbatim "kom_common.i.dfy"
-include verbatim "pagedb.i.dfy"
-include verbatim "smcapi.i.dfy"
+include {:verbatim} "kom_common.i.dfy"
+include {:verbatim} "pagedb.i.dfy"
+include {:verbatim} "smcapi.i.dfy"
 
 include "ARMdecls-unrefined.sdfy"
-include verbatim "ARMdecls-unrefined.gen.dfy"
 include "kom_utils.sdfy"
-include verbatim "kom_utils.gen.dfy"
 
 procedure kom_smc_stop(
     {:register OReg(R1)} as_page:int,

verified/subdir.mk

@@ -2,6 +2,7 @@ DAFNYTIMELIMIT ?= 60
 SPARTANDIRECT ?= 1
 DAFNYFLAGS = /trace /errorTrace:0 /timeLimit:$(DAFNYTIMELIMIT) /ironDafny /allocated:1 \
     $(call mkdafnyflags,$(notdir $(*))) $(if $(DAFNYPROC),/proc:"$(DAFNYPROC)")
+SPARTANFLAGS = -includeSuffix .sdfy .gen.dfy
 
 # dafny flags: file-specific flags plus /noNLarith unless the file is named nlarith.x
 mkdafnyflags = $(DAFNYFLAGS_$(1)) $(if $(filter nlarith.%,$(1)),,/noNLarith)