1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
-----------------------------------------------------------------------------
--- A tool to verify non-failure properties of Curry operations.
---
--- @author  Michael Hanus
--- @version August 2020
---------------------------------------------------------------------------

module Main where

import Directory    ( doesFileExist )
import FilePath     ( (</>) )
import Integer      ( ilog )
import IOExts
import List         ( (\\), elemIndex, find, isPrefixOf, isSuffixOf
                    , maximum, minimum, partition, splitOn, union )
import Maybe        ( catMaybes )
import State
import System

-- Imports from dependencies:
import Analysis.ProgInfo
import Analysis.TotallyDefined ( siblingCons )
import Analysis.Types
import Contract.Names
import Contract.Usage          ( checkContractUsage )
import CASS.Server             ( analyzeGeneric, analyzePublic )
import Debug.Profile
import FlatCurry.Annotated.TypeSubst ( substRule )
import FlatCurry.Files               ( readFlatCurryInt )
import FlatCurry.Types
import FlatCurry.Annotated.Goodies
import ShowFlatCurry                 ( showCurryModule )
import System.Path                   ( fileInPath )

-- Imports from package modules:
import ESMT
import Curry2SMT
import FlatCurry.Typed.Read
import FlatCurry.Typed.Goodies
import FlatCurry.Typed.Names
import FlatCurry.Typed.Types
import PackageConfig ( packagePath )
import ToolOptions
import VerifierState

------------------------------------------------------------------------
-- To support testing:

test :: Int -> String -> IO ()
test v = verifyNonFailingMod defaultOptions { optVerb = v }

testv :: String -> IO ()
testv = test 3

testcv :: String -> IO ()
testcv = verifyNonFailingMod defaultOptions { optVerb = 3, optContract = True }

------------------------------------------------------------------------

banner :: String
 = unlines [bannerLine,bannerText,bannerLine]
 where
   bannerText = "Fail-Free Verification Tool for Curry (Version of 03/08/20)"
   bannerLine = take (length bannerText) (repeat '=')

---------------------------------------------------------------------------
main :: IO ()
main = do
  args <- getArgs
  (opts,progs) <- processOptions banner args
  let optname = optName opts
  if not (null optname)
    then putStrLn $ "Non-failure condition for '" ++ optname ++ "':\n" ++
                    encodeContractName (optname ++ "'nonfail")
    else do
      z3exists <- fileInPath "z3"
      if z3exists
        then do
          when (optVerb opts > 0) $ putStrLn banner
          verifyNonFailingModules opts [] progs
        else do
          putStrLn "NON-FAILING ANALYSIS SKIPPED:"
          putStrLn "The SMT solver Z3 is required for the verifier to work"
          putStrLn "but the program 'z3' is not found on the PATH!"
          exitWith 1

verifyNonFailingModules :: Options -> [String] -> [String] -> IO ()
verifyNonFailingModules _ _ [] = done
verifyNonFailingModules opts verifiedmods (mod:mods)
  | mod `elem` verifiedmods
  = verifyNonFailingModules opts verifiedmods mods
  | optRec opts
  = do (Prog _ imps _ _ _) <- readFlatCurryInt mod
       let newimps = filter (`notElem` verifiedmods) imps
       if null newimps
         then do printWhenStatus opts ""
                 verifyNonFailingMod opts mod
                 verifyNonFailingModules opts (mod:verifiedmods) mods
         else verifyNonFailingModules opts verifiedmods
                     (newimps ++ mod : (mods \\ newimps))
  | otherwise -- non-recursive
  = do verifyNonFailingMod opts mod
       verifyNonFailingModules opts (mod:verifiedmods) mods


verifyNonFailingMod :: Options -> String -> IO ()
verifyNonFailingMod opts modname = do
  printWhenStatus opts $ "Analyzing module '" ++ modname ++ "':"
  prog <- readSimpTypedFlatCurryWithSpec opts modname
  let errs = checkContractUsage (progName prog)
               (map (\fd -> (snd (funcName fd), funcType fd)) (progFuncs prog))
  unless (null errs) $ do
    putStr $ unlines (map showOpError errs)
    exitWith 1
  impprogs <- mapIO (readSimpTypedFlatCurryWithSpec opts) (progImports prog)
  let allprogs = prog : impprogs
      vinfo  = foldr addFunsToVerifyInfo (initVerifyInfo opts)
                     (map progFuncs allprogs)
      vstate = foldr addProgToState (initVState vinfo) allprogs
  siblingconsinfo <- loadAnalysisWithImports siblingCons prog
  pi1 <- getProcessInfos
  printWhenAll opts $ unlines $
    ["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line]
  vstref <- newIORef vstate
  proveNonFailingFuncs opts siblingconsinfo vstref (progFuncs prog)
  stats <- readIORef vstref
  pi2 <- getProcessInfos
  let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
              maybe 0 id (lookup ElapsedTime pi1)
  when (optTime opts) $ putStrLn $
    "TOTAL VERIFICATION TIME  : " ++ show tdiff ++ " msec"
  when (optVerb opts > 0 || not (isVerified stats)) $
    putStr (showStats stats)
 where
  line = take 78 (repeat '-')

  showOpError (qf,err) =
    snd qf ++ " (module " ++ fst qf ++ "): " ++ err

-- Loads CASS analysis results for a module and its imported entities.
loadAnalysisWithImports :: Analysis a -> TAProg -> IO (ProgInfo a)
loadAnalysisWithImports analysis prog = do
  maininfo <- analyzeGeneric analysis (progName prog)
                >>= return . either id error
  impinfos <- mapIO (\m -> analyzePublic analysis m >>=
                                                     return . either id error)
                    (progImports prog)
  return $ foldr combineProgInfo maininfo impinfos

---------------------------------------------------------------------------
-- The state of the transformation process contains
-- * the current assertion
-- * a fresh variable index
-- * a list of all introduced variables and their types:
data TransState = TransState
  { preCond    :: Term
  , freshVar   :: Int
  , varTypes   :: [(Int,TypeExpr)]
  }

makeTransState :: Int -> [(Int,TypeExpr)] -> TransState
makeTransState = TransState tTrue

-- Increments fresh variable index.
incFreshVarIndex :: TransState -> TransState
incFreshVarIndex st = st { freshVar = freshVar st + 1 }

-- Adds variables to the state.
addVarTypes :: [(Int,TypeExpr)] -> TransState -> TransState
addVarTypes vts st = st { varTypes = vts ++ varTypes st }

---------------------------------------------------------------------------
-- Prove that a list of defined functions is fail free (w.r.t. their
-- non-fail conditions).
proveNonFailingFuncs :: Options -> ProgInfo [(QName,Int)] -> IORef VState
                     -> [TAFuncDecl] -> IO ()
proveNonFailingFuncs opts siblingconsinfo vstref =
  mapIO_ (proveNonFailingFunc opts siblingconsinfo vstref)

-- Prove that a function is fail free (w.r.t. their non-fail condition).
proveNonFailingFunc :: Options -> ProgInfo [(QName,Int)] -> IORef VState
                    -> TAFuncDecl -> IO ()
proveNonFailingFunc opts siblingconsinfo vstref fdecl =
  unless (isContractOp (funcName fdecl) || isProperty fdecl) $ do
    printWhenIntermediate opts $
      "Operation to be analyzed: " ++ snd (funcName fdecl)
    modifyIORef vstref incNumAllInStats
    let efdecl = etaExpandFuncDecl fdecl
    proveNonFailingRule opts siblingconsinfo vstref
                        (funcName efdecl) (funcType efdecl)
                        (funcRule efdecl)

-- Prove that a function rule is fail free (w.r.t. their non-fail condition).
-- The rule is in eta-expanded form.
proveNonFailingRule :: Options -> ProgInfo [(QName,Int)] -> IORef VState
                    -> QName -> TypeExpr -> TARule -> IO ()
proveNonFailingRule _ _ vstref qn ftype (AExternal _ _) = do
  ti <- readVerifyInfoRef vstref
  let atypes = argTypes ftype
      args   = zip [1 .. length atypes] atypes
      (nfcond,_)  = nonfailPreCondExpOf ti qn ftype args (makeTransState 0 [])
  unless (nfcond == tTrue) $ modifyIORef vstref incNumNFCInStats
proveNonFailingRule opts siblingconsinfo vstref qn@(_,fn) ftype
                    (ARule _ rargs rhs) = do
  ti <- readVerifyInfoRef vstref
  let -- compute non-fail precondition of operation:
      s0 = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) rargs
      (precondformula,s1)  = nonfailPreCondExpOf ti qn ftype rargs s0
      s2 = s1 { preCond = precondformula }
  unless (precondformula == tTrue)  $ modifyIORef vstref incNumNFCInStats
  -- verify only if the precondition is different from always failing:
  unless (precondformula == tFalse) $ proveNonFailExp ti s2 rhs
 where
  proveNonFailExp ti pts exp = case simpExpr exp of
    AComb _ ct (qf,qfty) args -> do
      mapIO_ (proveNonFailExp ti pts) args
      when (isCombTypeFuncPartCall ct) $
        let qnnonfail = toNonFailQName qf
        in maybe done -- h.o. call nonfailing if op. has no non-fail cond.
             (\_ -> do
               let reason = "due to call '" ++ ppTAExpr exp ++ "'"
               modifyIORef vstref (addFailedFuncToStats fn reason)
               printWhenIntermediate opts $
                 fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'")
             (find (\fd -> funcName fd == qnnonfail) (nfConds ti))
      when (ct==FuncCall) $ do
        printWhenIntermediate opts $ "Analyzing call to " ++ snd qf
        let ((bs,_)    ,pts1) = normalizeArgs args pts
            (bindexps  ,pts2) = mapS (binding2SMT True ti) bs pts1
            callargs = zip (map fst bs) (map annExpr args)
            (nfcondcall,pts3) = nonfailPreCondExpOf ti qf qfty callargs pts2
        -- TODO: select from 'bindexps' only demanded argument positions
        valid <- if nfcondcall == tTrue
                   then return (Just True) -- true non-fail cond. is valid
                   else do
                     modifyIORef vstref incFailTestInStats
                     let title = "SMT script to verify non-failing call of '" ++
                                 snd qf ++ "' in function '" ++ fn ++ "'"
                     checkImplicationWithSMT opts vstref title (varTypes pts3)
                          (preCond pts) (tConj bindexps) nfcondcall
        if valid == Just True
          then do
            printWhenIntermediate opts $
              fn ++ ": NON-FAILING CALL OF '" ++ snd qf ++ "'"
          else do
            let reason = if valid == Nothing
                           then "due to SMT error"
                           else "due to call '" ++ ppTAExpr exp ++ "'"
            modifyIORef vstref (addFailedFuncToStats fn reason)
            printWhenIntermediate opts $
              fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'"
    ACase _ _ e brs -> do
      proveNonFailExp ti pts e
      maybe
       (-- check a case expression for missing constructors:
        let freshvar = freshVar pts
            freshtypedvar = (freshvar, annExpr e)
            (be,pts1) = binding2SMT True ti (freshvar,e) (incFreshVarIndex pts)
            pts2 = pts1 { preCond = tConj [preCond pts, be]
                        , varTypes = freshtypedvar : varTypes pts1 }
            misscons = missingConsInBranch siblingconsinfo brs
        in do mapIO_ (verifyMissingCons pts2 freshtypedvar exp) misscons
              mapIO_ (proveNonFailBranch ti pts2 freshtypedvar) brs
       )
       (\ (fe,te) ->
           -- check a Boolean case with True/False branch:
           let (be,pts1) = pred2SMT e pts
               ptsf = pts1 { preCond = tConj [preCond pts, tNot be] }
               ptst = pts1 { preCond = tConj [preCond pts, be] }
           in do proveNonFailExp ti ptsf fe
                 proveNonFailExp ti ptst te
       )
       (testBoolCase brs)
    AOr _ e1 e2 -> do proveNonFailExp ti pts e1
                      proveNonFailExp ti pts e2
    ALet _ bs e -> do let ((rbs,re), pts1) = renameLetVars pts bs e
                      mapIO_ (proveNonFailExp ti pts1) (map snd rbs)
                      proveNonFailExp ti pts1 re
    AFree _ fvs e -> do let ((_,re), pts1) = renameFreeVars pts fvs e
                        proveNonFailExp ti pts1 re
    ATyped _ e _ -> proveNonFailExp ti pts e
    AVar _ _ -> done
    ALit _ _ -> done

  -- verify whether a variable (2. argument) can have the constructor (3. arg.)
  -- as a value w.r.t. the collected assertions
  verifyMissingCons pts (var,vartype) exp (cons,_) = do
    let title = "check missing constructor case '" ++ snd cons ++
                "' in function '" ++ fn ++ "'"
    printWhenIntermediate opts $
      title ++ "\nVAR: " ++ show (var,vartype) ++ "\nCASE:: " ++
      show (unAnnExpr (simpExpr exp))
    modifyIORef vstref incPatTestInStats

    valid <- checkImplicationWithSMT opts vstref ("SMT script to " ++ title)
               (varTypes pts) (preCond pts) tTrue
               (tNot (constructorTest False cons (TSVar var) vartype))
    unless (valid == Just True) $ do
      let reason = if valid == Nothing
                     then "due to SMT error"
                     else "maybe not defined on constructor '" ++
                          showQName cons ++ "'"
      modifyIORef vstref (addFailedFuncToStats fn reason)
      printWhenIntermediate opts $
        "POSSIBLY FAILING BRANCH in function '" ++ fn ++
        "' with constructor " ++ snd cons

  proveNonFailBranch ti pts (var,vartype) branch = do
    let (ABranch p e, pts1) = renamePatternVars pts branch
        -- set pattern type correctly (important for [] pattern)
        bpat = pat2smt (setAnnPattern vartype p)
        npts = pts1 { preCond = tConj [preCond pts1, tEquVar var bpat] }
    proveNonFailExp ti npts e

-- Returns the constructors (name/arity) which are missing in the given
-- branches of a case construct.
missingConsInBranch :: ProgInfo [(QName,Int)] -> [TABranchExpr] -> [(QName,Int)]
missingConsInBranch _ [] =
  error "missingConsInBranch: case with empty branches!"
missingConsInBranch _ (ABranch (ALPattern _ _) _ : _) =
  error "TODO: case with literal pattern"
missingConsInBranch siblingconsinfo
                    (ABranch (APattern _ (cons,_) _) _ : brs) =
  let othercons = maybe (error $ "Sibling constructors of " ++
                                 showQName cons ++ " not found!")
                        id
                        (lookupProgInfo cons siblingconsinfo)
      branchcons = map (patCons . branchPattern) brs
  in filter ((`notElem` branchcons) . fst) othercons

-- Simplifies a FlatCurry expression (only at the top-level!)
-- by considering the semantics of some predefined operations.
simpExpr :: TAExpr -> TAExpr
simpExpr exp = case exp of
  AComb ty FuncCall (qf,_) args ->
    if qf == pre "?"
      then AOr ty (args!!0) (args!!1)
      else if qf == pre "ord" || qf == pre "id" -- ops without preconditions
             then head args -- note: Char is implemented as Int in SMT
             else exp
  _ -> exp

-- Translates a FlatCurry expression to a Boolean formula representing
-- the binding of a variable (represented by its index in the first
-- component) to the translated expression (second component).
-- The translated expression is normalized when necessary.
-- For this purpose, a "fresh variable index" is passed as a state.
-- Moreover, the returned state contains also the types of all fresh variables.
-- If the first argument is `False`, the expression is not strictly demanded,
-- i.e., possible contracts of it (if it is a function call) are ignored.
binding2SMT :: Bool -> VerifyInfo -> (Int,TAExpr) -> State TransState Term
binding2SMT demanded ti (resvar,exp) =
 case simpExpr exp of
  AVar _ i -> returnS $ if resvar==i then tTrue
                                     else tEquVar resvar (TSVar i)
  ALit _ l -> returnS (tEquVar resvar (lit2smt l))
  AComb rtype ct (qf,_) args ->
    normalizeArgs args `bindS` \ (bs,nargs) ->
    -- TODO: select from 'bindexps' only demanded argument positions
    mapS (binding2SMT (isPrimOp qf || optStrict (toolOpts ti)) ti) bs
         `bindS` \bindexps ->
    comb2bool qf rtype ct nargs bs bindexps
  ALet _ bs e ->
    mapS (binding2SMT False ti)
         (map (\ ((i,_),ae) -> (i,ae)) bs) `bindS` \bindexps ->
    binding2SMT demanded ti (resvar,e) `bindS` \bexp ->
    returnS (tConj (bindexps ++ [bexp]))
  AOr _ e1 e2  ->
    binding2SMT demanded ti (resvar,e1) `bindS` \bexp1 ->
    binding2SMT demanded ti (resvar,e2) `bindS` \bexp2 ->
    returnS (tDisj [bexp1, bexp2])
  ACase _ _ e brs   ->
    getS `bindS` \ts ->
    let freshvar = freshVar ts
    in putS (addVarTypes [(freshvar, annExpr e)] (incFreshVarIndex ts)) `bindS_`
       binding2SMT demanded ti (freshvar,e) `bindS` \argbexp ->
       mapS branch2bool (map (\b->(freshvar,b)) brs) `bindS` \bbrs ->
       returnS (tConj [argbexp, tDisj bbrs])
  ATyped _ e _ -> binding2SMT demanded ti (resvar,e)
  AFree _ _ _ -> error "Free variables not yet supported!"
 where
   comb2bool qf rtype ct nargs bs bindexps
    | qf == pre "otherwise"
      -- specific handling for the moment since the front end inserts it
      -- as the last alternative of guarded rules...
    = returnS (tEquVar resvar tTrue)
    | ct == ConsCall
    = returnS (tConj (bindexps ++
                     [tEquVar resvar
                              (TComb (cons2SMT (null nargs) False qf rtype)
                                     (map arg2bool nargs))]))
    | qf == pre "apply"
    = -- cannot translate h.o. apply: ignore it
      returnS tTrue
    | isPrimOp qf
    = returnS (tConj (bindexps ++
                     [tEquVar resvar
                              (TComb (cons2SMT True False qf rtype)
                                     (map arg2bool nargs))]))
    | otherwise -- non-primitive operation: add contract only if demanded
    = let targs = zip (map fst bs) (map annExpr nargs) in
      preCondExpOf ti qf targs `bindS` \precond ->
      postCondExpOf ti qf (targs ++ [(resvar,rtype)]) `bindS` \postcond ->
      returnS (tConj (bindexps ++
                     if demanded && optContract (toolOpts ti)
                       then [precond,postcond]
                       else []))

   branch2bool (cvar, ABranch p e) =
     binding2SMT demanded ti (resvar,e) `bindS` \branchbexp ->
     getS `bindS` \ts ->
     putS ts { varTypes = patvars ++ varTypes ts} `bindS_`
     returnS (tConj [ tEquVar cvar (pat2smt p), branchbexp])
    where
     patvars = if isConsPattern p
                 then patArgs p
                 else []

   arg2bool e = case e of AVar _ i -> TSVar i
                          ALit _ l -> lit2smt l
                          _ -> error $ "Not normalized: " ++ show e

-- Returns the conjunction of the non-failure condition and precondition
-- (if the tool option `contract` is set) expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- Rename all local variables by adding the `freshvar` index to them.
nonfailPreCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)]
                    -> State TransState Term
nonfailPreCondExpOf ti qf ftype args =
  if optContract (toolOpts ti)
    then nonfailCondExpOf ti qf ftype args `bindS` \ (fvars,nfcond) ->
         preCondExpOf     ti qf (args ++ fvars) `bindS` \precond ->
         -- simplify term in order to check later for trivial precondition
         returnS (simpTerm (tConj [nfcond,precond]))
    else nonfailCondExpOf ti qf ftype args `bindS` \ (_,rt) -> returnS rt

-- Returns the non-failure condition expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- All local variables are renamed by adding the `freshvar` index to them.
-- If the non-failure condition requires more arguments (due to a
-- higher-order call), fresh arguments are added which are also returned.
nonfailCondExpOf :: VerifyInfo -> QName -> TypeExpr -> [(Int,TypeExpr)]
                 -> State TransState ([(Int,TypeExpr)], Term)
nonfailCondExpOf ti qf ftype args =
  maybe
    (predefs qf)
    (\fd -> let moreargs = funcArity fd - length args in
            if moreargs > 0
              then -- eta-expand function call with fresh variables so that one
                   -- can check non-fail conditions with a greater arity:
                let etatypes = argTypes (dropArgTypes (length args) ftype) in
                getFreshVarsForTypes (take moreargs etatypes) `bindS` \fvars ->
                applyFunc fd (args ++ fvars) `bindS` pred2SMT `bindS` \rt ->
                returnS (fvars,rt)
              else if moreargs < 0
                     then error $ "Operation '" ++ snd qf ++
                                  "': nonfail condition has too few arguments!"
                     else applyFunc fd args `bindS` pred2SMT `bindS` \rt ->
                          returnS ([],rt) )
    (find (\fd -> decodeContractQName (funcName fd) == toNonFailQName qf)
          (nfConds ti))
 where
  predefs qn | qn `elem` [pre "failed", pre "=:="] ||
               (qn == pre "error" && optError (toolOpts ti))
             = returnS ([],tFalse)
             | otherwise = returnS ([],tTrue)

-- Returns the precondition expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- Rename all local variables by adding the `freshvar` index to them.
preCondExpOf :: VerifyInfo -> QName -> [(Int,TypeExpr)] -> State TransState Term
preCondExpOf ti qf args =
  maybe (returnS tTrue)
        (\fd -> applyFunc fd args `bindS` pred2SMT)
        (find (\fd -> funcName fd == toPreCondQName qf) (preConds ti))

-- Returns the postcondition expression for a given operation
-- and its arguments (which are assumed to be variable indices).
-- Rename all local variables by adding `freshvar` to them and
-- return the new freshvar value.
postCondExpOf :: VerifyInfo -> QName -> [(Int,TypeExpr)]
              -> State TransState Term
postCondExpOf ti qf args =
  maybe (returnS tTrue)
        (\fd -> applyFunc fd args `bindS` pred2SMT)
        (find (\fd -> funcName fd == toPostCondQName qf) (postConds ti))


-- Applies a function declaration on a list of arguments,
-- which are assumed to be variable indices, and returns
-- the renamed body of the function declaration.
-- All local variables are renamed by adding `freshvar` to them.
-- Also the new fresh variable index is returned.
applyFunc :: TAFuncDecl -> [(Int,TypeExpr)] -> State TransState TAExpr
applyFunc fdecl targs s0 =
  let tsub = maybe (error $ "applyFunc: types\n" ++
                            show (argTypes (funcType fdecl)) ++ "\n" ++
                            show (map snd targs) ++ "\ndo not match!")
                   id
                   (matchTypes (argTypes (funcType fdecl)) (map snd targs))
      (ARule _ orgargs orgexp) = substRule tsub (funcRule fdecl)
      exp = rnmAllVars (renameRuleVar orgargs) orgexp
      s1  = s0 { freshVar = max (freshVar s0)
                                (maximum (0 : args ++ allVars exp) + 1) }
  in (simpExpr $ applyArgs exp (drop (length orgargs) args), s1)
 where
  args = map fst targs
  -- renaming function for variables in original rule:
  renameRuleVar orgargs r = maybe (r + freshVar s0)
                                  (args!!)
                                  (elemIndex r (map fst orgargs))

  applyArgs e [] = e
  applyArgs e (v:vs) =
    -- simple hack for eta-expansion since the type annotations are not used:
    -- TODO: compute correct type annotations!!! (required for overloaded nils)
    let e_v =  AComb failed FuncCall
                     (pre "apply", failed) [e, AVar failed v]
    in applyArgs e_v vs

-- Translates a Boolean FlatCurry expression into a Boolean formula.
-- Calls to user-defined functions are replaced by the first argument
-- (which might be true or false).
pred2SMT :: TAExpr -> State TransState Term
pred2SMT exp = case simpExpr exp of
  AVar _ i              -> returnS (TSVar i)
  ALit _ l              -> returnS (lit2smt l)
  AComb _ ct (qf,ftype) args -> comb2bool qf ftype ct (length args) args
  _                          -> returnS (tComb (show exp) []) -- TODO!
 where
  comb2bool qf ftype ct ar args
    | qf == pre "[]" && ar == 0
    = returnS (sortedConst "nil" (polytype2sort (annExpr exp)))
    | qf == pre "not" && ar == 1
    = pred2SMT (head args) `bindS` \barg -> returnS (tNot barg)
    | qf == pre "null" && ar == 1
    = let arg = head args
      in pred2SMT arg `bindS` \barg ->
         getS `bindS` \tstate ->
         returnS (tEqu barg
                       (sortedConst "nil"
                                    (polytype2sort (typeOfVar tstate arg))))
    | qf == pre "apply"
    = -- cannot translate h.o. apply: replace it by new variable
      getS `bindS` \ts ->
      let fvar = freshVar ts
          nts  = addVarTypes [(fvar,annExpr exp)] (incFreshVarIndex ts)
      in putS nts `bindS_`
         returnS (TSVar fvar)
    | qf == pre "/="
    = comb2bool (pre "==") ftype ct ar args `bindS` \be ->
      returnS (tNot be)
    | otherwise
    = mapS pred2SMT args `bindS` \bargs ->
      returnS (TComb (cons2SMT (ct /= ConsCall || not (null bargs))
                               False qf ftype)
                     bargs)

  typeOfVar tstate e = case e of
    AVar _ i -> maybe (error $ "pred2SMT: variable " ++ show i ++ " not found")
                      id
                      (lookup i (varTypes tstate))
    _        -> annExpr e -- might not be correct due to applyFunc!

normalizeArgs :: [TAExpr] -> State TransState ([(Int,TAExpr)],[TAExpr])
normalizeArgs [] = returnS ([],[])
normalizeArgs (e:es) = case e of
  AVar _ i -> normalizeArgs es `bindS` \ (bs,nes) ->
              returnS ((i,e):bs, e:nes)
  _        -> getS `bindS` \ts ->
              let fvar = freshVar ts
                  nts  = addVarTypes [(fvar,annExpr e)] (incFreshVarIndex ts)
              in putS nts `bindS_`
                 normalizeArgs es `bindS` \ (bs,nes) ->
                 returnS ((fvar,e):bs, AVar (annExpr e) fvar : nes)


-- Get for the types (given in the first argument) fresh typed variables.
getFreshVarsForTypes :: [TypeExpr] -> State TransState [(VarIndex, TypeExpr)]
getFreshVarsForTypes types pts =
  let n     = length types
      fv    = freshVar pts
      vars  = take n [fv ..]
      tvars = zip vars types
  in (tvars, pts { freshVar = fv + n, varTypes = tvars ++ varTypes pts })


-- Rename let-bound variables in a let expression.
renameLetVars :: TransState -> [((VarIndex, TypeExpr), TAExpr)] -> TAExpr
              -> (([((VarIndex, TypeExpr), TAExpr)], TAExpr),TransState)
renameLetVars pts bindings exp =
  let args = map (fst . fst) bindings
      minarg = minimum (0 : args)
      maxarg = maximum (0 : args)
      fv     = freshVar pts
      rnm i = if i `elem` args then i - minarg + fv else i
      nargs = map (\ ((v,t),_) -> (rnm v,t)) bindings
  in ((map (\ ((v,t),be) -> ((rnm v,t), rnmAllVars rnm be)) bindings,
       rnmAllVars rnm exp),
      pts { freshVar = fv + maxarg - minarg + 1
          , varTypes = nargs ++ varTypes pts })


-- Rename free variables introduced in an expression.
renameFreeVars :: TransState -> [(VarIndex, TypeExpr)] -> TAExpr
              -> (([(VarIndex, TypeExpr)], TAExpr),TransState)
renameFreeVars pts freevars exp =
  let args = map fst freevars
      minarg = minimum (0 : args)
      maxarg = maximum (0 : args)
      fv     = freshVar pts
      rnm i = if i `elem` args then i - minarg + fv else i
      nargs = map (\ (v,t) -> (rnm v,t)) freevars
  in ((map (\ (v,t) -> (rnm v,t)) freevars, rnmAllVars rnm exp),
      pts { freshVar = fv + maxarg - minarg + 1
          , varTypes = nargs ++ varTypes pts })


-- Rename argument variables of constructor pattern
renamePatternVars :: TransState -> TABranchExpr -> (TABranchExpr,TransState)
renamePatternVars pts (ABranch p e) =
  if isConsPattern p
    then let args = map fst (patArgs p)
             minarg = minimum (0 : args)
             maxarg = maximum (0 : args)
             fv = freshVar pts
             rnm i = if i `elem` args then i - minarg + fv else i
             nargs = map (\ (v,t) -> (rnm v,t)) (patArgs p)
         in (ABranch (updPatArgs (map (\ (v,t) -> (rnm v,t))) p)
                     (rnmAllVars rnm e),
             pts { freshVar = fv + maxarg - minarg + 1
                 , varTypes = nargs ++ varTypes pts })
    else (ABranch p e, pts)


---------------------------------------------------------------------------
-- Calls the SMT solver to check whether an assertion implies some
-- property.
checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)]
                        -> Term -> Term -> Term -> IO (Maybe Bool)
checkImplicationWithSMT opts vstref scripttitle vartypes
                        assertion impbindings imp = do
  let (pretypes,usertypes) =
         partition ((== "Prelude") . fst)
                   (foldr union [] (map (tconsOfTypeExpr . snd) vartypes))
  vst <- readIORef vstref
  let allsyms = catMaybes
                  (map (\n -> maybe Nothing Just (untransOpName n))
                       (map qidName
                         (allQIdsOfTerm (tConj [assertion, impbindings, imp]))))
  unless (null allsyms) $ printWhenIntermediate opts $
    "Translating operations into SMT: " ++
    unwords (map showQName allsyms)
  smtfuncs <- funcs2SMT vstref allsyms
  let decls = map (maybe (error "Internal error: some datatype not found!") id)
                  (map (tdeclOf vst) usertypes)
      smt   = concatMap preludeType2SMT (map snd pretypes) ++
              [ EmptyLine ] ++
              (if null decls
                 then []
                 else [ Comment "User-defined datatypes:" ] ++
                      map tdecl2SMT decls) ++
              [ EmptyLine, smtfuncs, EmptyLine
              , Comment "Free variables:" ] ++
              map typedVar2SMT vartypes ++
              [ EmptyLine
              , Comment "Boolean formula of assertion (known properties):"
              , sAssert assertion, EmptyLine
              , Comment "Bindings of implication:"
              , sAssert impbindings, EmptyLine
              , Comment "Assert negated implication:"
              , sAssert (tNot imp), EmptyLine
              , Comment "check satisfiability:"
              , CheckSat
              , Comment "if unsat, the implication is valid"
              ]
  --putStrLn $ "SMT commands as Curry term:\n" ++ show smt
  smtprelude <- readFile (packagePath </> "include" </> "Prelude.smt")
  let smtinput = "; " ++ scripttitle ++ "\n\n" ++ smtprelude ++ showSMT smt
  printWhenAll opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput
  printWhenAll opts $ "CALLING Z3 (with options: -smt2 -T:5)..."
  (ecode,out,err) <- evalCmd "z3" ["-smt2", "-in", "-T:5"] smtinput
  when (ecode>0) $ do printWhenAll opts $ "EXIT CODE: " ++ show ecode
                      writeFile "error.smt" smtinput
  printWhenAll opts $ "RESULT:\n" ++ out
  unless (null err) $ printWhenAll opts $ "ERROR:\n" ++ err
  let pcvalid = let ls = lines out in not (null ls) && head ls == "unsat"
  return (if ecode>0 then Nothing else Just pcvalid)
 where
  line = take 78 (repeat '-')

-- Operations axiomatized by specific smt scripts (no longer necessary
-- since these scripts are now automatically generated by Curry2SMT.funcs2SMT).
-- However, for future work, it might be reasonable to cache these scripts
-- for faster contract checking.
axiomatizedOps :: [String]
axiomatizedOps = ["Prelude_null","Prelude_take","Prelude_length"]

---------------------------------------------------------------------------
-- Translate a typed variables to an SMT declaration:
typedVar2SMT :: (Int,TypeExpr) -> Command
typedVar2SMT (i,te) = DeclareVar (SV i (polytype2sort te))

-- Gets all type constructors of a type expression.
tconsOfTypeExpr :: TypeExpr -> [QName]
tconsOfTypeExpr (TVar _) = []
tconsOfTypeExpr (FuncType a b) =  union (tconsOfTypeExpr a) (tconsOfTypeExpr b)
tconsOfTypeExpr (TCons qName texps) =
  foldr union [qName] (map tconsOfTypeExpr texps)
tconsOfTypeExpr (ForallType _ te) =  tconsOfTypeExpr te

---------------------------------------------------------------------------
-- Auxiliaries:

--- Tests whether the given branches of a case expressions
--- are a Boolean case distinction.
--- If yes, the expressions of the `False` and `True` branch
--- are returned.
testBoolCase :: [TABranchExpr] -> Maybe (TAExpr,TAExpr)
testBoolCase brs =
  if length brs /= 2 then Nothing
                     else case (brs!!0, brs!!1) of
    (ABranch (APattern _ (c1,_) _) e1, ABranch (APattern _ (c2,_) _) e2) ->
      if c1 == pre "False" && c2 == pre "True"  then Just (e1,e2) else
      if c1 == pre "True"  && c2 == pre "False" then Just (e2,e1) else Nothing
    _ -> Nothing

--- Shows a text with line numbers prefixed:
showWithLineNums :: String -> String
showWithLineNums txt =
  let txtlines  = lines txt
      maxlog    = ilog (length txtlines + 1)
      showNum n = (take (maxlog - ilog n) (repeat ' ')) ++ show n ++ ": "
  in unlines . map (uncurry (++)) . zip (map showNum [1..]) $ txtlines

---------------------------------------------------------------------------

{-

Still to be done:

- consider encapsulated search


Verified system libraries:

- Prelude
- Char
- Either
- ErrorState
- Integer
- Maybe
- State
- ShowS

 Prelude Char Either ErrorState Integer Maybe State ShowS

-}