Typingrules

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -2368,6 +2368,22 @@ object (self)
               rhs
          | _ -> rhs in
 
+       let is_rhs_volatile =
+         let rhsvars = Xprt.variables_in_expr rhs in
+         List.exists (fun v ->
+             if self#f#env#is_global_variable v then
+               TR.tfold_default
+                 (fun gvaddr ->
+                   if memmap#has_location gvaddr then
+                     let gloc = memmap#get_location gvaddr in
+                     gloc#is_volatile
+                   else
+                     false)
+                 false
+                 (self#f#env#get_global_variable_address v)
+             else
+               false) rhsvars in
+
        if self#f#env#is_global_variable lhs then
          let _ =
            log_diagnostics_result
@@ -2377,6 +2393,15 @@ object (self)
              ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs)] in
          [ABSTRACT_VARS [lhs]]
 
+       else if is_rhs_volatile then
+         let _ =
+           log_diagnostics_result
+             ~msg:(p2s self#l#toPretty)
+             ~tag:("get_assign_cmds_r: abstract volatile assignment")
+             __FILE__ __LINE__
+             ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs)] in
+         [ABSTRACT_VARS [lhs]]
+
        else
          let rhs =
            (* if rhs is a composite symbolic expression, create a new variable

CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml

@@ -157,6 +157,8 @@ object (self)
     | Ok ty -> is_scalar ty
     | _ -> false
 
+  method is_volatile: bool = BCHBCTypeUtil.is_volatile self#btype
+
   method is_typed: bool = not (btype_equal self#btype t_unknown)
 
   method size: int option = grec.gloc_size

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -4398,6 +4398,7 @@ class type global_location_int =
     method address: doubleword_int
     method btype: btype_t
     method size: int option
+    method is_volatile: bool
     method is_readonly: bool
     method is_initialized: bool
     method is_typed: bool

CodeHawk/CHB/bchlib/bCHSystemSettings.ml

@@ -119,7 +119,7 @@ let _ =
       ("LDR-memop-tc", "enable");
       ("LDR-stack-addr", "enable");
       ("LDR-struct-field", "enable");
-      ("LDRH-memop-tc", "enable");
+      ("LDRH-memop-tc", "disable");
       ("POP-sig-rv", "enable");
       ("STR-memop-tc", "enable")
     ]

CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml

@@ -1128,6 +1128,19 @@ object (self)
             ~error:(fun e -> log_error_result __FILE__ __LINE__ e)
             xtype_r);
 
+       (* LDRH rt, ...  : X_rt <: integer type *)
+         (let tc = mk_int_type_constant SignedNeutral 16 in
+          let tctypeterm = mk_cty_term tc in
+          let rttypeterm = mk_vty_term rttypevar in
+          let rule = "LDRH-def-lhs" in
+          if fndata#is_typing_rule_enabled iaddr rule then
+            begin
+              log_subtype_constraint __LINE__ rule tctypeterm rttypeterm;
+              store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm
+            end
+          else
+            log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm);
+
          (* LDRH rt, [rn, rm] :  X_rndef.load <: X_rt *)
          (let xrdef = get_variable_rdefs_r (rn#to_variable floc) in
           let rnreg = rn#to_register in
@@ -1684,7 +1697,8 @@ object (self)
          (match rn#get_kind with
           | ARMRegBitSequence (r, _, _) ->
              let rnreg = register_of_arm_register r in
-             let rndefs = get_variable_rdefs_r (rn#to_variable floc) in
+             let rnvar = Ok (floc#env#mk_arm_register_variable r) in
+             let rndefs = get_variable_rdefs_r rnvar in
              begin
                (List.iter (fun rnrdef ->
                     let rnaddr = rnrdef#getBaseName in
@@ -1714,8 +1728,8 @@ object (self)
          (regvar_type_introduction "UXTH" rd);
          (regvar_linked_to_exit "UXTH" rd);
 
-         (let opttc = mk_btype_constraint rdtypevar t_short in
-          let rule = "UBFX-def-lhs" in
+         (let opttc = mk_btype_constraint rdtypevar t_ushort in
+          let rule = "UXTH-def-lhs" in
           (match opttc with
            | Some tc ->
               if fndata#is_typing_rule_enabled iaddr rule then