floverParser.v 15.8 KB
Newer Older
1 2
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List
        Coq.Reals.Reals Coq.Bool.Bool Coq.QArith.QArith.
3

4
Require Import CertificateChecker Infra.MachineType.
5 6 7 8 9 10 11 12 13

Import Coq.Lists.List.ListNotations.

Inductive Token:Type :=
| DLET
| DRET
| DPRE
| DABS
| DCOND
14 15
| DGAMMA
| DTYPE:mType -> Token
Heiko Becker's avatar
Heiko Becker committed
16
| DFIXED
17
| DVAR
Heiko Becker's avatar
Heiko Becker committed
18
| DCONST: nat -> Token
19 20 21 22 23
| DNEG
| DPLUS
| DSUB
| DMUL
| DDIV
24
| DFRAC
25
| DCAST
Heiko Becker's avatar
Heiko Becker committed
26
| DFAIL: string -> Token.
27 28 29 30 31 32 33 34 35 36

Open Scope string_scope.

Definition getChar (input:string):=
  match input with
  |String c s => c
  | _ => ascii_of_nat 0
  end.

Definition getConst (c:ascii) :=
Heiko Becker's avatar
Heiko Becker committed
37
  ((nat_of_ascii c) - 48)%nat.
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54

Definition suffix (s:string) :=
match s with
|String c s' => s'
| EmptyString => EmptyString
end.

Definition isDigit (c:ascii) :=
  (48 <=? (nat_of_ascii c)) && (nat_of_ascii c <=? 57).

Definition isAlpha (c:ascii) :bool :=
  (65 <=? nat_of_ascii c) && (nat_of_ascii c <=? 90) ||
    (97 <=? nat_of_ascii c) && (nat_of_ascii c <=? 122).

Definition isAlphaNum (c :ascii) :bool :=
  isDigit c || isAlpha c.

Heiko Becker's avatar
Heiko Becker committed
55
Fixpoint lexConst (input:string) (akk:nat) :=
56 57 58 59
  match input with
  |String c input' =>
   if (isDigit c)
   then lexConst input' (akk * 10 + getConst c)
60
   else (akk, input)
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
  |EmptyString => (akk, input)
  end.

Fixpoint lexName (input:string) :=
    match input with
     | String char input' =>
       if (isAlphaNum char)
       then
         let (name, input') := lexName input' in
         (String char name, input')
       else ("", input)
     | "" => ("",input)
     end.

Fixpoint strSize str :nat :=
    match str with
    | String _ str' => 1 + strSize str'
    | "" => 0
    end.

Fixpoint lex input fuel :=
match fuel with
  |S fuel' =>
   match input with
       | String char input' =>
         if isDigit char
         then
           let (num, input'') := lexConst input 0 in
           DCONST num :: lex input'' fuel'
         else
           if isAlpha char
           then
             let (name, input'') := lexName input in
             match name with
                 | "Ret" => DRET :: lex input'' fuel'
                 | "Let" => DLET :: lex input'' fuel'
                 | "PRE" => DPRE :: lex input'' fuel'
                 | "ABS" => DABS :: lex input'' fuel'
99
                 | "GAMMA" => DGAMMA :: lex input'' fuel'
100
                 | "Var" => DVAR :: lex input'' fuel'
101
                 | "Cast" => DCAST :: lex input'' fuel'
Heiko Becker's avatar
Heiko Becker committed
102
                 | "F" => DFIXED :: lex input'' fuel'
103 104
                 | "MTYPE" => let ts := lex input'' fuel' in
                              (match ts with
Heiko Becker's avatar
Heiko Becker committed
105
                               |DCONST 16 :: ts' => DTYPE M16 :: ts'
106 107
                               |DCONST 32 :: ts' => DTYPE M32 :: ts'
                               |DCONST 64 :: ts' => DTYPE M64 :: ts'
Heiko Becker's avatar
Heiko Becker committed
108 109
                               |DFIXED :: DCONST w :: DCONST f :: ts' =>
                                DTYPE (F (Pos.of_nat w) (Pos.of_nat f)) :: ts'
110 111 112 113
                            (* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
                            (* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
                               | _ => []
                               end)
114 115 116 117 118 119 120 121
                 | _ => []
             end
           else
             match char with
                  | "+"%char => DPLUS :: lex input' fuel'
                  | "-"%char => DSUB  :: lex input' fuel'
                  | "*"%char => DMUL :: lex input' fuel'
                  | "/"%char => DDIV :: lex input' fuel'
122
                  | "035"%char => DFRAC :: lex input' fuel'
123 124 125 126
                  | "?"%char => DCOND :: lex input' fuel'
                  | "~"%char => DNEG :: lex input' fuel'
                  | " "%char => lex input' fuel'
                  | "010"%char => lex input' fuel'
Heiko Becker's avatar
Heiko Becker committed
127
                  | _ => DFAIL (String char ("")) :: []
128 129 130 131 132 133
              end
       |  _  => []
   end
  |_ => []
end.

134 135 136 137 138 139
Fixpoint str_join s1 s2 :=
  match s1 with
  | String c s1' => String c (str_join s1' s2)
  | "" => s2
  end.

140 141 142 143
Fixpoint str_of_num (n:nat) (m:nat):=
  match m with
    |S m' =>
     if n <? 10 then String (ascii_of_nat (n + 48)) ""
144
     else str_join (str_of_num (n/10) m') (String (ascii_of_nat ((n mod 10) + 48)) "")
145 146 147
    |_ => ""
  end .

148 149 150 151 152 153 154
Fixpoint type_to_string (m:mType) :=
match m with
|M32 => "MTYPE 32"
|M64 => "MTYPE 64"
| _ => "" (* FIXME *)
end.

155 156 157 158 159 160 161 162
Definition pp_token (token:Token) :=
  match token with
  | DLET => "Let"
  | DRET => "Ret"
  | DPRE => "PRE"
  | DABS => "ABS"
  | DCOND => "?"
  | DVAR => "Var"
Heiko Becker's avatar
Heiko Becker committed
163
  | DCONST num => str_of_num num num
164 165
  | DGAMMA => "Gamma"
  | DTYPE m => str_join "MTYPE " (type_to_string m)
Heiko Becker's avatar
Heiko Becker committed
166
  | DFIXED => ""
167 168 169 170 171 172
  | DNEG => "~"
  | DPLUS => "+"
  | DSUB => "-"
  | DMUL => "*"
  | DDIV => "/"
  | DFRAC => "#"
173 174
  | DCAST => "Cast"
  | DFAIL s => ""
175 176 177 178 179
  end .

(* Pretty Printer for Tokens *)
Fixpoint pp (tokList:list Token) :=
  match tokList with
180
  | token :: tokRest => str_join (pp_token token) ( str_join " " (pp tokRest))
181 182
  | [] => ""
  end.
183

184 185
(** Prefix form parser for exprressions **)
Fixpoint parseExp (tokList:list Token) (fuel:nat):option (expr Q * list Token) :=
186 187 188
  match fuel with
    |S fuel' =>
     match tokList with
189
     | DCONST n :: DFRAC :: DCONST m :: DTYPE t :: tokRest =>
190
       match m with
Heiko Becker's avatar
Heiko Becker committed
191 192
       | 0%nat => None
       |S p => Some (Const t (Z.of_nat n # (Pos.of_nat p)), tokRest)
193
       end
Heiko Becker's avatar
Heiko Becker committed
194
     | DVAR :: DCONST n :: tokRest => Some (Var Q n, tokRest)
195 196
     | DNEG :: tokRest =>
       match (parseExp tokRest fuel') with
197
       | Some (Const m c, tokRest) => Some (Const m (- c), tokRest)
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
       | Some (e1,tokRest') => Some (Unop Neg e1, tokRest')
       | None => None
       end
     | DPLUS :: tokRest =>
       match parseExp tokRest fuel' with
       | Some (e1,tokRest') =>
         match (parseExp tokRest' fuel') with
         | Some (e2, tokRest'') => Some (Binop Plus e1 e2, tokRest'')
         | None => None
         end
       | None => None
       end
     | DSUB :: tokRest =>
       match parseExp tokRest fuel' with
       | Some (e1,tokRest') =>
         match (parseExp tokRest' fuel') with
         | Some (e2, tokRest'') => Some (Binop Sub e1 e2, tokRest'')
         | None => None
         end
       | None => None
       end
     | DMUL :: tokRest =>
       match parseExp tokRest fuel' with
       | Some (e1,tokRest') =>
         match (parseExp tokRest' fuel') with
         | Some (e2, tokRest'') => Some (Binop Mult e1 e2, tokRest'')
         | None => None
         end
       | None => None
       end
     | DDIV :: tokRest =>
       match parseExp tokRest fuel' with
       | Some (e1,tokRest') =>
         match (parseExp tokRest' fuel') with
         | Some (e2, tokRest'') => Some (Binop Div e1 e2, tokRest'')
         | None => None
         end
       | None => None
       end
237 238 239 240 241 242
     | DCAST :: DTYPE m :: tokRest =>
       match parseExp tokRest fuel' with
       |Some (e1, tokRest') =>
        Some (Downcast  m e1, tokRest')
       |_ => None
       end
243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
     | _ => None
     end
    |_ => None
  end.

Definition parseRet input fuel :option (cmd Q * list Token):=
    match parseExp input fuel with
     | Some (e, tokRest) => Some (Ret e, tokRest)
     | None => None
    end .

Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
  match fuel with
    |S fuel' =>
     match input with
     (* We already have a valid let binding *)
259 260 261
     | DVAR ::DCONST n :: DTYPE m :: exprLetRest =>
       (* so we parse an exprression *)
       match parseExp exprLetRest fuel with
262 263 264 265 266 267 268
       | Some (e, letRest) =>
         match letRest with
             (* If we continue with a let *)
             | DLET :: letBodyRest =>
               (* Parse it *)
               match (parseLet letBodyRest fuel') with
               (* And construct a result from it *)
Heiko Becker's avatar
Heiko Becker committed
269
               | Some (letCmd, arbRest) => Some (Let m n e letCmd, arbRest)
270 271 272 273 274 275 276
               | _ => None
               end
             (* But if we have a return *)
             | DRET :: retBodyRest =>
               (* parse only this *)
               match (parseRet retBodyRest fuel) with
               (* and construct the result *)
Heiko Becker's avatar
Heiko Becker committed
277
               | Some (retCmd, arbRest) => Some (Let m n e retCmd, arbRest)
278 279 280 281
               | _ => None
               end
             | _ => None (* fail if there is no continuation for the let *)
       end
282
     | None => None (* fail if we do not have an exprression to bind *)
283 284 285 286 287 288 289 290 291
     end
    | _ => None (* fail if we cannot find a variable *)
  end
| _ => None
end.

Definition parseFrac (input:list Token) :option (Q * list Token) :=
  match input with
  | DNEG :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
292
    match m with
Heiko Becker's avatar
Heiko Becker committed
293 294
    |0%nat => None
    |S p => Some ((- Z.of_nat n # Pos.of_nat p),tokRest)
295
    end
296
  | DCONST n :: DFRAC :: DCONST m :: tokRest =>
297
    match m with
Heiko Becker's avatar
Heiko Becker committed
298 299
    |0%nat => None
    |S p => Some ((Z.of_nat n # Pos.of_nat p),tokRest)
300
    end
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
  | _ => None
  end.

Definition parseIV (input:list Token) :option (intv * list Token) :=
  match (parseFrac input) with
  |Some (iv_lo, tokRest) =>
   match (parseFrac tokRest) with
   | Some (iv_hi, tokList) => Some ((iv_lo, iv_hi), tokList)
   | _ => None
   end
  | _ => None
  end.

Definition defaultPre :(nat -> intv):= fun x => mkIntv 0 0.

Definition updPre (n:nat) (iv:intv) (P:precond) :=
  fun m => if (n =? m) then iv else P m.

(** Precondition parser:
  The precondition should be encoded in the following format:
  PRECOND ::= DCOND DVAR DCONST FRACTION FRACTION PRECOND | EPSILON
  The beginning of the precondition is marked by the DPRE token
**)
Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list Token) :=
  match fuel with
    |S fuel' =>
     match input with
     | DCOND :: DVAR :: DCONST n :: fracRest =>
       match parseIV fracRest with
       | Some (iv, precondRest) =>
         match parsePrecondRec precondRest fuel' with
Heiko Becker's avatar
Heiko Becker committed
332 333
         | Some (P, tokRest) => Some (updPre n iv P, tokRest)
         | None => Some (updPre n iv defaultPre, precondRest)
334 335 336 337 338 339 340 341 342 343 344 345 346 347
         end
       | _ => None
       end
     | _ => None
     end
    |_ => None
  end.

Definition parsePrecond (input :list Token) fuel :=
  match input with
  | DPRE :: tokRest => parsePrecondRec tokRest fuel
  | _ => None
  end.

348
Definition defaultAbsenv:analysisResult := FloverMap.empty (intv * error).
349

350
Definition updAbsenv (e:expr Q) (iv:intv) (err:Q) (A:analysisResult):=
351
  FloverMap.add e  (iv, err) A.
352 353 354 355 356 357 358 359 360 361

(** Abstract environment parser:
  The abstract environment should be encoded in the following format:
  ABSENV ::= ? EXPRESSION FRACTION FRACTION FRACTION ABSENV | EPSILON
  The beginning of the abstract environment is marked by the DABS token
**)
Fixpoint parseAbsEnvRec (input:list Token) fuel :option (analysisResult * list Token):=
  match fuel with
    |S fuel' =>
     match input with
362 363
     | DCOND :: exprRest =>
       match parseExp exprRest fuel with
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
       | Some (e,fracRest) =>
         match parseIV fracRest with
         | Some (iv, errRest) =>
           match parseFrac errRest with
           | Some (err, absenvRest) =>
             match parseAbsEnvRec absenvRest fuel' with
             | Some (A, tokRest) => Some (updAbsenv e iv err A, tokRest)
             | None => Some (updAbsenv e iv err defaultAbsenv, absenvRest)
             end
           | None => None
           end
         | _ => None
         end
       | None => None
       end
     | _ => Some (defaultAbsenv, input)
     end
    |_ => None
  end.

Definition parseAbsEnv (input:list Token) fuel :=
  match input with
  | DABS :: tokRest => parseAbsEnvRec tokRest fuel
  | _ => None
  end.

390 391 392 393 394 395
Definition defaultGamma := fun n:nat => None:option mType.

Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * list Token) :=
  match input with
  | DVAR :: DCONST n :: DTYPE m :: inputRest =>
    match parseGammaRec inputRest with
Heiko Becker's avatar
Heiko Becker committed
396
    | Some (Gamma, rest) => Some (updDefVars n m Gamma, rest)
397 398 399 400 401 402 403 404 405 406 407
    | None => None
     end
  | _  => Some (defaultGamma, input)
  end.

Definition parseGamma (input:list Token) :=
  match input with
  | DGAMMA :: tokenRest => parseGammaRec tokenRest
  | _ => None
  end.

408 409 410 411 412 413 414 415 416 417 418 419 420 421
Definition dParse  (input:list Token) fuel :=
  let cmdParse :=
      match input with
      | DLET :: tokRest => parseLet tokRest fuel
      | DRET :: tokRest => parseRet tokRest fuel
      | _ => None
      end
  in
  match cmdParse with
  | Some (dCmd, tokRest) =>
    match tokRest with
    | DPRE :: preRest =>
      match parsePrecond tokRest fuel with
      | Some (P, absenvRest) =>
422
        match absenvRest with
Heiko Becker's avatar
Heiko Becker committed
423 424
        | DABS :: _ =>
          match parseAbsEnv absenvRest fuel with
425 426 427 428 429 430 431
          | Some (A, residual) =>
            match parseGamma residual with
            | Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
            | _ => None
            end
          | _ => None
          end
Heiko Becker's avatar
Heiko Becker committed
432 433
        | DGAMMA :: _ =>
          match parseGamma absenvRest with
434 435 436 437 438 439 440
          | Some (Gamma, residual) =>
            match parseAbsEnv residual fuel with
            | Some (A,residual) => Some ((dCmd, P, A, Gamma), residual)
            | _ => None
            end
          | _ => None
          end
441 442
        | _ => None
        end
443
      | _ => None
444
      end
Heiko Becker's avatar
Heiko Becker committed
445
    | DABS :: _ =>
446
      match parseAbsEnv tokRest fuel with
447 448
      | Some (A, absenvRest) =>
        match absenvRest with
Heiko Becker's avatar
Heiko Becker committed
449 450
        | DPRE :: _ =>
          match parsePrecond absenvRest fuel with
451 452 453 454 455 456 457
          | Some (P, residual) =>
            match parseGamma residual with
            | Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
            | _ => None
            end
          | _ =>  None
          end
Heiko Becker's avatar
Heiko Becker committed
458 459
        | DGAMMA :: _ =>
          match parseGamma absenvRest with
460 461 462 463 464 465 466 467 468 469 470
          | Some (Gamma, residual) =>
            match parsePrecond residual fuel with
            | Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
            | _ => None
            end
          | _ => None
          end
        | _ => None
        end
      | _ => None
      end
Heiko Becker's avatar
Heiko Becker committed
471
    | DGAMMA :: _ =>
472 473 474
      match parseGamma tokRest with
      | Some (Gamma, absenvRest) =>
        match absenvRest with
Heiko Becker's avatar
Heiko Becker committed
475 476
        | DPRE :: _ =>
          match parsePrecond absenvRest fuel with
477 478 479 480 481 482 483
          | Some (P, residual) =>
            match parseAbsEnv residual fuel with
            | Some (A, residual) => Some ((dCmd,P,A,Gamma),residual)
            | _ => None
            end
          | _ =>  None
          end
Heiko Becker's avatar
Heiko Becker committed
484 485
        | DABS :: _ =>
          match parseAbsEnv absenvRest fuel with
486 487 488 489 490 491 492
          | Some (A, residual) =>
            match parsePrecond residual fuel with
            | Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
            | _ => None
            end
          | _ => None
          end
493 494
        | _ => None
        end
495
      | _ => None
496 497 498 499 500 501 502 503 504 505
      end
    | _ => None
    end
  | _ => None
  end.

Fixpoint check_rec (input:list Token) (num_fun:nat) fuel:=
  match num_fun with
  | S n' =>
    match dParse input fuel with
506 507
    | Some ((dCmd, P, A, Gamma), []) =>
      if CertificateCheckerCmd dCmd A P Gamma
508 509
      then "True\n"
      else "False\n"
510 511
    | Some ((dCmd, P, A, Gamma), residual) =>
      if CertificateCheckerCmd dCmd A P Gamma
512 513
      then check_rec residual n' fuel
      else "False\n"
514
    | None => "parse failure\n"
515 516 517 518 519 520 521 522 523 524
    end
  | _ => "failure num of functions given"
  end.

Fixpoint str_length s :=
  match s with
  |String c s' => S (str_length s')
  |"" => O
  end.

525
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
526
  match n with
527
  |S n' => CertificateCheckerCmd f A P Gamma && (check f P A Gamma n')
528 529 530 531 532 533 534
  |_ => true
  end.

Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
  match num_fun with
  |S nf =>
   match (dParse input fuel) with
535 536
   |Some ((f,P,A, Gamma), residual) =>
    if (check f P A Gamma iters)
537 538 539 540 541 542 543 544 545 546 547 548
    then
      match residual with
      |a :: b => check_all nf iters residual fuel
      |[] => "True"
      end
    else
      "False"
   |None => "Failure: Parse"
   end
  |_ => "Failure: Number of Functions in certificate\n"
  end.

549 550 551
Definition runChecker (input:string) :=
  let tokList := lex input (str_length input) in
  match tokList with
Heiko Becker's avatar
Heiko Becker committed
552
  | DCONST n :: DCONST m :: tokRest => check_all m n tokRest (List.length tokList * 100)
553 554
  | _ => "failure no num of functions"
  end.