Library POLAR_asn1_get_len

Require Import ssreflect ssrbool eqtype.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.
Require Import POLAR_parse_client_hello.

Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.

Module PolarSSL.
Include POLAR_parse_client_hello.PolarSSL.

Definition POLARSSL_ERR_ASN1_OUT_OF_DATA := cst32 (Z2s _ 20).
Definition POLARSSL_ERR_ASN1_INVALID_LENGTH := cst32 (Z2s _ 24).

Definition asn1_get_len : @while.cmd cmd0 bexp := (
  

  
  "_p_" <-* var_e "p" ;
  while.ifte (exp2bexp (sub_pe (var_e "end") (var_e "_p_") \<e cst32 (Z2s _ 1)))
  (
    "ret" <- POLARSSL_ERR_ASN1_OUT_OF_DATA ;
    ret
  )
  (
    
    "_c_" <-* var_e "_p_" ;
    while.ifte (exp2bexp ((var_e "_c_" \&e cst32 (Z2s _ 128)) \=e cst32 (Z2s _ 0)))
    (
      "_len0_" <-* var_e "_p_" ;
      var_e "len" *<- var_e "_len0_" ;
      "_p1_" <- add_pe (var_e "_p_") (cst32 (Z2s _ 1)) ;
      var_e "p" *<- var_e "_p1_" ;
      
      while.ifte (exp2bexp (sub_pe (var_e "end") (var_e "_p1_") \<e var_e "_len0_"))
      (
        "ret" <- POLARSSL_ERR_ASN1_OUT_OF_DATA ;
        ret
      )
      (
        "ret" <- cst32 (Z2s _ 0) ;
        ret
      )
    )
    (
      
      "_n_" <- var_e "_c_" \&e cst32 (Z2s _ 127) ;
      while.ifte (exp2bexp ((var_e "_n_") \=e (cst32 (Z2s _ 1))))
      (
        
        
        while.ifte (exp2bexp (sub_pe (var_e "end") (var_e "_p_") \<e cst32 (Z2s _ 2)))
        (
          "ret" <- POLARSSL_ERR_ASN1_OUT_OF_DATA ;
          ret
        )
        (
          
          "_len1_" <-* add_pe (var_e "_p_") (cst32 (Z2s _ 1)) ;
          var_e "len" *<- var_e "_len1_" ;
          "_p2_" <- add_pe (var_e "_p_") (cst32 (Z2s _ 2)) ;
          var_e "p" *<- var_e "_p2_" ;

          
          while.ifte (exp2bexp (sub_pe (var_e "end") (var_e "_p2_") \<e var_e "_len1_"))
          (
            "ret" <- POLARSSL_ERR_ASN1_OUT_OF_DATA ;
            ret
          )
          (
            "ret" <- cst32 (Z2s _ 0) ;
            ret
          )))
      (
      while.ifte (exp2bexp ((var_e "_n_") \=e (cst32 (Z2s _ 2))))
      (
        
        
        while.ifte (exp2bexp (sub_pe (var_e "end") (var_e "_p_") \<e cst32 (Z2s _ 3)))
        (
          "ret" <- POLARSSL_ERR_ASN1_OUT_OF_DATA ;
          ret
        )
        (
          
          "_len2_" <-* add_pe (var_e "_p_") (cst32 (Z2s _ 1)) ;
          "_len3_" <-* add_pe (var_e "_p_") (cst32 (Z2s _ 2)) ;
          "_len4_" <- (var_e "_len2_" \<<e cst32 (Z2s _ 8)) \|e var_e "_len3_" ;
          var_e "len" *<- var_e "_len4_" ;
          "_p3_" <- add_pe (var_e "_p_") (cst32 (Z2s _ 3)) ;
          var_e "p" *<- var_e "_p3_" ;

          
          while.ifte (exp2bexp (sub_pe (var_e "end") (var_e "_p3_") \<e var_e "_len4_"))
          (
            "ret" <- POLARSSL_ERR_ASN1_OUT_OF_DATA ;
            ret
          )
          (
            "ret" <- cst32 (Z2s _ 0) ;
            ret
          )))
      (
        "ret" <- POLARSSL_ERR_ASN1_INVALID_LENGTH ;
        ret
      )))))%string.

End PolarSSL.